Abstract
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 induction 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 a method for generating automatically lemmae. Generation of lemmae is motivated by attempts to find appropriate instantiations for non-induction variables in the inductive step. We consider implicative formulae of the form For All(x) over bar There Exists(y) over bar Gamma((x) over bar,(y) over bar) double left arrow Delta ((x) over bar), where Gamma and Delta are conjunction of atoms and (x) over bar and (y) over bar are vectors of universal a nd of existential variables respectively. (C) 2003 Elsevier Inc. All rights reserved.