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 |
| Keywords: | |
| 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. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}