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 paper 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-Moore theorem prover
A Logic Level Specification of the NQTHM Simplification Process
Giunchiglia, Fausto;
1997-01-01
Abstract
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 paper 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-Moore theorem proverI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
