| Project/Area Number |
20K03712
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Institute of Science Tokyo |
|---|
Principal Investigator |
鹿島 亮 東京科学大学, 情報理工学院, 准教授 (10240756)
|
|---|
| Project Period (FY) |
2020-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 様相論理 / 証明可能性論理 / シークエント計算 / ２階型付けラムダ計算 / 完全性 / 中間論理 / ２階論理 / 命題論理 / 非古典論理 |
|---|
| Outline of Research at the Start |
中間論理とは直観主義論理よりも強く古典論理よりも弱い論理体系の総称である。それらは使用する論理記号によって (1) 中間命題論理、(2) 中間１階述語論理、(3) 中間２階命題論理、(4) 中間２階述語および中間高階述語論理に分類される。(1,2)はすでに多く研究されているが(3)や(4)の研究は今までほとんどなされていなかった。その研究を立ち上げ、博士課程学生や学外の研究協力者とともに推進していく。
|
| Outline of Annual Research Achievements |
本研究課題である中間２階命題論理はクリプキモデルにさまざまな条件を加えることで得られる論理であるが、クリプキモデルを用いる論理の一般論が様相論理の研究である。すなわち中間２階命題論理の研究は様相論理の研究の特殊例と見なすことができる。中間２階命題論理に関して当初計画していた研究は進んでいないのだが、広い視点で様相論理の研究を進めており、以下の成果を得た。
（１）証明可能性論理GL（算術の証明可能性述語に対応する様相記号を持つ様相論理）は、「無限遷移を持たない」という条件のクリプキモデルを持ち、古くから深く研究されている重要な様相論理である。これに対して以前から行なってきた以下の２つの研究を完成させ、論文として発表した。(1-1) GLの入れ子シークエント計算のシンプルな構文論的カット除去（間庭彬仁氏との共同研究）。(1-2) GLの変種である様相論理Dのシークエント計算（倉橋太志氏、岩田荘平氏、森岡蒼氏との共同研究）。
（２）GLのベースを古典論理から直観主義論理に弱めた論理をIGLと呼ぶ。IGLの従来の研究は様相記号□しか持たない研究しかなかったが、様相記号◇も入れたIGLが近年研究され始めた。様相記号が増えたことで表現能力が高まるが、性質を分析することが極端に難しくなり、無限的な証明体系や技巧的な推論規則を持つ証明体系は研究されているがシンプルな証明体系は見つかっていない。そこでIGLのシンプルな証明体系を得ることを目的に研究を進め、ラベル付きシークエント計算に関していくつの結果を得た（ただし査読付きの会議・雑誌に投稿できるだけの結果にはまだ至っていない）。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
中間２階命題論理の研究は進んでいないが、様相論理、特にGLの周辺の論理についていくつの重要な結果を得ることができた。
|
| Strategy for Future Research Activity |
研究実績概要で述べたIGLの証明体系に関する研究を進める。また、当研究代表者が以前から取り組んでいる様相ミュー計算（様相論理に不動点演算子を追加したもので、記述能力が非常に高い有用な論理）の証明体系に関して、新しい進展のアイデアがあるのでそれについて研究を進める。これらについては、2024年秋から受け入れている外国人特別研究員とも共同して研究を行う。
|
