| 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 2023)
|
| 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. 言語を制限した一階述語論理の循環証明体系のカット除去可能性：既に、1引数述語記号と1引数関数記号をもつ一階述語論理の循環証明体系についてはカット除去可能性が不成立であることを示す反例が示されているが、1引数述語記号を含み、関数記号を含まない一階述語論理の循環証明体系のカット除去可能性について調査した。とくに、変数の名前替えを同一視した上での証明中のシーケントの弱い有限性（擬有限性と呼ぶ）をもつ無限証明は循環証明に変換可能であることを示した。無限証明におけるカット除去手続は既に与えられているが、この手続を改良することにより擬有限性を保存するカット除去手続が得られると予想しており、これが示されれば1引数述語、関数記号なしにおけるカット除去可能性が証明される。
2. 帰納的定義節を制限した循環証明体系のカット除去可能性：乗法的連言のみを含むような線形命題論理の循環証明体系において、命題の帰納的定義節を準線形と呼ばれる非常に単純な形に制限してもカット除去可能性が不成立であることを示す反例を与えた。この反例よりただちに、シンボリック・ヒープ分離論理の循環証明体系において、準線形な帰納的定義節に制限してもカット除去可能性が不成立であることが示される。また、同様の体系において、結論に含まれない帰納的述語を用いたカットを利用しなければ証明できない例を示した。
さらに、前年度までの成果を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
当初、帰納的述語を準線形と呼ばれる非常に単純な形に制限することによりカット除去可能性が成立すると予想していたが、これが成立しない反例を発見した。応用面ではネガティヴな結果であるが、理論的には興味深い結果であり、予想とは異なる形で研究が進展していると考える。
|
| Strategy for Future Research Activity |
準線形な帰納的定義は、任意の帰納的命題に対して意味論的に同値な命題を定義できるようなクラスになっており、帰納的命題の表現力は変わらない。これまでに得られた結果より、帰納的定義の表現力を弱めることなくカット除去可能性を得ることは非常に難しいと考えられるため、帰納的定義に対するより本質的な制限が必要である。今後は、このような制限として適当なものを提案し、その中でカット除去可能性を証明することを目指す。
|
