Island Planning and Refinement
Erica Melis⋆ · 1996
Proof planning is an alternative to classical theorem proving. Proof planning is classical planning with no goal interaction. It faces search problems because of long solutions and possibly infinite branching. It is also required to provide plans comprehensible for the user. This article introduces new planning strategies inspired by proof planning examples in order to tackle the search-space-problem and the structured-plan-problem. Island planning and refinement as well as subproblem refinement are integrated into a general planning framework and some exemplary control knowledge suitable for proof planning is given. We think that planning for other realistic problems even in a static and deterministic environment with complete information faces similar problems and can make use of our approach. 1 Introduction Refinement planning as unguided search is notoriously hard because of the combinatorial search involved. For realistic planning problems the intractable search space prevents ma...