| 研究課題/領域番号 |
18K11161
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究分担者 |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | 分離論理 / シーケント計算 / カット除去 / 循環証明 |
|---|
| 研究実績の概要 |
本研究では，様々な論理体系，とくに，プログラム検証のための分離論理に対する循環証明体系に関する基本的性質について調査し，以下の結果が得られた．
1. 証明体系として期待される基本的な性質の一つであるカット除去可能性について，前年度までに分離論理のための循環証明体系においてカット除去定理が成立しないことを証明していたが，さらに，分離論理の理論的基盤であるbunched logicの循環証明体系においても同様にカット除去定理が成立しないことを証明した．
2. 証明探索の妨げにならない程度にカットを制限する可能性について考察した．具体的には，カットを用いないボトムアップ証明探索において出現し得る論理式のみをカット論理式として認めるカット規則を「推測可能なカット」と定義し，「任意の証明可能な結論が推測可能なカットのみで証明できる」という準カット除去可能性の概念を提案した．これは，（一般のカット除去定理が成立しない）様相論理のシーケント計算などで成立する性質である．
3. 分離論理の循環証明体系において準カット除去可能性が成立しないことを反例を用いて証明した．すなわち，任意のカットを用いて証明可能な結論で，推測可能なカットのみでは証明できないものが存在することを証明した．この結果は，分離論理の循環証明体系における証明探索に対する一つの限界を示す，理論的に重要な結果である．この結果は，プログラミング言語論分野の主要な国際会議であるFLOPS 2020に採録が決定している．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
カット除去可能性に関して，当初の予想とは異なる，理論的に非常に興味深い結論が得られた．これは証明探索の応用に対して否定的な結論であり，証明探索を用いた論理式の妥当性判定器の実現については進展が得られなかった．
|
| 今後の研究の推進方策 |
推測可能性という制限をさらに緩めることによって，証明探索の妨げにならないが，証明能力を弱めないようなカットを含む体系を構築することを目指す．これまでに得られた準カット除去可能性に対する反例から，そのような弱い制限に関するいくつかの知見が得られているので，それらをもとに研究を進める．
|
| 次年度使用額が生じた理由 |
新型コロナウイルス拡大防止のために出張の取り止めなどが発生したため。
該当額は今年度の研究打合せ旅費や書籍購入に充当する予定である。
|
