Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Anupam Das, Marianna Girlando · Lecture notes in computer science · 2022
Abstract We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic ( $$\mathrm {PDL}$$ PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and $$\mathrm {PDL}$$ PDL , thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.