Using theorem provers for PL1EQ as inductive provers

Abstract

This report presents a method to create an inductive proof system by using a theorem prover for PL1EQ (first order logic with equality) as a basic system. This method not only comprises the general principles necessary for making a theorem prover for PL1EQ capable of performing inductive proofs, but also includes further features that may be added to systems for inductive proofs in order to guide the individual proof (for instance heuristics aimed at optimizing the application of the inference rules with respect to the fact that a proof by induction is to be found). An emphasis lies on the automatic generation of inductive Iemmata which are crucial to the success of inductive proofs. In this domain a range of heuristics were conceived, partly as derivations of ideas of other authors, partly as own developments, which in many cases can generate a lemma that ends the proof attempt successfully. (This includes that this lemma itself can be proved by induction as well.)