Publication
Failure Reasoning in Multiple-Strategy Proof Planning
Andreas Meier; Erica Melis
In: M.P. Bonacina; T. Boy de la Tour (Hrsg.). Proceedings of Workshop ``Strategies in Automated Deduction'' at the Second International Joint Conference on Automated Reasoning (IJCAR2004). International Joint Conference on Automated Reasoning (IJCAR), Cork, Pages 93-105, 7/2004.
Abstract
The control in multi-strategy proof planning goes beyond the control in other automated theorem proving approaches: not only the selection of the inference and the facts for the next step can be guided by domain-specific heuristics but also the combination of proof plan refinements such as step introduction, backtracking, and variable instantiation. This enables a dynamic traversal of the search space and a dynamic construction of the proof plan guided by mathematically motivated heuristics. This paper discusses how proof planning with multiple strategies exploits failures to guide the subsequent proof plan manipulations and refinements.