Proof theoretic analysis of cyclic proof systems

2020 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

プログラミング言語理論

Academic Significance and Societal Importance of the Research Achievements

循環証明体系は，帰納的述語を含む論理式の妥当性判定のために有用であり，とくに分離論理の循環証明体系はプログラミング検証の分野への応用が期待される．証明探索においてカット規則を適用するためには発見的な手法が必要である．このため，カット除去定理は証明探索のために期待される性質である．本研究の結果は，完全な証明体系のためにはカット規則が必要であることを示すものであり，証明探索の実現のためにはある種の制限が必要であるという理論的限界を明らかにするものである．