Extended Resolution: the reasoning engine
of Euclid
The reasoning engine of euclid is based
on an extension of the resolution principle. Much
in the spirit of the language Prolog and logic programming,
a proof is a set of derivations from the original
goal. Similar to the languages following the constraint
logic programming scheme a stack of bindings for the non-domain
variables and a stack of constraints for each solver is
maintained throughout the computation. The selection strategies
follow prolog and CLP(R).
Extended Unification
The resolution principle is based on finding
equal terms by providing bindings to their variables. Since
we have to make sure that this equality holds for all possible
interpretations of the terms, logic programming confines
itself to syntactic equality. This form of syntactic equality
is known as unification. Since in Euclid we work
partly in the intended interpretation the unification principle
is extended to include semantic information. The generalization
is straightforward: if the two terms compared are non-domain
terms standard unification applies to ensure equality on
all possible interpretations. If on the other hand the terms
are domain terms equality is handled by the solvers. In
that sense unifying the terms 5+3 and 8 succeeds as does
X+3 and 8 by returning the simplified constraint X=5.
The proof mechanism can also be seen in
terms of standard logic programming as partial evaluation:
the constraints are not evaluated and the answer to a query
is the result of this partial evaluation. Clearly the correctness
of such a computation depends primeraly on the correctness
of the domain solvers which directly manipulate the constraints.
