Proceedings of the First Working of Abstraction, Analogy and Metareasoning

Our ultimate goal is to define a framework and a methodology which will allow users to construct or extend complex reasoning systems in a "plug and play" manner. Our approach is based on the notion of Open Mechanized Reasoning System (OMRS). 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. In this extended abstract we informally introduce the concept of OMRS and develops the theory underlying the logical component of an OMRS. 1 Introduction An important problem in the domain of automated reasoning is the development of mechanisms for the interoperation and integration of disparate provers. (In the following we use the word "prover" to mean any piece of software with reasoning capabilities, e.g. mechanized ..