Cyclic proofs with ordering constraints

DOI10.1007/978-3-319-66902-1_19MaRDI QIDQ1694475zbMATH OpenOpenAlexFDO

Authors Sorin Stratulat

Publication date 2 February 2018

Full work available at URL https://doi.org/10.1007/978-3-319-66902-1_19

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Abstract cyclic proofs
• Theorem proving with ordering and equality constrained clauses
• Cyclic ordering through partial orders
• Automated Reasoning with Analytic Tableaux and Related Methods
• Realizability in cyclic proof: extracting ordering information for infinite descent
• Cyclic proofs, hypersequents, and transitive closure logic
• scientific article; zbMATH DE number 1182797
• Orderings and Constraints: Theory and Practice of Proving Termination
• On the Logical Strength of Confluence and Normalisation for Cyclic Proofs.

Cited in

(8)

• Cyclic ordering is NP-complete
• Realizability in cyclic proof: extracting ordering information for infinite descent
• Validating back-links of \(\mathrm{FOL_{ID}}\) cyclic pre-proofs
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• A complete cyclic proof system for inductive entailments in first order logic
• Classical system of Martin-Löf's inductive definitions is not equivalent to cyclic proofs
• Automated Reasoning with Analytic Tableaux and Related Methods
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs

This page was built for publication: Cyclic proofs with ordering constraints

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