AI-Techniques in Proof Planning.
Erica Melis⋆ · 1998
. Proof planning is an application of Artificial Intelligence (AI)-planning in mathematical domains for theorem proving. The paper presents a knowledge-based proof planning approach that is implemented in the OMEGA proof planner. It evaluates control-rules in order to restrict the otherwise intractable search spaces and combines proof planning with domain-specific constraint solving. Several AI-techniques contribute to the successful planning of proofs that were beyond the capabilities of theorem provers and proof planners previously. 1 Introduction Classical logic-based automated theorem provers, such as OTTER [16], have gained considerable strength. They could even prove some non-trivial open mathematical problems such as the Robbins algebra conjecture [15] whose proofs are rather unintuitive and tricky for humans. In general, however, most proofs of genuinely mathematical problems are beyond the capabilities of these theorem provers because traditional automated theorem proving tha...