Cyclic proofs, hypersequents, and transitive closure logic

DOI10.1007/978-3-031-10769-6_30MaRDI 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 logic; hypersequents; transitive closure logic; cyclic proofs

Mathematics Subject Classification ID

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

Related Items

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