The automation of proof by mathematical induction (Q2751365)

This chapter surveys the automation of theorem proving using induction rules. Specifically, it is concerned with `explicit' induction, in which induction rules are explicitly incorporated into proofs. `Implicit' induction, or `inductionless induction' is dealt with in another Chapter of the Handbook [\textit{H. Comon}, ``Inductionless induction'', ibid., 913-960 (2001; Zbl 0994.03006)], reviewed below. Recursion is frequently used in the construction of classes of objects and in the definition of functions and programs; induction is needed to reason about, for instance, recursive datatypes and recursive definitions. The automation of induction is necessary for applications such as proving statements about formal methods of system development. Apart from showing the application of induction rules, emphasis is put on some proof techniques used in inductive proofs which are related to rewriting (such as fertilization or destructor elimination), and its termination properties. Later, theoretical limitations arising from results by Gödel and Kreisel are recalled, in the form of the incompleteness of inductive inference and the failure of cut elimination for inductive theories. Later, special search control techniques to solve problems related to the introduction of infinite branch points into the search space are presented. The search control problems of induction rule choice, lemma introduction and generalisation are presented. Then, rippling is introduced as a partial solution to many of the special problems described previously; among the advantages of rippling we have that it is more restrictive than conventional rewriting (reducing the search space), it always terminates, it allows rewriting in both directions, and it supports several heuristics. A section is devoted to the study of conjectures which include existential variables. This raises the need of extending some of techniques previously introduced. The final section presents some of the problems and solutions found in the development of interactive explicitly inductive theorem provers.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].