Inductionless induction
This chapter surveys theorem proving using minimal Herbrand models without making use of explicit induction rules (also known as `inductionless induction' or `proof by consistency'). The automation of `explicit' induction is dealt with in another Chapter of this Handbook [\textit{A. Bundy}, ``The automation of proof by mathematical induction, ibid., 845-911 (2001; Zbl 0994.03007)]. NEWLINENEWLINENEWLINEThe inductionless induction approach is the basis of several inductive theorem provers; one of its main advantages is the ability to use general purpose first-order theorem provers for inductive theorem proving, without the need of developing dedicated tools. NEWLINENEWLINENEWLINEThe subject of this chapter is to explain how and why this method works: what are the deduction rules used in this context and how can one build an axiomatization which has the desired properties.NEWLINENEWLINENEWLINEAfter introducing the formal background, the general setting of the inductionless induction method is presented. Roughly, the method works as follows: given a set of clauses with equality \(E\), and a set of conjectures \(C\), one studies the union \(E\cup C\) and tries to derive an inconsistency. Then, the deduction engine in the framework of inductive proofs by consistency methods (usually being the Knuth-Bendix completion procedure) is given from a more general point of view: without restriction to the equational case. After recalling the concepts of redundancy and saturation, a general framework of inductive saturation is given, together with a set of deduction rules for inductive completion, which covers some inductive completion methods described in the literature.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- Inductive proof search modulo
- Automatic proofs by induction in theories without constructors
- Induction = I-axiomatization + first-order consistency.
- Sound generalizations in mathematical induction
- Induction and Skolemization in saturation theorem proving
- Combining induction and saturation-based theorem proving
- Induction in saturation-based proof search
- Finite reasons for safety. Parameterized verification by finite model finding
- Herbrand's theorem and term induction
- Schematic cut elimination and the ordered pigeonhole principle
- Inductive prover based on equality saturation for a lazy functional language
- Analysis of the Collision Resistance of RadioGatúnUsing Algebraic Techniques
- scientific article; zbMATH DE number 1324445 (Why is no real title available?)
- Reducing equational theories for the decision of static equivalence
- Proving termination by dependency pairs and inductive theorem proving
- scientific article; zbMATH DE number 2090032 (Why is no real title available?)
- Mechanically certifying formula-based Noetherian induction reasoning
- Clause set cycles and induction
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Induction using term orderings
- Automated Reasoning with Analytic Tableaux and Related Methods
- A tableaux-based decision procedure for multi-parameter propositional schemata
- Proving weak properties of rewriting
- Mechanizing Mathematical Reasoning
- A decidable class of nested iterated schemata
- Perfect discrimination graphs: indexing terms with integer exponents
- An algebraic approach to the equivalence checking of deterministic top-down tree transducers
- A unified view of induction reasoning for first-order logic
- A unifying logical foundation for initial algebra semantics and induction
- Types, Tableaus and Gödel’s God in Isabelle/HOL
This page was built for publication: Inductionless induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751366)
