We propose a new approach to automated tactical theorem proving and proof planning which has the following advantages: By using meta-rules to control the search for a proof, heuristic knowledge is declaratively collected. This eases the user's understanding of the system's search for a proof thus making user-interactions easier. The system's heuristics can be modified by simply using different sets of meta-rules. Via meta-rules contextual preconditions for tactics can be formulated in a transparent way. Furthermore, subproofs can be reused.
The meta-rule interpreter interleaves proof planning, plan execution (tactic application), and reasoning about the tactic's results. Thus many problems concerning the failure of tactics to achieve the desired results become obsolete. In our framework the planner has access to more information, because the meta-rule interpreter knows about the history of the proof resp. the proof plan by being able to access the (partial) proof-tree. This leads to more sophisticated plans.
Proof Planning, Deduction, Tactical Theorem Proving