Isn totally automated theorem proving infeasible?
For the foreseeable future theorem provers will require human interaction to guide the search for non-trivial proofs. Fortunately, proof planning is also useful in interactive theorem provers. Proof plans facilitate the hierarchical organisation of a partial proof, assisting the user to navigate around it and understand its structure. They also provide a language for chunking the proof and for describing the interrelation between the chunks. Interaction with a semi-automated theorem prover can be based on this language. For instance, the user can: ask why a proof method failed to apply; demand that a heuristic precondition is overridden; use the analysis from proof critics to patch a proof; etc. The XBarnacle system is an semi-automated theorem prover based on proof planning. An introductory paper is: Lowe, H. and Duncan, D. XBarnacle: Making theorem provers more accessible Proceedings of CADE-14, McCune, W., Springer-Verlag LNAI 1249, pp 404-408, 1997.
