Cyclic proofs, hypersequents, and transitive closure logic

DOI10.1007/978-3-031-10769-6_30OpenAlexW4289104024MaRDI QIDQ2104539

Marianna Girlando, Anupam Das

Publication date: 7 December 2022

Full work available at URL: https://arxiv.org/abs/2205.08616

zbMATH Keywords

propositional dynamic logichypersequentstransitive closure logiccyclic proofs

Mathematics Subject Classification ID

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

Related Items (1)

Cyclic hypersequent system for transitive closure logic

Uses Software

• Cyclist

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
• 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
• 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 proofs, hypersequents, and transitive closure logic