Automated deduction scheme
Date: July 17th (Wednesday)
Time: 10:45-11:10
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
- [Formisano, A., and Policriti, A, 1995]
T-resolution: Refinements and Model Elimination.
Research Report 32/95, Dip. di Matematica e Informatica, Univ. di
Udine, 1995.
- [Jaffar, J., and Lassez, J.-L., 1986]
Constraint Logic Programming.
Tech. rep., Department of Computer Science, Monash University, June
1986.
- [Jaffar, J., and Maher, M. J., 1994]
Constraint Logic Programming: A Survey.
The Journal of Logic Programming 19-20 (1994), 503-581.
- [Policriti, A., and Schwartz, J. T., 1996]
T-theorem proving I.
Journal of Symbolic Computation (1996). To appear.
- [Stickel, M. E., 1985]
Automated deduction by theory resolution.
Journal of Automated Reasoning I (1985).
