We are interested in developing a methodology for integrating mechanized reasoning systems such as Theorem Provers, Computer Algebra Systems, and Model Checkers. Our approach is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchiglia et al. (1994) 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. We 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 constraint co∼textual rewriting as a set of cooperating specialized reasoning modules. © 2001 Academic Press.

The control layer in Open Mechanized Reasoning Systems: Annotations and tactics / Armando, A.; Coglio, A.; Giunchiglia, F.; Ranise, S.. - In: JOURNAL OF SYMBOLIC COMPUTATION. - ISSN 0747-7171. - 32:4(2001), pp. 305-332. [10.1006/jsco.2000.0464]

The control layer in Open Mechanized Reasoning Systems: Annotations and tactics

Giunchiglia F.;Ranise S.
2001-01-01

Abstract

We are interested in developing a methodology for integrating mechanized reasoning systems such as Theorem Provers, Computer Algebra Systems, and Model Checkers. Our approach is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchiglia et al. (1994) 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. We 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 constraint co∼textual rewriting as a set of cooperating specialized reasoning modules. © 2001 Academic Press.
2001
4
Armando, A.; Coglio, A.; Giunchiglia, F.; Ranise, S.
The control layer in Open Mechanized Reasoning Systems: Annotations and tactics / Armando, A.; Coglio, A.; Giunchiglia, F.; Ranise, S.. - In: JOURNAL OF SYMBOLIC COMPUTATION. - ISSN 0747-7171. - 32:4(2001), pp. 305-332. [10.1006/jsco.2000.0464]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333260
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
  • OpenAlex ND
social impact