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

DOI10.29007/XGC6zbMATH Open1416.03027OpenAlexW2907543096MaRDI QIDQ5222971FDOQ5222971

C. Şerban, Radu Iosif

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

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

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)

Cited In (3)

• 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

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)