Proof planning was introduced by Alan Bundy for inductive theorem proving (see) and realized in the proof planner Clam. It employs a search heuristic, called rippling. This heuristic works in particular for equational proofs and proofs by mathematical induction. However, there are many theorems that are difficult or impossible to prove by Clam. Therefore, we extended the proof planning paradigm to knowledge-based proof planning.
In knowledge-based proof planning the plan operators represent general or domain-specific 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. Knowledge-based proof planning provides a basis for systems that truly assist mathematicians and students. Because a proof plan is an abstract representations of a proof it provides an adequate level for communicating with the user.
OMEGA's proof planner constructs a proof plan for a goal node from a set of supporting nodes (the initial state) using a set of proof planning operators, called methods. These methods represent mathematically meaningful proof steps. Technically, a method is a frame-like data structure that has a declarative specification in a meta-level language. Currently, OMEGA's planner combines forward and backward state-space search with hierarchical expansion of non-primitive methods and precondition abstraction.
OMEGA incorporates the plans found by the planning procedure into the Proof Plan Data Structure (PDS) as depicted in the above figure that contains all the plans at all levels of expansion. In the PDS the reasons for the planning decisions and failed proof attempts are also stored for later use in meta-reasoning, proof explanation, and analogy-driven proof plan construction.
The actual reasoning competence of OMEGA's planner builds upon the availability of appropriate methods together with the control knowledge represented by control-rules that guides the planning. OMEGA can also use analogy as a control strategy of the planner. The planner's competence has been improved by extending the domain knowledg theory-specific external systems such as constraint solvers that help to restrict the search.
In order to make proof planning more robust and flexible we extended the proof
planning paradigm of OMEGA to multi-strategy proof planning. The key
idea of multi-strategy proof planning is to combine proof planning with other
algorithms also refining or modifying partial proof plans such as case-based
planning, call of traditional automated theorem provers, expansion of complex
steps, and instantiation of meta-variables. In addition, the behavior of these
algorithms can be influenced by different parameter settings. Each different
instantiation of an algorithm by different parameters is a strategy.
Different strategies are not just tried one after another, rather we can
switch - guided by strategic meta-reasoning - flexibly between strategies to
tackle different subproblems with different strategies.