A Critique of Proof Planning
Alan Bundy3
| (3) |
Division of Informatics, University of Edinburgh, UK |
Abstract
Proof planning is an approach to the automation of theorem proving in which search is conducted, not at the object-level,
but among a set of proof methods. This approach dramatically reduces the amount of search but at the cost of completeness.
We critically examine proof planning, identifying both its strengths and weaknesses. We use this analysis to explore ways
of enhancing proof planning to overcome its current weaknesses.
The research reported in this paper was supported by EPSRC grant GR/M/45030. I would like to thank Andrew Ireland, Helen Lowe,
Raul Monroy and two anonymous referees for helpful comments on this paper. I would also like to thank other members of the
Mathematical Reasoning Group and the audiences at CIAO and Scottish Theorem Provers for helpful feedback on talks from which
this paper arose.
References secured to subscribers.