Theorem proving with built-in hybrid theories

Abstract

A growing number of applications of automated reasoning exhibits the necessity of flexible deduction systems. A deduction system should be able to execute inference rules which are appropriate to the given problem. One way to achieve this behavior is the integration of different calculi. This led to so called hybrid reasoning [22, 1, 10, 20] which means the integration of a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purpose inference rules according to a built-in theory. The aim of this paper is to go a step further, i.e. to treat the background reasoner as a hybrid system itself. The paper formulates sufficient criteria for the construction of complete calculi which enable reasoning under hybrid theories combined from sub-theories. For this purpose we use a generic approach described in [20]. This more detailed view on built-in theories is not covered by the known general approaches [1, 3, 6, 20] for building in theories into theorem provers. The approach is demonstrated by its application to the target calculi of the algebraic translation [9] of multi-modal and extended multi-modal [7] logic to first-order logic.