Lemmae discovery in inductive proof

An inductive proof attempt may fail as the available induction hypotheses cannot be applied to simplify the conclusion. One of the major problems which arise when performing inductive proofs is to transform the conclusion of an inductive step in order to make the hypothesis applicable. Often, to overcome this problem, several additional lemmae are needed. However, most inductive theorem provers rely upon user intervention in supplying the required lemmae. In contrast, we present in this paper a method for automatically generating lemmae, called simplification lemmae. Generation of lemmae is motivated by attempts to find appropriate instantiations of non-induction variables in the inductive step. We consider implicative formulae of the form ∀x~ ∃y~ Γ(x~, y~)⇐Δ(x~), where Γ and Δ are conjunction of atoms, and x~ and y~ are vectors of universal and of existential variables respectively.