Research Paper #592
|The Use of Planning Critics in Mechanizing Inductive Proofs
|Published in International Conference on Logic Programming and Automated Reasoning - LPAR 92, St. Petersburg, Ed. A Voronkov. Lecture Notes in Artificial Intell
|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.
|NO ONLINE COPY