Theory reasoning in connection calculi (Q1276499): Difference between revisions

The general motivation for Baumgartner's book is the goal to construct an efficient reasoning system for first-order logic. The used technique is called theory reasoning -- an incorporation of specialized and efficient modules (theories) for handling special problem domains. Let us motivate the technique by an example: In a theorem prover supporting theory reasoning the traditional question whether \(F \models \phi\) holds is viewed as follows. The set of formulae \(F\) is partitioned into \({\mathcal T} \cup F_{\phi}\), where \(\mathcal T\) is a theory handled by a specialized reasoner \(\vdash_{\mathcal T}\) (background reasoner). Answer to the question is computed by a combination of a universal reasoner \(\vdash\) (foreground reasoner) and the specialized background reasoner. The original question can be transformed into \(F_{\phi} \vdash_{\vdash_{\mathcal T}} \phi\). Connection calculi are used as foreground (universal) reasoners. Several theory-reasoning versions of connection calculi are defined and related to each other. Theory model elimination was selected as the primary calculus of interest. The text is self-contained. The necessary logical background is presented in the book. Subsequently, connection calculi, model elimination, and their theory-reasoning versions are discussed. Model elimination is considered for further refinements. Interfacing the foreground reasoner to the background reasoner is an important aspect of theory reasoning. One variant of the coupling is called total theory reasoning. The background reasoner can be thought of as a black box which satisfies some semantic properties. The properties are defined in such a way that an answer completeness result for the combined calculus holds. Partial theory reasoning requires a tighter and symmetric coupling of the two reasoners. A syntactic framework, called theory inference rules, is proposed. It can be seen as a specification language for permissible partial theory inferences. A general completeness criterion for background reasoners following this schema is defined, and the resulting calculus is proven as answer-complete. A variant of model elimination -- restart model elimination is discussed. In order to make the framework applicable in practice, the background theory has to be instantiated with a set of theory inference rules satisfying the completeness criterion. A compilation technique, called linearizing completion, which fills this gap, was proposed. The technique is compatible with model elimination. Linearizing completion can be used also as a stand-alone computation technique for Horn theories. The framework partial theory model elimination plus linearizing completion was implemented. The results of experiments show that the suggested methodology significantly improves the power of model-elimination based theorem proving.