SLD resolution

In logic programming, SLD resolution is an algorithm for mechanically proving statements of first-order logic from a set of Horn clauses; particularly, linear resolution with a selection function for definite sentences. SLD stands for Selected, Linear, Definite. It is better known for its extension, SLDNF (NF meaning "negation as failure"), the resolution algorithm employed by the Prolog programming language.

Definite sentence

A definite sentence is a Horn clause with exactly one positive literal. In SLD resolution, the positive literal of a definite sentence is considered the head, or conclusion, or goal of the sentence; any negative literals are considered its body, or antecedents, or subgoals. For example, the Horn clause

$\lnot a\lor \lnot b\lor c$

is logically equivalent to

$(a\land b)\to c$

or, in turn, the Prolog rule

c :- a, b.

In each case, $c$ is the conclusion, and $a$ and $b$ are the antecedents.

The resolution process

Given a program (a set of Horn clauses) and a special Horn clause denoted as a query, SLD resolution works much like other forms of resolution by attempting to unify Horn clauses to create new ones, until either a contradiction is reached, or no further unification can be made.

In particular, it starts by negating the query, then unifying the result with a program clause. The program clause is found deterministically by matching its positive literal with its negative counterpart in the query. The program clauses are considered to be ordered; if more than one match exists, then the first one is used.

If a contradiction is found, then the negation is inconsistent with the program, meaning that the query succeeds. If no unification can be found, then the query fails. If a unification exists but yields no contradiction, then the new clause is unified against the program in a subprocess. If no unification can be found in a subprocess, then the next outer unification is considered to have failed, and the search continues from where that match was found; this backtracking step is how matches after the first clause may be used.

For a simple example, given the program:

  $\lnot p\lor q$ 
  $p\,$

and the query:

  $q\,$

The query is negated - $\lnot q$ - and a unifiable match is sought in the program. The first clause is that match. Conjuncting them yields:

  $(\lnot p\lor q)\land \lnot q\to \lnot p$

Repeating the process for $\lnot p$ , the second clause is a match.

  $p\land \lnot p\to F$

This is a contradiction, so $q\,$ succeeds.

In Prolog, the first clause would appear as q :- p . The algorithm then looks like this: "to prove q, find a clause that concludes it. The first clause matches, and requires p to be proven. The second clause proves p, and so q is proved."

If the following clause were added to the front of the program:

  $\lnot r\lor q$

then the resolution would match it first, obtain $\lnot r$ from unification, and then fail to unify $\lnot r$ . This would lead to backtracking; SLD resolution would seek to match $\lnot q$ with a later clause, find $\lnot p\lor q$ , and then proceed as in the previous example.

External Links

[1] Definition from the Free On-Line Dictionary of Computing