de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

A recursion planning analysis of inductive completion

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

MPI-I-92-230.pdf
(beliebiger Volltext), 126KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


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