Cyclic proofs, hypersequents, and transitive closure logic

DOI10.1007/978-3-031-10769-6_30MaRDI QIDQ2104539zbMATH OpenOpenAlexFDO

Authors Anupam Das, Marianna Girlando

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

cyclic proofshypersequentspropositional dynamic logictransitive closure logic

Mathematics Subject Classification ID

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

Cites work

• A cut-free cyclic proof system for Kleene algebra
• 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
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Complete systems of \(\mathcal B\)-rational identities
• Focused labeled proof systems for modal logic
• Games for the -calculus
• Handbook of modal logic
• scientific article; zbMATH DE number 408795 (Why is no real title available?)
• scientific article; zbMATH DE number 6863660 (Why is no real title available?)
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Infinitary proof theory: the multiplicative additive case
• Integrating induction and coinduction via closure operators and proof cycles
• Languages that Capture Complexity Classes
• Modal logic
• Non-well-founded proof theory of transitive closure logic
• On the proof theory of the modal mu-calculus
• Sequent calculi for induction and infinite descent
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Cited in

(6)

• Cyclic proofs with ordering constraints
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Cyclic hypersequent system for transitive closure logic
• Abstract cyclic proofs
• A proof theory of ( -)context-free languages, via non-wellfounded proofs
• A complete propositional dynamic logic for regular expressions with lookahead

Describes a project that uses

Uses Software

• Cyclist

This page was built for publication: Cyclic proofs, hypersequents, and transitive closure logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104539)