Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


A recursion planning analysis of inductive completion

Barnett, Richard and Basin, David A. and Hesketh, Jane

MPI-I-92-230. July 1992, 14 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-230.pdfMPI-I-92-230.pdfMPI-I-92-230.dvi72 KBytes; 126 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  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},