Using theorem provers for PL1EQ as inductive provers

Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern,
Postfach 3049, W-6750 Kaiserslautern, GERMANY
E-mail: fuchs@informatik.uni-kl.de

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 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 lemmata 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.)

Keywords

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1993/papers/
file: Fuchs.SR-93-01.ps.SEKI.Z