Proof planning with multiple strategies

Abstract

Humans have diffierent problem solving strategies at their disposal and they can flexibly employ several strategies when solving a complex problem, whereas previous theorem proving and planning systems typically employ a single strategy or a hard coded combination of a few strategies. We introduce multi-strategy proof planning that allows for combining a number of strategies and for switching flexibly between strategies in a proof planning process. Thereby proof planning becomes more robust since it does not necessarily fail if one problem solving mechanism fails. Rather it can reason about preference of strategies and about failures. Moreover, our strategies provide a means for structuring the vast amount of knowledge such that the planner can cope with the otherwise overwhelming knowledge in mathematics.