The use of proof planning for co-operative theorem proving

We describe BARNACLE: a co-operative interface to the CLAM inductive theorem proving system. For the foreseeable future, there will be theorems which cannot be proved completely automatically, so the ability to allow human intervention is desirable; for this intervention to be productive the problem of orienting the user in the proof attempt must be overcome. There are many semi-automatic theorem provers: we call our style of theorem proving co-operative, in that the skills of both human and automaton are used each to their best advantage, and used together may find a proof where other methods fail. The co-operative nature of the BARNACLE interface is made possible by the proof planning technique underpinning CLAM. Our claim is that proof planning makes new kinds of user interaction possible. Proof planning is a technique for guiding the search for a proof in automatic theorem proving. Common patterns of reasoning in proofs are identified and represented computationally as proof plans, which can then be used to guide the search for proofs of new conjectures. We have harnessed the explanatory power of proof planning to enable the user to understand where the automatic prover got to and why it is stuck. A user can analyse the failed proof in terms of CLAM'S specification language, and hence override the prover to force or prevent the application of a tactic, or discover a proof patch. This patch might be to apply further rules or tactics to bridge the gap between the effects of previous tactics and the preconditions needed by a currently inapplicable tactic. (C) 1998 Academic Press Limited.