Cyclic Proofs, Hypersequents, and Transitive Closure Logic

TL;DR

This paper introduces a new cut-free cyclic proof system for Transitive Closure Logic using hypersequents, which improves completeness over previous systems and supports automated reasoning for Kleene Algebra and PDL.

Contribution

The paper presents a novel cyclic proof system for TCL that is complete for KA and PDL, overcoming limitations of earlier sequent systems and incorporating a richer correctness criterion.

Findings

The new system is cut-free and sound for TCL, KA, and PDL.

It faithfully simulates known cyclic systems for KA and PDL.

The system employs a richer correctness criterion with 'alternating traces'.

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 (PDL), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and 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.