2001: ’A critique of proof planning

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. Preamble This paper consists of two parts: 1. a brief ‘bluffer’s guide ’ to proof planning1; and 2. a critique of proof planning organised as a 4x3 array. Those already familiar with proof planning may want to skip straight to the critique which starts at §2, p4.