Reasoning theories. Toward an architecture for open mechanized reasoning systems (Q5931115)

The paper presents the development of a general framework for specifying, structuring and interoperating provers. The authors focus their attention on the formalization of the architectural and implementational choices that underlie the construction of such provers. They call the resulting provers OMRS (Open Mechanized Reasoning Systems). From a theoretical point of view the authors see at least three applications of the presented framework: An OMRS specification can be used to develop provers whose implementation is provable correct under certain weak hypotheses. An OMRS specification can be used to synthesize a prover. An OMRS specification can be used to integrate existing provers. The authors specify the architecture of OMRS as follows. OMRS = Reasoning System + Interaction. Reasoning System = Reasoning Theory + Control. Reasoning Theory = Sequent System + Rules. The first goal in this paper is to introduce the main intuitions underlying the OMRS framework. The main focus is on its use in the integration of provers. The second goal is the development of the basic notions concerning reasoning theories: sequent system rules, reasoning theory. The authors propose a set of primitive operations and show that they generate all and only the possible reasoning structures. They show how these primitive operations can be used to define various directional modes of rule application. The related and future work are discussed.