Adaptation of declaratively represented methods in proof planning

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 apparently the 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. The examples should illustrate our philosophy of proof planning as well: Besides planning with the current repertoire of methods, the repertoire of methods evolves with experience in that new ones are created by meta-methods which modify existing ones. (orig.)SIGLEAvailable from TIB Hannover: RO 7629(95-12) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekDEGerman