The control layer in open mechanized reasoning systems: Annotations and tactics

We are interested in developing a methodology for integrating mechanized re asoning systems such as Theorem Provers, Computer Algebra Systems, and Mode l Checkers. Our approach is to provide a framework for specifying mechanize d reasoning systems and to use specifications as a starting point for integ ration. We build on the work presented by Giunchiglia et al. (1994) which i ntroduces the notion of Open Mechanized Reasoning Systems (OMRS) as a speci fication framework for integrating reasoning systems. An OMRS. specificatio n 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 knowl edge to the data structures representing the logic by means of annotations and then by specifying proof strategies via tactics. To show the adequacy o f the approach we present and discuss a structured specification of constra int contextual rewriting as a set of cooperating specialized reasoning modu les. (C) 2001 Academic Press.