Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions

Abstract Cyclic-proof systems are sequent-calculus-style proof systems that allow circular structures that represent induction. Cyclic-proof systems are considered suitable for automated inductive reasoning, and the cut-elimination property is desirable because finding cut formulas often requires heuristics. However, the cut-elimination property does not hold in some cyclic-proof systems, such as the sequent calculus for first-order logic and the entailment system for symbolic-heap separation logic. This paper proves that the cyclic-proof system for the logic of bunched implications does not satisfy the cut-elimination property, even if the system is restricted to the positive fragment with inductively defined propositions. To prove this, we use a new proof technique called proof unrolling. To demonstrate that proof unrolling is a general technique, this paper adapts proof unrolling to another cyclic-proof system for multiplicative additive linear logic with fixed-point operators.