MPI-I-92-230
A recursion planning analysis of inductive completion
Barnett, Richard and Basin, David A. and Hesketh, Jane
July 1992, 14 pages.
.
Status: available - back from printing
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.
-
MPI-I-92-230.pdf
- Attachement: MPI-I-92-230.dvi (72 KBytes); MPI-I-92-230.pdf (126 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-230
BibTeX
@TECHREPORT{BarnettBasinHesketh92,
AUTHOR = {Barnett, Richard and Basin, David A. and Hesketh, Jane},
TITLE = {A recursion planning analysis of inductive completion},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-92-230},
MONTH = {July},
YEAR = {1992},
ISSN = {0946-011X},
}