[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A Logic Level Specification of the NQTHM Simplification Process
Coglio, A. and Giunchiglia, F. and Pecchiari, P. and Talcott, C. L. - 1997

Our ultimate goal is to provide a framework and a methodology which will allow users to construct and extend complex reasoning systems by composing existing modules in a “plug and play” manner. To this end in a previous we have defined a general architecture for a class of reasoning modules and systems called Open Mechanized Reasoning Systems (OMRSs). An OMRS has three components: a logic component which consists of the assertions manipulated by the OMRS and the elementary deductions upon them; a control component which consists of the inference strategies of the OMRS; an interaction component which provides the OMRS with the capability of interacting with other systems, including OMRSs and human users. We have already developed a theoretical framework underlying the logic component of this architecture. In this paper we show how this formalism can be used in practice to specify the logic component of the simplification process of NQTHM, the Boyer-NMoore prover.

Keywords: reasoning system, OMRS, composing, NQTHM