@ARTICLE{BarnettBasinHesketh92a,
AUTHOR        = {Richard Barnett and David Basin and Jane Hesketh},
TITLE         = {A Recursion Planning Analysis of Inductive Completion},
YEAR          = 1993,
JOURNAL       = {Annals of Mathematics and Artificial Intelligence},
VOLUME        = {8},
NUMBER        = {3--4},
PAGES         = {363--381},
NOTE          = {Also available as Technical Report MPI-I-92-230},
ABSTRACT      = {
We use the AI proof planning techniques of {\it recursion
analysis} and {\it rippling} as tools to analyze so-called
{\it inductionless induction} proof techniques. Recursion
analysis chooses induction schemas and variables and rippling
controls rewriting in explicit induction proofs. They provide
a basis for explaining the success and failure of inductionless
induction, both in deduction of critical pairs and in their
simplification. Furthermore, these explicit induction techniques
motivate and provide insight into advancements in inductive
completion algorithms and suggest directions for further
improvements. Our study includes an experimental comparison
of Clam, an explicit induction theorem prover, with an implementation
of Huet and Hullot's inductionless induction.},
}