Failure Reasoning in Multiple-Strategy Proof Planning

Monitoring a solution process and applying the right action at the right moment are at the heart of intelligent problem solving by humans. This includes the analysis of failure events and the development of “recommendations” to overcome typical failures.In this article, we present how meta-reasoning on failures is used in multiple-strategy proof planning with the Multi system. Multi allows for a flexible traversal of the search space and a flexible construction of the proof plan guided by mathematically motivated heuristics. Because of the flexible control in Multi failures can be exploited to guide subsequent proof plan manipulations and refinements. The failure reasoning cannot only ease the derivation of a solution proof plan but is required for some problems to find a solution at all