Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions. (English) Zbl 07700616

Kobayashi, Naoki (ed.), 6th international conference on formal structures for computation and deduction, FSCD 2021, Buenos Aires, Argentina, virtual conference, July 17–24, 2021. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 195, Article 11, 14 p. (2021).
Summary: Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, G. Kimura et al. [Comupter Software, 37(1):39–52 (2020)] have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.
For the entire collection see [Zbl 1465.68024].


68-XX Computer science
03B70 Logic in computer science
68Qxx Theory of computing
Full Text: DOI