Inductionless induction (Q2751366)

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].