Knowledge-based proof planning

摘要

Knowledge-based proof planning is a new paradigm in automated theorem proving (ATP) which swings the motivational pendulum back to its AI origins in that it employs and further develops many AI principles and techniques such as hierarchical planning, knowledge representation in frames and control-rules, constraint solving, tactical and meta-level reasoning. It differs from traditional search-based techniques in ATP not least with respect to its level of abstraction: the proof of a theorem is planned at an abstract level and an outline of the proof is found. This outline, i.e., the abstract proof plan, can be recursively expanded and it will thus construct a proof within a logical calculus. The plan operators represent mathematical techniques familiar to a working mathematician. While the knowledge of a domain is specific to the mathematical field, the representational techniques and reasoning procedures are general-purpose. The general-purpose planner makes use of this mathematical domain knowledge and of the guidance provided by declaratively represented control-rules which correspond to mathematical intuition about how to prove a theorem in a particular situation. These rules provide a basis for meta-level reasoning and goal-directed behaviour. We demonstrate our approach for the mathematical domain of limit theorems, which was proposed as a challenge to automated theorem proving by the late Woody Bledsoe. Using the proof planner of the Ωmega system we were able to solve all the well known challenge theorems including those that cannot be solved by any of the existing traditional systems.