Mapping OMRS to Rewriting Logic

AbstractThe long-term objective of the Open Mechanized Reasoning Systems (OMRS) project is to provide a framework for specifying and structuring reasoning systems, and a technology for integrating and interoperating diverse proof systems with each other and with other software components. We structure an OMRS in three layers: the deductive machinery; strategies for controlling inference; and interaction capabilities. The underlying deduction machinery of an OMRS is described by a reasoning theory which provides a sequent system, a set of rules and an operational model given by an associated algebra of derivation structures. There is an obvious analogy between reasoning theories and rewriting logic theories. Namely, a sequent system in its simplest form corresponds to the equational part of a rewriting logic theory, reasoning theory rules correspond to the rule part of a rewriting logic theory, and the algebra of derivation structure corresponds to the proof term model of rewriting logic. The objective of this paper is to make this correspondence more precise, and to indicate how the correspondence might be used in different ways to enrich both the OMRS world and the rewriting logic world