Failure of cut-elimination in cyclic proofs of separation logic

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

研究成果: Article査読

2 被引用数 (Scopus)

抄録

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-onclusion, 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.

本文言語English
ページ(範囲)39-52
ページ数14
ジャーナルComputer Software
37
1
DOI
出版ステータスPublished - 2020

ASJC Scopus subject areas

  • Software

フィンガープリント 「Failure of cut-elimination in cyclic proofs of separation logic」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル