What happens if the attempt to find a proof plan fails?
In certain circumstances proof critics can suggest an appropriate patch to a partial proof plan. Suppose the preconditions of a method succeed, but this method is unpacked into a series of sub-methods one of which fails, ie the preconditions of the sub-method fail. Critics are associated with some of these patterns of failure. For instance, one critic may fire if the first two preconditions of a method succeed, but the last one fails. It will then suggest an appropriate patch for this kind of failure, eg suggest the form of a missing lemma, suggest generalising the conjecture. The patch is instituted and proof planning continues. The original critics paper is Ireland, A. The use of planning critics in mechanizing inductive proofs in International Conference on Logic Programming and Automated Reasoning (LPAR 92), St. Petersburg, Lecture Notes in Artificial Intelligence No. 624, ed Voronkov, A., Springer-Verlag”, pp178-189, 1992. A more recent paper is Ireland, A. and Bundy, A., Producti
