Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

• KIMURA Daisuke

  Toho University

• NAKAZAWA Koji

  Nagoya University

• TERAUCHI Tachio

  Waseda University

• UNNO Hiroshi

  Tsukuba University

抄録

This paper studies the role of the cut rule in cyclic proof systems for separation logic. A cyclic proof system is a sequent-calculus style proof system for proving properties involving inductively defined predicates. Recently, there has been much interest in using cyclic proofs for proving properties described in separation logic with inductively defined predicates. In particular, for program verification, several theorem provers based on mechanical proof search procedures in cyclic proof systems for separation logic have been proposed. This paper shows that the cut-elimination property fails in cyclic proof systems for separation logic in several settings. We present two systems, one for sequents with single-antecedent and single-conclusion, and another for sequents with single-antecedent and multiple-conclusions. To show the cut-elimination failure, we present concrete and reasonably simple counter-example sequents which the systems can prove with cuts but not without cuts. This result suggests that the cut rule is important for a practical application of cyclic proofs to separation logic, since a naïve proof search procedure, which tries to find a cut-free proof, gives a limit to what one would be able to prove.

収録刊行物

• コンピュータ ソフトウェア

  コンピュータ ソフトウェア 37 (1), 1_39-1_52, 2020-01-24

  日本ソフトウェア科学会

詳細情報

• CRID: 1390846609815436416
• NII論文ID: 130007815024
• DOI: 10.11309/jssst.37.1_39
• ISSN: 02896540
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • CiNii Articles
  • KAKEN
  • Crossref
• 抄録ライセンスフラグ: 使用不可