BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TN-94-15
       ENTRY:: December 08, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Reasoning Theories: Towards an Architecture for Open
               Mechanized Reasoning Systems
        TYPE:: Technical Note
      AUTHOR:: Giunchiglia, Fausto
      AUTHOR:: Pecchiari, Paolo
      AUTHOR:: Talcott, Carolyn
        DATE:: December 1994
       PAGES:: 60
    ABSTRACT:: Our ultimate goal is to provide a framework and a methodology
               which will allow users, and not only system developers, to
               construct complex reasoning systems by composing existing
               modules, or to add new modules to existing systems, in a
               ``plug and play'' manner. These modules and systems might be
               based on different logics; have different domain models; use
               different vocabularies and data structures; use different
               reasoning strategies; and have different interaction
               capabilities. This paper makes two main contributions towards
               our goal. First, it proposes a general architecture for a
               class of reasoning modules and systems called Open Mechanized
               Reasoning Systems (OMRSs). An OMRS has three components: a
               reasoning theory component which is the counterpart of the
               logical notion of formal system, a control component which
               consists of a set of inference strategies, and an interaction
               component which provides an OMRS with the capability of
               interacting with other systems, including OMRSs and human
               users. Second, it develops the theory underlying the
               reasoning theory component. This development is motivated by
               an analysis of state of the art systems. The resulting theory
               is then validated by using it to describe the integration of
               the linear arithmetic module into the simplification process
               of the Boyer-Moore system, NQTHM.
       NOTES:: [Adminitrivia V1/Prg/19941208]
         END:: STAN//CS-TN-94-15