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
|