| 研究課題/領域番号 |
22K11901
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究分担者 |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| キーワード | 循環証明体系 / カット除去可能性 / 不動点演算子 / 分離論理 |
|---|
| 研究実績の概要 |
今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。
1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。
2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の見込みはおおよそ達成できたが、一階述語論理の循環証明体系に関する予想の証明は想定よりも難航したため解決しなかった。現時点で証明の目処が立ったため、次年度前半までに解決する予定である。
|
| 今後の研究の推進方策 |
引き続き、理論的な面では、一階述語論理の言語を制限した循環証明体系におけるカット除去性を調べる。「関数記号なしの場合、循環証明体系はカット除去可能である」ことを予想しているので、これを証明することを目指す。応用面では、とくに分離論理の循環証明体系においてカット論理式にある種の制限を課しても証明能力が変わらないことを示すことにより、自動証明探索に有用な証明体系を模索することを目指す。
|
| 次年度使用額が生じた理由 |
投稿論文の採録決定までの期間が予想を上回り年度を超過したため、投稿費用の予算を繰越し、翌年度に利用する予定である。
|
