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 de(cid:12)ned predicates. Recently, there has been much interest in using cyclic proofs for proving properties described in separation logic with inductively de(cid:12)ned predicates. However, it is not known whether such systems has the cut-elimination property, an important meta-theoretic property of proof systems. Cut-elimination is not only of theoretical interest, because needing arbitrary cuts would mean that there is a limit to what one would be able to prove by a na(cid:127)(cid:16)ve mechanical proof search. In this paper, we answer the question by showing that the cut-elimination property fails in cyclic proof systems for separation logic. We present two systems, one for sequents with single-conclusion, and another for sequents with multiple-conclusions. To show the cut-elimination failure, we present concrete counter-example sequents which the systems can prove with cuts but not without cuts. The counter-examples are reasonably simple formulas about singly-linked lists, and therefore, suggest that the cut rule is important for a practical application of cyclic proofs to separation logic.
The Japan ACM SIGCHI Chapter and CHI2020 Japan Chapter local meeting committee reports on the online presentation of the Japan local meeting of ACM CHI2020, which was cancelled due to a new coronavirus disease (COVID-19) © 2020 Japan Society for Software Science and Technology All rights reserved
