| 研究課題/領域番号 |
20K03712
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
鹿島 亮 東京工業大学, 情報理工学院, 准教授 (10240756)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 様相論理 / 証明可能性論理 |
|---|
| 研究実績の概要 |
本研究課題である中間2階命題論理はクリプキモデルに様々な条件を加えることで得られる論理であるが、クリプキモデルを用いる論理の研究の一般論が様相論理の研究である。すなわち中間2階命題論理の研究は様相論理の研究の特殊例とみなすことができる。現在、中間2階命題論理の当初計画していた研究はやや行き詰まっているので、より広い視点で様相論理の研究に重点を置いて研究を進めている。具体的には次の2つである。
(1)証明可能性論理(算術の証明可能性述語に対応する様相記号を持つ論理)について。これについては次の2つの成果を得た。(1-1) 証明可能性論理Dのシンプルなシークエント計算体系を2つ作り上げそれらのカット除去定理を証明した。この結果は2023年10月に開催された国際会議 17th Asian Logic Conference で発表するとともに、論文誌に投稿中である。(1-2) 証明可能性論理GLの入れ子シークエント計算の構文論的カット除去をシンプルに示した。GLは証明可能性論理の基本中の基本でありカット除去についても今までの多くの研究があるが、それに対して新しい成果を示した。この結果は2024年秋に開催される国際会議に投稿中である。
(2)様相ミュー計算の完全性について。様相ミュー計算は様相論理に不動点演算子を加えたもので、幅広い応用を持つ重要な論理である。この論理の証明体系の完全性はWalukiewicz(2000)によって示されているが、その証明は難解であり改良が期待されている。本研究でもこれに取り組みんでいるが、残念ながら2023年度には外部に発表できる実績は得られなかった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
計画策定時の見込み違いにより中間2階命題論理の性質が当初想定したものとやや異なることがわかり、当初やろうと思っていたことがあまりうまくできないことがわかってきた。これをどう回避するかは検討中である。
一方、より幅広い視点で様相論理の研究に取り組み、特に証明可能性論理のシークエント計算について良い成果を複数得ている。
|
| 今後の研究の推進方策 |
以下の3つのテーマについて研究を進める。
(1)証明可能性論理のカット除去の研究。証明可能性論理の従来の研究は算術の証明可能性に紐づいているが、その縛りから離れて純粋に「クリプキモデルのクラスで特徴付けられる論理」として研究を発展させる。また証明可能性論理のカット除去はカリーハワード対応によって計算の再帰呼び出しに対応すると考えることもできるので、その視点での研究を発展させる。
(2)様相ミュー計算の研究。2024年秋から受け入れ予定の学振外国人特別研究員との共同研究によって様相ミュー計算の証明体系の完全性の簡潔な証明を目指す。
(3)中間2階命題論理について、当初の見込みを適切に修正し研究を軌道に乗せる。
|
| 次年度使用額が生じた理由 |
研究打ち合わせのための出張の機会が少なかったため。2024年度は計画最終年度であり、海外での研究集会の旅費などに適切にすべて使用する予定である。
|
