It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.
Given a goal clause, represented as the negation of a problem to be solved :
, SLD resolution derives another goal clause, in which the selected literal is replaced by the negative literals of the input clause and the unifying substitution
However, in the more general case, the unifying substitution is necessary to make the two literals identical.
The name "SLD resolution" was given by Maarten van Emden for the unnamed inference rule introduced by Robert Kowalski.
[1] Its name is derived from SL resolution,[2] which is both sound and refutation complete for the unrestricted clausal form of logic.
"SLD" stands for "SL resolution with Definite clauses".
In both, SL and SLD, "L" stands for the fact that a resolution proof can be restricted to a linear sequence of clauses:
In both SL and SLD, "S" stands for the fact that the only literal resolved upon in any clause
In SL resolution, the selected literal is restricted to one which has been most recently introduced into the clause.
In the simplest case, such a last-in-first-out selection function can be specified by the order in which literals are written, as in Prolog.
In clausal logic, an SLD refutation demonstrates that the input set of clauses is unsatisfiable.
In logic programming, however, an SLD refutation also has a computational interpretation.
is the derivation, by means of backward reasoning, of a new set of sub-goals using an input clause as a goal-reduction procedure.
both passes input from the selected subgoal to the body of the procedure and simultaneously passes output from the head of the procedure to the remaining unselected subgoals.
The empty clause is simply an empty set of subgoals, which signals that the initial conjunction of subgoals in the top clause has been solved.
It is a failure node if its associated goal clause is non-empty but its selected literal unifies with no positive literal of definite clauses in the program.
Prolog searches the tree depth-first, one branch at a time, using backtracking when it encounters a failure node.
SLD resolution is also non-deterministic in the sense, mentioned earlier, that the selection rule is not determined by the inference rule, but is determined by a separate decision procedure, which can be sensitive to the dynamics of the program execution process.
The SLD resolution search space is an or-tree, in which different branches represent alternative computations.
In the case of propositional logic programs, SLD can be generalised so that the search space is an and-or tree, whose nodes are labelled by single literals, representing subgoals, and nodes are joined either by conjunction or by disjunction.
In the general case, where conjoint subgoals share variables, the and-or tree representation is more complicated.
Given the logic program in the Prolog language: and the top-level goal: the search space consists of a single branch, in which q is reduced to p which is reduced to the empty set of subgoals, signalling a successful computation.
In this case, the program is so simple that there is no role for the selection function and no need for any search.
In clausal logic, the program is represented by the set of clauses:
In Prolog, if this clause were added to the front of the original program, then Prolog would use the order in which the clauses are written to determine the order in which the branches of the search space are investigated.
If the clause were now added to the program, then the search tree would contain an infinite branch.
If this clause were tried first, then Prolog would go into an infinite loop and not find the successful branch.
SLDNF[3] is an extension of SLD resolution to deal with negation as failure.
In SLDNF, goal clauses can contain negation as failure literals, say of the form