Planning Mathematical Proofs with Methods
Xiaorong Huang, Manfred Kerber, Jörn Richts, Arthur Sehn · 1994
In this article 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 Bundy. While significant deductive power has been achieved with the planning approach towards automated deduction, the procedural character of the tactic part of methods, however, 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 problem 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 situa...