The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #518

Title:A Recursion Planning Analysis of Inductive Completion
Authors:Barnett,R; Basin,D; Hesketh,J
Date: 1991
Presented:Submitted to IJCAI91
Abstract:We use the AI proof planning techniques of recursion analysis and rippling as tools to analyze induction completion or so called inductionless induction proof techniques. Recursion analyses chooses induction schemas and variables and rippling controls post-induction rewriting in explicit induction proofs. The provide a theoretical basis for explaining the success and failure of inductionless induction both in generating conflatable critical pairs (which correspond to induction schemas) and in the simplification of these pairs (which corresponds to post-induction proof). Furthermore, these explicit induction techniques motivate and provide insight into recent improvements in inductive completion algorithms and suggest directions for further improvements. Our study also includes an experimental comparison of Clam, an explicit induction theorem prover, with an implementation of Huet and Hullot's inductionless induction.

[Search These Pages] [DAI Home Page] [Comment]