TY - JOUR

T1 - Failure of cut-elimination in cyclic proofs of separation logic

AU - Kimura, Daisuke

AU - Nakazawa, Koji

AU - Terauchi, Tachio

AU - Unno, Hiroshi

N1 - Funding Information:
Brotherston for valuable discussions about cyclic proofs. We also thank the anonymous referees for their helpful comments. This work is partially supported by JSPS KAKENHI Grant Numbers JP16H05856, JP17H01720, JP18K11161, JP17H01723, JP18K19787, and by JSPS Core-to-Core Program (A. Advanced Research Networks).
Publisher Copyright:
© 2020 Japan Society for Software Science and Technology. All rights reserved.

PY - 2020

Y1 - 2020

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

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

UR - http://www.scopus.com/inward/record.url?scp=85082526452&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85082526452&partnerID=8YFLogxK

U2 - 10.11309/jssst.37.1_39

DO - 10.11309/jssst.37.1_39

M3 - Article

AN - SCOPUS:85082526452

SN - 0289-6540

VL - 37

SP - 39

EP - 52

JO - Computer Software

JF - Computer Software

IS - 1

ER -