Cyclic Hypersequent System for Transitive Closure Logic
Anupam Das, Marianna Girlando · Journal of Automated Reasoning · 2023
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 ( $$\text {PDL}$$ PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and $$\text {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.