| 研究課題/領域番号 |
18K11161
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究分担者 |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | 循環証明 / カット除去 / 分離論理 |
|---|
| 研究実績の概要 |
本研究では，様々な論理体系，とくに，プログラム検証のための分離論理に対する循環証明体系に関する基本的性質について調査し，以下の結果が得られた．
1. 証明体系として期待される基本的な性質の一つであるカット除去可能性について，分離論理のための循環証明体系においてカット除去定理が成立しないことを，反例を提示することによって証明した．この反例となる判断はカットを用いて証明できるが，カットなしの循環証明を構成することができないことを示した．この反例は非常に単純なものであり，線型論理などの場合に容易に拡張できると考えられる．さらにこの証明をもとに，O'Hearnらのbunched implicationの論理や，一階述語論理の循環証明体系に対して同様の反例を構成できると予想している．
2. 循環証明体系は自動証明への応用が期待されているが，カット規則の適用はカット論理式の探索において発見的な手法が必要とするため，カット除去定理の不成立は自動証明において大きな障害となる．そこで，一階述語論理のための循環証明体系において，カットを制限されたものに限定する部分的カット除去定理を予想し，そのための局所的カット除去手続を提案した．制限されたカット規則は，カット論理式の候補が狭い（とくに有限である）ため，自動証明に対しても有効である．このアイディアは分離論理など他の論理にも自然に適用可能であると予想している．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の予定どおり，分離論理のための循環証明体系に対するカット除去定理の不成立を証明できた．さらに，部分的カット除去定理に対して大きな進捗があり，種々の論理体系のための循環証明体系に対するカット除去可能性についての一般的な知見が得られた．
|
| 今後の研究の推進方策 |
本年度の成果を踏まえ，以下の課題を達成することを目標として研究を進める．
1. 分離論理に対して与えたカット除去定理の反例を，線型論理，一階述語論理，bunched implicationの論理などに適用し，これらの循環証明体系のカット除去定理が成立しないことを証明する．
2. 部分的カット除去定理の証明を完成させる．その結果をもとに，制限されたカットを含む循環証明体系における自動証明アルゴリズムについて考察する．
3. 無限証明に対する有限表現として，循環証明体系を包含する，より広いクラスを提案する．循環証明体系におけるカット除去定理の不成立の原因は，その正則性条件が強すぎることにあると考え，より広い無限証明のクラスでカット除去可能であるようなものを構成する．
|
| 次年度使用額が生じた理由 |
当初必要であると思われていた消耗品の購入が不要となったため、次年度の物品購入に充てる予定である。
|
