de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

A recursion planning analysis of inductive completion

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

MPI-I-92-230.pdf
(Any fulltext), 126KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Barnett, R., Basin, D. A., & Hesketh, J.(1992). A recursion planning analysis of inductive completion (MPI-I-92-230). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B1E2-2
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.