論文

査読有り 招待有り 本文へのリンクあり
2020年

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

コンピュータソフトウェア
  • Daisuke Kimura
  • ,
  • Koji Nakazawa
  • ,
  • Tachio Terauchi
  • ,
  • Hiroshi Unno

37
1
開始ページ
1_39
終了ページ
1_52
記述言語
英語
掲載種別
研究論文(学術雑誌)
DOI
10.11309/jssst.37.1_39
出版者・発行元
日本ソフトウェア科学会

<p>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.</p>

リンク情報
DOI
https://doi.org/10.11309/jssst.37.1_39
CiNii Articles
http://ci.nii.ac.jp/naid/130007815024
URL
https://www.jstage.jst.go.jp/article/jssst/37/1/37_1_39/_article/-char/en/ 本文へのリンクあり
ID情報
  • DOI : 10.11309/jssst.37.1_39
  • ISSN : 0289-6540
  • CiNii Articles ID : 130007815024

エクスポート
BibTeX RIS