Report Number: CS-TN-94-15
Institution: Stanford University, Department of Computer Science
Title: Reasoning Theories: Towards an Architecture for Open
Mechanized Reasoning Systems
Author: Giunchiglia, Fausto
Author: Pecchiari, Paolo
Author: Talcott, Carolyn
Date: December 1994
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.
http://i.stanford.edu/pub/cstr/reports/cs/tn/94/15/CS-TN-94-15.pdf