Success in the search for a 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 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 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 where many eureka steps, e.g. missing lemmas and generalizations, have been discovered automatically.
More recently we have been investigating proof plans for reasoning about the behaviour of imperative programs. In particular we have focussed on the search control issues associated with the discovery and verification of loop invariants. In terms of formal reasoning the discovery of a loop invariant is typically seen as a eureka step. The strong connection between iteration and recursion has enabled us to transfer proof plans and critics designed for reasoning about functional programs into this new domain with some promising results.
My talk will provide an overview to proof plans with particular emphasis on the critics mechanism. I will argue for the merits of proof plans as a basis for developing flexible and robust automatic theorem provers.