| Project/Area Number |
24KF0214
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 外国 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Institute of Science Tokyo |
|---|
Principal Investigator |
鹿島 亮 東京科学大学, 情報理工学院, 准教授 (10240756)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KAWAKAMI PACHECO LEONARDO 東京科学大学, 情報理工学院, 外国人特別研究員
|
|---|
| Project Period (FY) |
2024-11-15 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 2026: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2025: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2024: ¥500,000 (Direct Cost: ¥500,000)
|
|---|
| Keywords | 直観主義的様相論理 |
|---|
| Outline of Research at the Start |
ミュー計算（通常は様相ミュー計算と呼ばれる）は様相論理に不動点演算子を加えて拡張した体系であり研究がさかんに行われているが、構成的ミュー計算（通常の古典論理ではなく直観主義論理をベースにしたもの）はほとんど研究されていない。構成的ミュー計算は古典論理ベースでは記述できない不完全な情報や矛盾する情報を表現できるので、より現実的な状況へ適用可能なモデル検査技術のための基礎となる。本研究では構成的ミュー計算の数学的な基本性質を解明し、さらその結果をPDL、LTLといったモデル検査の場面で実際に頻繁に使用されている様相論理に落とし込んで、構成的PDLや構成的LTLの基礎を確立することを目指す。
|
| Outline of Annual Research Achievements |
通常の様相論理は古典論理をベースにしているが、そのベースを直観主義論理に変更した論理を一般に直観主義様相論理と呼ぶ。本研究課題である構成的ミュー計算は、直観主義様相論理にさらに不動点演算子を加えて得られる論理である。現段階ではまだ構成的ミュー計算について直接的な成果は得られていないが、その前段階として直観主義様相論理および関連する論理に関する以下の成果を得た。
(1) IGLと呼ばれる論理はGLという様相論理の直観主義版である。GLは算術の証明可能性述語に対応する様相記号を持つ論理であり、「無限遷移を持たない」という興味深い性質のクリプキモデルにも対応し、広く研究されている。GLのベースを古典論理から直観主義論理に変更したものがIGLである。IGLに対して従来の研究は様相記号□だけを扱ってきた。そこに様相記号◇も追加すると表現能力が増えて良いのだが、論理の性質を分析することが極端に難しくなるので、◇も入ったIGLに対する研究は重要な研究課題である。当研究分担者は近年、◇入りIGLに対していくつかの証明体系を考察していたが、今回はそれらとは別に、無限分岐を持つ証明体系とヒルベルト流の証明体系という２つの新しい証明体系を与えた。これらを基にして◇入りIGLの研究のさらなる発展が期待できる。
(2) IS4と呼ばれる論理はS4という重要な様相論理のベースを直観主義論理に変更したものである。この論理に対しては従来はクリプキモデルによる意味論しか考察されていなかったが、これに対して位相的な意味論を与えた（これはDavid Fernandez-Duque氏との共同研究である）。
(3) 様相論理の変種であるハイブリッド論理と呼ばれる論理体系について、「対象が存在しない名前」を許すようように意味論を拡張して、それに対する証明体系を与えた（これは西村祐輝氏との共同研究である）。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の最終的な研究対象は構成的様相ミュー計算とその変種（μCS4など）である。上記の実績(1)にあげたIGL（あるいはGL）は不動点を持つ様相論理であり、様相ミュー計算の特殊例とみなすこともできる。また上記の実績(2)に挙げたIS4に不動点演算子を追加すればμCS4になる。つまり、現時点では様相ミュー計算そのものの本格的な研究には至っていないが、その前段階となるいくつかの論理に対する研究が順調に進んでいる。
|
| Strategy for Future Research Activity |
上記のように IGLやIS4に対するいくつかの研究成果が得られたので、それらを基にして構成的様相ミュー計算の本格的な研究に取り掛かる。具体的に現在決まっている予定としては、当研究分担者がバーミンガム大学を訪問して共同研究を行う。また７月にウィーンで開催される国際会議 Logic Colloquium 2025 に出席して本研究の途中経過を発表する。その他にも国内外の多くの研究集会に参加して研究者との情報交換を行い、研究を推進する。
|
