循環証明体系におけるカット除去定理とカット規則の制限
| Project/Area Number |
22K11901
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2025: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 循環証明体系 / カット除去可能性 / 不動点演算子 / 分離論理 / 証明体系 / 帰納的述語 / カット除去 |
|---|
| Outline of Research at the Start |
循環証明体系は，帰納法に相当する原理を証明の循環構造によって表現する証明体系であり，自動証明との相性が良いことが知られている．本研究では，証明体系の重要な性質である「カット除去可能性」に注目する．カット規則は推論規則の一つであるが，カット規則の適用は自動証明においては不都合である．そのため，カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが，多くの循環証明体系ではカット除去可能性が成立しないことが分かっている．本研究では，論理に制限を課した上でのカット除去可能性や，自動証明の邪魔をしない程度までカット規則を制限できないか，などを明らかにする．
|
| Outline of Annual Research Achievements |
今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。
1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。
2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の見込みはおおよそ達成できたが、一階述語論理の循環証明体系に関する予想の証明は想定よりも難航したため解決しなかった。現時点で証明の目処が立ったため、次年度前半までに解決する予定である。
|
| Strategy for Future Research Activity |
引き続き、理論的な面では、一階述語論理の言語を制限した循環証明体系におけるカット除去性を調べる。「関数記号なしの場合、循環証明体系はカット除去可能である」ことを予想しているので、これを証明することを目指す。応用面では、とくに分離論理の循環証明体系においてカット論理式にある種の制限を課しても証明能力が変わらないことを示すことにより、自動証明探索に有用な証明体系を模索することを目指す。
|
Report
(1 results)
Research Products
(3 results)
