Planning Mathematical Proofs with Methods

Xiaorong HuangXiaorong Huang, Manfred KerberManfred Kerber, Jörn RichtsJörn Richts, Arthur SehnArthur Sehn

Xiaorong Huang, Manfred Kerber, Jörn Richts, Arthur Sehn
Planning Mathematical Proofs with Methods
Journal of Information Processing and Cybernetics, EIK, 30(5-6):277-291, 1994

Details
Bibtex

KurzfassungAbstract
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 situations is a fundamental part of human mathematical competence. We believe it is extremely valuable to account computationally for this kind of reasoning. The main part of this article 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 illustrate the mechanical modification of declaratively encoded methods by so-called meta-methods.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ HuangKerber+-EIK-94,
  author = {Xiaorong {Huang} and Manfred {Kerber} and J{\"o}rn {Richts} and Arthur {Sehn}},
  journal = {Journal of Information Processing and Cybernetics, EIK},
  number = {5-6},
  pages = {277--291},
  title = {Planning Mathematical Proofs with Methods},
  volume = {30},
  year = {1994},
}