Productive use of failure

Success in the search for a mathematical proof typically involves the analysis of failed proof attempts. It is this analysis, coupled with a strong expectation as to how a proof should proceed, which often holds the key to success. A proof plan [1] makes such ``expectations'' explicit by providing a representation of the common structure which defines a family of proofs. This common structure can be used to automate the search for particular proofs. Proof critics [2] are an extension to proof plans which automate proof patching through the analysis of failed proof attempts. The mechanism has been applied very successfully within the domain of mathematical induction [3,4,5] where many eureka steps, e.g. missing lemmas and generalizations, have been discovered automatically.

As currently implemented, proof critics perform a rather static form of failure analysis. That is, critics search for particular patterns of plan failure which are constructed off-line. We are now investigating a more dynamic form of failure analysis which will make use of meta-level reasoning.