A complete cyclic proof system for inductive entailments in first order logic

DOI10.29007/XGC6MaRDI QIDQ5222971zbMATH OpenOpenAlexFDO

Authors Radu Iosif, C. Şerban

Publication date 4 July 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/xgc6

zbMATH Keywords

inductive definitionsinfinite descentcyclic proofsantichain-based tree automata language inclusion

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Structure of proofs (03F07)

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• Cyclic proofs with ordering constraints
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Cyclic arithmetic is equivalent to Peano arithmetic
• Formalised Inductive Reasoning in the Logic of Bunched Implications

Cited in

(7)

• Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions
• Cyclic hypersequent system for transitive closure logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Cyclic arithmetic is equivalent to Peano arithmetic
• Cyclic proofs for the first-order \(\mu\)-calculus
• Cyclic proofs for transfinite expressions

This page was built for publication: A complete cyclic proof system for inductive entailments in first order logic

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