Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems

Our long-term goal is the development of a general framework for specifying, structuring, and interoperating provers. Our main focus is on the formalization of the architectural and implementational choices that underlie the construction of such systems. This paper has two main goals. The first is to introduce the main intuitions underlying the proposed framework. We concentrate on its use in the integration of provers. The second is the development of the notion of reasoning theory, meant as the formalization of the notion of `implementation of the logic` of a prover. As an example we sketch an analysis, at the reasoning theory level, of the integration of linear arithmetic into the NQTHM simplification proces