Cyclic hypersequent system for transitive closure logic

DOI10.1007/s10817-023-09675-1OpenAlexW4385876474MaRDI QIDQ6050767

Marianna Girlando, Anupam Das

Publication date: 19 September 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-023-09675-1

zbMATH Keywords

proof theorypropositional dynamic logichypersequentstransitive closure logiccyclic proofs

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Games for the \(\mu\)-calculus
• On the proof theory of the modal mu-calculus
• Complete systems of \(\mathcal B\)-rational identities
• A cut-free cyclic proof system for Kleene algebra
• Integrating induction and coinduction via closure operators and proof cycles
• Cyclic proofs, hypersequents, and transitive closure logic
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Sequent calculi for induction and infinite descent
• Focused Labeled Proof Systems for Modal Logic
• Languages that Capture Complexity Classes
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Non-well-founded Proof Theory of Transitive Closure Logic
• Automated Cyclic Entailment Proofs in Separation Logic
• A Proof System for the Linear Time μ-Calculus
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Automatically verifying temporal properties of pointer programs with cyclic proof

This page was built for publication: Cyclic hypersequent system for transitive closure logic