Clause set cycles and induction

MaRDI QIDQ5140266zbMATH OpenFDO

Authors Stefan Hetzl, Jannik Vierling

Publication date 15 December 2020

Full work available at URL https://arxiv.org/abs/1910.03917, https://lmcs.episciences.org/6932

zbMATH Keywords

arithmetical theoriesclause logiccyclic proofsinductive theorem proving

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Inductionless induction
• The automation of proof by mathematical induction
• Combining induction and saturation-based theorem proving
• Completeness and decidability results for first-order clauses with indices
• Combining superposition and induction: a practical realization

Cites work

• Automating Inductive Proofs Using Theory Exploration
• Combining induction and saturation-based theorem proving
• Combining superposition and induction: a practical realization
• scientific article; zbMATH DE number 1144041 (Why is no real title available?)
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Open sentences and the induction axiom
• Paramodulation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Sequent calculi for induction and infinite descent
• Some observations on the logical foundations of inductive theorem proving
• Superposition with structural induction

Cited in

(4)

• Unprovability results for clause set cycles
• Induction and Skolemization in saturation theorem proving
• Clause Set Cycles and Induction
• Quantifier-free induction for lists

Describes a project that uses

Uses Software

• HipSpec
• Cyclist

This page was built for publication: Clause set cycles and induction

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