Huang, Xiaorong; Kerber, Manfred; Cheikhrouhou, Lassaad Adaptation of declaratively represented methods in proof planning. (English) Zbl 0913.68191 Ann. Math. Artif. Intell. 23, No. 3-4, 299-320 (1998). Summary: The reasoning power of human-oriented plan-based reasoning systems is primarily derived from their domain-specific problem solving knowledge. Such knowledge is, however, intrinsically incomplete. In order to model the human ability of adapting existing methods to new situations we present in this work a declarative approach for representing methods, which can be adapted by so-called meta-methods. Since the computational success of this approach relies on the existence of general and strong meta-methods, we describe several meta-methods of general interest in detail by presenting the problem solving process of two familiar classes of mathematical problems. These examples should illustrate our philosophy of proof planning as well: besides planning with a pre-defined repertory of methods, the repertory of methods evolves with experience in that new ones are created by meta-methods that modify existing ones. MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:plan-based reasoning systems Software:Nuprl PDFBibTeX XMLCite \textit{X. Huang} et al., Ann. Math. Artif. Intell. 23, No. 3--4, 299--320 (1998; Zbl 0913.68191) Full Text: DOI