Planning Mathematical Proofs with Methods

Abstract

In this report we formally describe a declarative approach for encoding plan operators in proof planning, the so-called methods. The notion of method evolves from the much studied concept tactic and was first used by A. Bundy. Significant deductive power has been achieved with the planning approach towards automated deduction, however, the procedural character of the tactic part of methods hinders mechanical modification. Although the strength of a proof planning system largely depends on powerful general procedures which solve a large class of problems, mechanical or even automated modification of methods is nevertheless necessary for at least two reasons. Firstly methods designed for a specific type of problems will never be general enough. For instance, it is very difficult to encode a general method which solves all problems a human mathematician might intuitively consider as a case of homomorphy. Secondly the cognitive ability of adapting existing methods to suit novel situations is a fundamental part of human mathematical competence. We believe it is extremely valuable to computationally account for this kind of reasoning. The main part of this report is devoted to a declarative language for encoding methods, composed of a tactic and a specification. The major feature of our approach is that the tactic part of a method is split into a declarative and a procedural part in order to enable a tractable adaption of methods. The applicability of a method in a planning situation is formulated in the specification, essentially consisting of an object level formula schema and a meta-level formula of a declarative constraint language. After setting up our general framework, we mainly concentrate on this constraint language. Furthermore we illustrate how our methods can be used in a STRIPS-like planning framework. Finally we briefly show the mechanical modification of declaratively encoded methods. An annotated runtime protocol of an example can be found in the appendix.