Automated deduction scheme

Agostino Dovier, Andrea Formisano, Alberto Policriti

Date: July 17th (Wednesday)
Time: ??.??
Abstract
In this research we discuss the problem of integrating domain-specific knowledge within a general framework for theorem proving. Our starting point is T-resolution [Policriti and Schwartz, 1996], that parametrically generalizes standard resolution with respect to a theory T (the parameter). T-resolution was introduced to provide a general theorem-proving framework in which the power of the basic inference rule can grow with the underlying theory T; another motivation was to establish criteria to classify first-order theories with respect to their suitability for theorem proving. In the framework obtained the tedious details of a proof are hidden inside the manager of the theory.
Being binary, the T-resolution inference rule is simpler than the previously proposed (n-ary) theory-resolution rule [Stickel, 1985] and more suitable for integration with refinements already proposed for (classical) resolution. Moreover, the T-resolution rule ensures a complete independence between the background level (the T-decider) of the T-theorem prover and its foreground reasoner. This could not be the case for theory-resolution, where the background reasoner plays an active role in the inference steps (residues generation [Stickel, 1985]).
The intrinsic non-determinism of T-resolution rule (as well as for theory-resolution) would reflect in a potential inefficiency of the implementation of a T-theorem prover. However, provided the theory T fulfills some simple and uniform requirements (i.e., ground decidability), strong-linearity constraints on the resolution tree can be imposed, without affecting completeness [Formisano and Policriti, 1995].
As a matter of fact, linearity is one of the most important refinements of resolution strictly linked with the ability to integrate domain-specific knowledge and inferential engines. The Constraint Logic Programming scheme proposed as a framework to integrate efficient constraint solver in the Logic Programming paradigm, is in fact another of our starting points.

We show that CLP(X) scheme [Jaffar and Lassez, 1986; Jaffar and Maher, 1994] can be easily embedded inside linear T-resolution. In a certain sense, CLP(X) stands to Horn-clause programming as T-resolution stands to standard resolution.
Extensions of the CLP(X)-scheme using the T-resolution inference rule allow to operate beyond equality and its drawbacks. For instance it is possible to define/characterize particular objects with respect to T, i.e. specify the T-properties of (newly introduced) entities.

In this work we will discuss the basics of T-resolution and its refinements, as well as its ability to encode the CLP(X) scheme. Moreover, we present some results to be used in order to classify theories with respect to their suitability for a use within the T-resolution scheme.
References

______________
__________________________________________

Previous page RISC SWP Linz Austria