Proof theoretic analysis of cyclic proof systems
| Project/Area Number |
18K11161
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
Nakazawa Koji 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
木村 大輔 東邦大学, 理学部, 講師 (90455197)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 分離論理 / カット除去定理 / 循環証明 / シーケント計算 / カット除去 / 帰納的述語 / 証明論 / ソフトウェア検証 |
|---|
| Outline of Final Research Achievements |
We investigate proof theoretic properties of cyclic proof systems, and we obtain the following results. (1) We show that the cut-elimination fails in the cyclic proof system for the symbolic heap separation logic. (2) We show that the restriction of the cut rule to extended subformulas of the bottom sequent in that system properly changes the provability. (3) We show that the cut-elimination fails in the cyclic proof system for the bunched logic.
|
| Academic Significance and Societal Importance of the Research Achievements |
循環証明体系は，帰納的述語を含む論理式の妥当性判定のために有用であり，とくに分離論理の循環証明体系はプログラミング検証の分野への応用が期待される．証明探索においてカット規則を適用するためには発見的な手法が必要である．このため，カット除去定理は証明探索のために期待される性質である．本研究の結果は，完全な証明体系のためにはカット規則が必要であることを示すものであり，証明探索の実現のためにはある種の制限が必要であるという理論的限界を明らかにするものである．
|
Report
(4 results)
Research Products
(9 results)
