Cyclic Proofs, Hypersequents, and Transitive Closure Logic

2022/05/17 by Anupam Das, Das, Anupam, Marianna Girlando +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2205.08616

openalex publication_date 2022/05/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
• A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
• Infinitary and Cyclic Proof Systems for Transitive Closure Logic
• Cyclic Henkin Logic
• Cut elimination for propositional cyclic proof systems with fixed-point operators