| 研究課題/領域番号 |
20K03712
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
鹿島 亮 東京工業大学, 情報理工学院, 准教授 (10240756)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 様相論理 |
|---|
| 研究実績の概要 |
本研究課題である中間2階命題論理はクリプキモデルに様々な条件を加えることで得られる論理であるが、クリプキモデルを用いる論理の研究の一般論が様相論理の研究である。すなわち中間2階命題論理の研究は様相論理の研究の特殊例とみなすことができる。現在、中間2階命題論理の当初計画していた研究はやや行き詰まっているので、より広い視点で様相論理の研究に重点を置いて研究を進めている。具体的には次の２つである。
（１）証明可能性論理（算術の証明可能性述語に対応する様相記号を持つ論理）について。これは前年度から引き続き研究を進めているものであるが大きな進展が得られた。2021年度は基本的な二つの論理（GLとGLS）のうちのあまり研究が進んでいなかったGLSについて、意味論的なカット除去を行った。2022年度はこの手法をDと呼ばれる論理に対して適用することに成功した。DはGLとGLSの中間に位置する論理であり、非正規様相論理なので一般の教科書には載っていないが、素直なクリプキモデルを持つ基本的な論理である。Dのシークエント計算は従来知られていなかったが、本研究ではDのシンプルなシークエント計算体系を２つ作り上げそれらのカット除去定理を証明した。
（２）様相ミュー計算の完全性について。様相ミュー計算は様相論理に不動点演算子を加えたもので、幅広い応用も持つ重要な論理である。この論理の証明体系の完全性はWalukiewicz(2000)によって示されているが、その証明は難解であり改良が期待されている。本研究でもこれに取り組み、タブロー法の完全性についての有名な論文（Niwinski and Walukiewicz, 1996)の不備を指摘した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
計画策定時の見込み違いにより、中間2階命題論理の性質が当初想定したものとやや異なることがわかり、当初やろうと思っていたことがあまりうまくできないことがわかってきた。これをどう回避するかは検討中である。
一方、より幅広い視点で様相論理の研究に取り組み、成果を挙げている。
|
| 今後の研究の推進方策 |
以下の３つのテーマについて研究を進める。
（１）証明可能性論理カット除去の研究。証明可能性論理の従来の研究は算術の証明可能性に紐づいているが、その縛りから離れて純粋に「クリプキモデルのクラスで特徴付けられる論理」として研究を発展させる。上述のDに対する結果はこの第一歩である。
（２）様相ミュー計算の研究。上述のように従来の論文の不備は明らかになったが，これに対する満足のいく修正はできていないのでまずはそれに取り組む。さらにそれを足がかりにして、様相ミュー計算の証明体系の完全性の簡潔な証明を目指す。
（３）中間2階命題論理について、当初の見込みを適切に修正し、研究を軌道に乗せる。
なお（２）と（３）については、博士課程学生にRAとして研究補助をしてもらう計画である。
|
| 次年度使用額が生じた理由 |
研究打ち合わせのための出張の機会が少なかったため。2023年度は対面での研究打ち合わせを当初計画よりやや多く実施して、次年度使用額を使用する予定である。
|
