We are interested in integrating mechanized reasoning systems such as, e.g., Theorem Provers and Computer Algebra Systems. Our approach to the problem is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on top of the work presented in [9] which introduces the notion of Open Mechanized Reasoning Systems (OMRS) as a specification framework for integrating reasoning systems. An OMRS specification consists of three components: the logic component, the control component, and the interaction component. In this paper we focus on the control level and propose to specify the control component by first adding control knowledge to the data structures representing the logic by means of annotations, and then by specifying proof strategies via tactics. To show the adequacy of the approach we present and discuss a structured specification of the top-level inference strategy of NQTHM as a set of cooperating specialized reasoning modules
The Control Component of Open Mechanized Reasoning Systems
Armando, Alessandro;Giunchiglia, Fausto
1999-01-01
Abstract
We are interested in integrating mechanized reasoning systems such as, e.g., Theorem Provers and Computer Algebra Systems. Our approach to the problem is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on top of the work presented in [9] which introduces the notion of Open Mechanized Reasoning Systems (OMRS) as a specification framework for integrating reasoning systems. An OMRS specification consists of three components: the logic component, the control component, and the interaction component. In this paper we focus on the control level and propose to specify the control component by first adding control knowledge to the data structures representing the logic by means of annotations, and then by specifying proof strategies via tactics. To show the adequacy of the approach we present and discuss a structured specification of the top-level inference strategy of NQTHM as a set of cooperating specialized reasoning modulesI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
