Höhfeld and Smolka provide a generalization of the SLD-resolution method known from standard logic programming (cf. [Lloyd1987]) to definite clauses in . The key result of this generalization is that most important results from conventional logic programming carry over for definite clause specifications using arbitrary constraint languages.
The fundamental inference rule for definite clauses in is the following goal reduction rule (using a slightly different notation from that given in [Höhfeld and Smolka1988])
where 
is the selected element of a goal and
is a variant of a clause of a definite clause specification S, such that the variables in the clause do not occur in the original goal, except for the variables explicitly mentioned, which means that the variant must be variable-disjoint from the original goal (the antecedent part of the goal reduction rule). A variant of a clause can be obtained by renaming the variables of the clause.
We also say that the new goal 
is a derived form and call it the resolvent of the goal
and 
. Höhfeld and Smolka show that goal reduction
is a sound and complete basic inference rule for definite clause
specifications in .
Note that the inference rule is only applied in case the resulting
constraint 
is satisfiable, since otherwise we would not
be able to find some answer. Therefore, we will make use of the
following optimization known from conventional logic programming and
proven by [Höhfeld and Smolka1988] for the general case:
Immediately after a goal reduction step, it is checked, whether the
resulting constraint is
satisfiable through a constraint solver which attempts
to compute a normalized constraint that is equivalent to .
Note that this requires the underlying constraint language
to have a set of normal -constraints, as does the one presented in
the next section. If such a normal constraint cannot be computed,
we immediately try another clause since this part of the search space
cannot contain any answer. This kind of constraint solving is related to the
`unification' operation in Prolog or PATR-II. Thus we can define the
following optimized goal reduction rule:
where is the selected element of a goal and
is a variant of a clause of a definite clause specification
S, and 
is the most general unifier obtained by unifying
and 
, which we also write as 
.
A proof of a goal g for a clause specification S is a sequence of
goals 
where each goal 
is derived from 
by applying goal reduction using a variant of a clause of S and the
last goal is the empty clause, where its associated constraint is said
to be the computed S-answer of the goal g.
Höhfeld and Smolka show that answers computed in that way are answers
for the goal.
A proof of a goal as described above is a refutation proof,
which shows that the denial of some formula q is inconsistent with the
assumptions of S, i.e., if 
derives the empty clause.
If the empty clause is
obtained, then a refutation has been discovered, and the
constraint associated with the empty clause is an answer of the goal.
The sequence of goals obtained during a proof is called an SLD-derivation. A SLD-derivation may be finite or infinite. A finite SLD-derivation may be successful or failed. A successful derivation is just a refutation. A failed SLD-derivation is one that ends in a non-empty goal with the property that the resulting constraint is unsatisfiable.
The SLD-refutation by itself does not define an algorithm since it does not make use of a concrete selection function (or computation rule) as well as a strategy for selecting clauses. The first nondeterminism is known as don't care and the second as don't know. The don't care property of the selection function is also known as the ``independence property'' of the selection function (cf. [Lloyd1987]) and means that in principle a CLP system can choose any local selection function it finds convenient.
The don't know property means that for the selection of clauses an exhaustive search is necessary, since it cannot be known in advance which sequence of clauses will lead to a successful proof. Since for the selected element of a goal several alternative clauses may be available leading to a set of alternative re-solvents, the search space is a certain type of tree, called an SLD-tree. Clearly, the whole search space is only defined implicitly by a definite clause specification, so that an SLD-tree has to be constructed during the proof of some goal. The strategy used to search an SLD-tree is defined by the search rule.
An SLD-tree for 
of a
definite clause specification S and a goal g is a tree satisfying
the following condition (cf. also [Lloyd1987]):
be a node in
the tree and the selected element. Then each possible
resolvent (using all matching clauses from S) is a child of
that node
Each branch of an SLD-tree is a derivation of , where
those branches which correspond to successful derivations are called
success branches, and branches corresponding to failed
derivations are called failure branches. This implies that each
success branch corresponds to a computed answer of g.
A search rule is a strategy for searching SLD-trees to find success branches. An SLD-refutation procedure is specified by a selection function together with a search rule. For example, Prolog is a SLD-refutation procedure using the leftmost selection function and a top-down, depth-first backtracking search rule.
In the next chapter we present a SLD-refutation procedure using a data-driven selection function and an Earley-type search rule. However, in order to illustrate this new algorithm by concrete examples, we first have to define a specific constraint language.