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

Research Paper #592

Title:The Use of Planning Critics in Mechanizing Inductive Proofs
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
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.

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