| 研究課題/領域番号 |
18K11161
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| 研究分担者 |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2020年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2019年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2018年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 分離論理 / カット除去定理 / 循環証明 / シーケント計算 / カット除去 / 帰納的述語 / 証明論 / ソフトウェア検証 |
|---|
| 研究成果の概要 |
本研究では，帰納的に定義された述語を含む論理式に対する証明体系である循環証明体系に注目し，その基本性質であるカット除去可能性などの証明論的性質を調べた．主な成果は以下のとおりである．(1) プログラム検証に利用されている分離論理において，シンボリックヒープと呼ばれる論理式のクラスに対する循環証明体系ではカット除去ができない例があることを示した．(2) この循環証明体系において，カットをある種の部分論理式にまで制限しても証明能力が真に異なることを示した．(3) 分離論理の基盤論理であるbunched logicに対する循環証明体系でもカット除去ができない例があることを示した．
|
| 研究成果の学術的意義や社会的意義 |
循環証明体系は，帰納的述語を含む論理式の妥当性判定のために有用であり，とくに分離論理の循環証明体系はプログラミング検証の分野への応用が期待される．証明探索においてカット規則を適用するためには発見的な手法が必要である．このため，カット除去定理は証明探索のために期待される性質である．本研究の結果は，完全な証明体系のためにはカット規則が必要であることを示すものであり，証明探索の実現のためにはある種の制限が必要であるという理論的限界を明らかにするものである．
|
