Combining superposition and induction: a practical realization

DOI10.1007/978-3-642-40885-4_2MaRDI QIDQ2849478zbMATH OpenOpenAlexFDO

Authors Abdelkader Kersani, Nicolas Peltier

Publication date 20 September 2013

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-40885-4_2

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Superposition modulo linear arithmetic SUP(LA)
• Combining induction and saturation-based theorem proving
• A superposition oriented theorem prover
• Superposition with structural induction

Cited in

(15)

• Superposition with structural induction
• Unprovability results for clause set cycles
• Induction and Skolemization in saturation theorem proving
• Combining induction and saturation-based theorem proving
• Induction in saturation-based proof search
• A decision procedure for (co)datatypes in SMT solvers
• A decision procedure for (co)datatypes in SMT solvers
• Completeness and decidability results for first-order clauses with indices
• Implementing Superposition in iProver (System Description)
• Clause set cycles and induction
• Getting saturated with induction
• Quantifier-free induction for lists
• Automating induction by reflection
• Rewriting and inductive reasoning
• Symbol elimination and applications to parametric entailment problems

Describes a project that uses

Uses Software

• SPIKE

This page was built for publication: Combining superposition and induction: a practical realization

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