Modularity in Computer Assisted Reasoning Systems

1 Problem being addressed

An important problem in the domain of automated rea­ soning is the development of mechanisms for the integra­ tion of disparate provers . The components of a prover may be based on different logics, they may have different domain models, they may use different representations of information and reasoning strategies , and they may have different interaction capabilities. The need for compos­ ing complex provers from existing modules, and to add new modules to existing provers is motivated by the de­ sire of not having to build from scratch a new prover for each new problem or variation of an old problem. Multi­ logic provers are needed in many formalization problems, such as hardware and software verification. Multi-logic provers are also needed in complex applications which require embedding of reasoning modules inside other sys­ tems . Some examples are: program transformation sys­ tems , including synthesis ; partial evaluation and com­ piling; planning systems; intelligent agents ; and natural language systems .

2 Thesis objectives

Our ultimate goal is to provide a framework and a methodology which will allow users , and not only devel­ opers , to construct complex re<1-5oning systems by com­ posing existing modules , or to add new modules to ex­ isting systems. These modules and systems might be based on different logics; have different domain models; use different vocabularies and data structures; use dif­ ferent reasoning strategies. The thesis proposal makes two main contributions towards our goal. First, it pro­ poses a formal notation (FB-Hypersequents) for present­ ing the syntax and semantics of reasoning theories of Open Mechanized Reasoning Systems (OMRSs) as stated in [Giunchiglia eta/. , 1994]. Second , it developes the the­ ory underlying the control component - which consists of a set of inference strategies - of OMRSs . This de­ velopment is motivated by an analysis of (logical) conse­ quence relation in general, and especially its possible re­ lations with computational issues. Some of the problems that the thesis proposal addresses are general problem of modularization , composability, and interoperability that are not specific to the domain of automated reasoning. As the ideas and techniques become better developed, we expect that general principles will emerge that can be used in other research areas .

· Also Mechanized Reasoning Group DISA, Universita di Trento, Via lnamaj 1 - 38100 Trento, Italy.

3 Proposed work plan

We are in the middle of a long term project [Giunchiglia et al. , 1994] which still needs to be developed in many directions. The thesis is organized into two main work phases. In the first phase we define the for­ mal framework for representing the syntax and seman­ tics of reasoning theories of OMRSs . In particular , we ( 1) define the language and the central notion of FB-hypersequent, its syntax and semantics; For doing this, we expect to use some previous works on formal bidirectional natural deduction such as [Agostini, 1992; 1993]; (2) extend FB-hypersequents to formalize these­ quent systems inside reasoning theories , and illustrate, with examples, the uniformity of our framework for a di­ versity of logics (reasoning theories); (3) add a semanti­ cal component to our framework and provide for a notion of model for reasoning theories.

In the second phase we study the computational prop­ erties of reasoning theories as formalized in the first phase by FB-hypersequents. These properties provide for the amount of computational information needed by reasoning systems to guide search proof, and in some case to reduce the search space.