Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #592 | |
|---|---|
| Title: | The Use of Planning Critics in Mechanizing Inductive Proofs |
| Authors: | Ireland,A |
| Date: | 1992 |
| Presented: | Published in International Conference on Logic Programming and Automated Reasoning - LPAR 92, St. Petersburg, Ed. A Voronkov. Lecture Notes in Artificial Intell |
| Keywords: | |
| Abstract: | Proof plans provide a technique for guiding the search for a proof in the context of tactical style reasoning. We propose an extension to this technique in which failure may be exploited in the search for a proof. This extension is based upon the concept of planning critics. In particular we illustrate how proof critics may be used to patch proof plans in the domain of inductive proofs. |
| 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}