Projects per year
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.
Original language | English |
---|---|
Article number | 27 |
Number of pages | 40 |
Journal | Journal of Automated Reasoning |
Volume | 67 |
Issue number | 3 |
Early online date | 16 Aug 2023 |
DOIs | |
Publication status | Published - Sept 2023 |
Keywords
- Transitive closure logic
- Proof theory
- Propositional dynamic logic
- Hypersequents
- Cyclic proofs
Fingerprint
Dive into the research topics of 'Cyclic Hypersequent System for Transitive Closure Logic'. Together they form a unique fingerprint.Projects
- 1 Active