Failure of cut-elimination in cyclic proofs of separation logic

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)39-52
Number of pages14
JournalComputer Software
Volume37
Issue number1
DOIs
Publication statusPublished - 2020

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Failure of cut-elimination in cyclic proofs of separation logic'. Together they form a unique fingerprint.

  • Cite this