Methods : The Basic Units for Planning and Verifying Proofs

Abstract

This paper concerns a knowledge structure called method, within a computational model for human oriented deduction. With human oriented theorem proving cast as an interleaving process of planning and verification, the body of all methods reflects the reasoning repertoire of a reasoning system. While we adopt the general structure of methods introduced by Alan Bundy, we make an essential advancement in that we strictly separate the declarative knowledge from the procedural knowledge. This is achieved by postulating some standard types of knowledge we have identified, such as inference rules, assertions, and proof schemata, together with corresponding knowledge interpreters. Our approach in effect changes the way deductive knowledge is encoded: A new compound declarative knowledge structure, the proof schema, takes the place of complicated procedures for modeling specific proof strategies. This change of paradigm not only leads to representations easier to understand, it also enables us modeling the even more important activity of formulating meta-methods, that is, operators that adapt existing methods to suit novel situations. In this paper, we first introduce briefly the general framework for describing methods. Then we turn to several types of knowledge with their interpreters. Finally, we briefly illustrate some meta-methods.