| 研究課題/領域番号 |
22K11901
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究分担者 |
木村 大輔 東邦大学, 理学部, 准教授 (90455197)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2025年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2022年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 循環証明体系 / 帰納的述語 / カット除去可能性 / 分離論理 / 不動点演算子 / 証明体系 / カット除去 |
|---|
| 研究開始時の研究の概要 |
循環証明体系は，帰納法に相当する原理を証明の循環構造によって表現する証明体系であり，自動証明との相性が良いことが知られている．本研究では，証明体系の重要な性質である「カット除去可能性」に注目する．カット規則は推論規則の一つであるが，カット規則の適用は自動証明においては不都合である．そのため，カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが，多くの循環証明体系ではカット除去可能性が成立しないことが分かっている．本研究では，論理に制限を課した上でのカット除去可能性や，自動証明の邪魔をしない程度までカット規則を制限できないか，などを明らかにする．
|
| 研究実績の概要 |
種々の論理に関する循環証明体系の証明論的性質について研究を行ない、以下の成果を得た。
1. 言語を制限した一階述語論理の循環証明体系のカット除去可能性：既に、1引数述語記号と1引数関数記号をもつ一階述語論理の循環証明体系についてはカット除去可能性が不成立であることを示す反例が示されているが、1引数述語記号を含み、関数記号を含まない一階述語論理の循環証明体系のカット除去可能性について調査した。とくに、変数の名前替えを同一視した上での証明中のシーケントの弱い有限性（擬有限性と呼ぶ）をもつ無限証明は循環証明に変換可能であることを示した。無限証明におけるカット除去手続は既に与えられているが、この手続を改良することにより擬有限性を保存するカット除去手続が得られると予想しており、これが示されれば1引数述語、関数記号なしにおけるカット除去可能性が証明される。
2. 帰納的定義節を制限した循環証明体系のカット除去可能性：乗法的連言のみを含むような線形命題論理の循環証明体系において、命題の帰納的定義節を準線形と呼ばれる非常に単純な形に制限してもカット除去可能性が不成立であることを示す反例を与えた。この反例よりただちに、シンボリック・ヒープ分離論理の循環証明体系において、準線形な帰納的定義節に制限してもカット除去可能性が不成立であることが示される。また、同様の体系において、結論に含まれない帰納的述語を用いたカットを利用しなければ証明できない例を示した。
さらに、前年度までの成果を3件の論文の形にまとめ、学術雑誌に投稿した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初、帰納的述語を準線形と呼ばれる非常に単純な形に制限することによりカット除去可能性が成立すると予想していたが、これが成立しない反例を発見した。応用面ではネガティヴな結果であるが、理論的には興味深い結果であり、予想とは異なる形で研究が進展していると考える。
|
| 今後の研究の推進方策 |
準線形な帰納的定義は、任意の帰納的命題に対して意味論的に同値な命題を定義できるようなクラスになっており、帰納的命題の表現力は変わらない。これまでに得られた結果より、帰納的定義の表現力を弱めることなくカット除去可能性を得ることは非常に難しいと考えられるため、帰納的定義に対するより本質的な制限が必要である。今後は、このような制限として適当なものを提案し、その中でカット除去可能性を証明することを目指す。
|
