MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


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.pdfMPI-I-92-230.pdfMPI-I-92-230.dvi
  • Attachement: MPI-I-92-230.dvi (72 KBytes); MPI-I-92-230.pdf (126 KBytes)

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},