Publikation
Proof Planning with Multiple Strategies
Erica Melis; Andreas Meier; Jörg Siekmann
In: Artificial Intelligence (AIJ), Pages 656-684, Elesevier, 2008.
Zusammenfassung
Proof planning is a technique for theorem proving which replaces the ultra-efficient but blind search of classical theorem proving systems by an informed knowledge-based planning process that employs mathematical knowledge at a human-oriented level of abstraction. Standard proof planning uses em methods as operators and em control rules to find an abstract proof plan which can be expanded (using em tactics) down to the level of the underlying logic calculus. In this paper, we propose more flexible refinements and a modification of the proof planner with an additional strategic level of control above the previous proof planning control. This em strategic control guides the cooperation of the problem solving strategies by meta-reasoning. We present a general framework for proof planning with multiple strategies and describe its implementation in the MULTI system. The benefits are illustrated by several large case studies, which significantly push the limits of what can be achieved by a machine today.