SLD resolution

SLD resolution

SLD resolution ("Selective Linear Definite" clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.

The SLD inference rule

Given a goal clause:

$eg L_1 or cdots or eg L_i or cdots or eg L_n$

with selected literal $eg L_i$, and an input definite clause:

$L or eg K_1 or cdots or eg K_m$

whose positive literal $L_i ,$ unifies with the selected literal $L ,$, 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 $heta ,$ is applied:

$\left( eg L_1 or cdots or eg K_1 or cdots or eg K_m or cdots or eg L_n\right) heta$

In the simplest case, in propositional logic, the literals $L_i ,$ and $L ,$ are identical, and the unifying substitution $heta ,$ is vacuous. However, in the more general case, the unifying substitution is necessary to make the two literals identical.

The origin of the name "SLD"

The name "SLD resolution" was given by Maarten van Emden for the unnamed inference rule introduced by Robert Kowalski in [Kowalski 1973, 1974] . Its name is derived from SL resolution [Kowalski and Kuehner 1971] , 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:

$C_1, C_2, cdots, C_l$

where the "top clause" $C_1 ,$ is an input clause, and every other clause $C_\left\{i+1\right\} ,$ is a resolvent one of whose parents is the previous clause $C_i ,$. The proof is a refutation if the last clause $C_l ,$ is the empty clause.

In SLD, all of the clauses in the sequence are goal clauses, and the other parent is an input clause. In SL resolution, the other parent is either an input clause or an ancestor clause earlier in the sequence.

In both SL and SLD, "S" stands for the fact that the only literal resolved upon in any clause $C_i ,$ is one that is uniquely selected by a selection rule or selection function. 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. However, the selection function in SLD resolution is more general than in SL resolution and in Prolog. There is no restriction on the literal that can be selected.

The computational interpretation of SLD resolution

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. The top clause $eg L_1 or cdots or eg L_i or cdots or eg L_n$ can be interpreted as the denial of a conjunction of subgoals $L_1 and cdots and L_i and cdots and L_n$. The derivation of clause $C_\left\{i+1\right\} ,$ from $C_i ,$ is the derivation, by means of backward reasoning, of a new set of sub-goals using an input clause as a goal-reduction procedure. The unifying substitution $heta ,$ 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.

The non-deterministic nature of SLD resolution

SLD resolution implicitly defines a search tree of alternative computations, in which the initial goal clause is associated with the root of the tree. For every node in the tree and for every definite clause in the program whose positive literal unifies with the selected literal in the goal clause associated with the node, there is a child node associated with the goal clause obtained by SLD resolution.

A leaf node, which has no children, is a success node if its associated goal clause is the empty clause. It is a failure node if its associated goal clause is non-empty but its selected literal unifies with the positive literal of no input clause.

SLD resolution is non-deterministic in the sense that it does not determine the search strategy for exploring the search tree. Prolog searches the tree depth-first, one branch at a time, using backtracking when it encounters a failure node. Depth-first search is very efficient in its use of space, but is incomplete if the search space contains infinite branches and the search strategy searches these in preference to finite branches. Other search strategies, including breadth-first, best-first, and branch-and-bound search are also possible. Moreover, the search can be carried out sequentially, one node at a time, or in parallel, many nodes simultaneously.

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.

Example

Given the logic program:

` q :- p `

`p`

and the top-level goal:

`q`

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:

$q or eg p$

$p ,$

and top-level goal is represented by the goal clause with a single negative literal:

$eg q$

The search space consists of the single refutation:

$eg q, eg p, false$

where $false ,$ represents the empty clause.

If the following clause were added to the program:

` q :- r `

then there would be an additional branch in the search space, whose leaf node `r` is a failure node. 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. Prolog would try this new branch first, fail, and then backtrack to investigate the single branch of the original program and succeed.

If the clause

` p :- p `

were now added to the progam, 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.

LDNF

SLDNF [Apt and van Emden 1982] 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 $not\left(p\right) ,$, which can be selected only if they contain no variables. When such a variable-free literal is selected, a subproof (or subcomputation) is attempted to determine whether there is an SLDNF refutation starting from the corresponding unnegated literal $p ,$ as top clause. The selected subgoal $not\left(p\right) ,$ succeeds if the subproof fails, and it fails if the subproof succeeds.

References

*Krzysztof Apt and Maarten van Emden, Contributions to the Theory of Logic Programming, Journal of the Association for Computing Machinery. Vol, 1982 - portal.acm.org

*Robert Kowalski and Donald and Kuehner, [http://www.doc.ic.ac.uk/~rak/papers/sl.pdf Linear Resolution with Selection Function] Artificial Intelligence, Vol. 2, 1971, pp. 227-60.

*Robert Kowalski [http://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf Predicate Logic as a Programming Language] Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.

* [http://foldoc.org/?SLD+resolution] Definition from the Free On-Line Dictionary of Computing

Wikimedia Foundation. 2010.

Look at other dictionaries:

• SLD-resolution — SLD résolution En programmation logique, la SLD résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d un ensemble de clauses de Horn. Elle est basée sur… …   Wikipédia en Français

• Sld-résolution — En programmation logique, la SLD résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d un ensemble de clauses de Horn. Elle est basée sur une résolution… …   Wikipédia en Français

• SLD-résolution — En programmation logique, la SLD résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d un ensemble de clauses de Horn. Elle est basée sur une résolution… …   Wikipédia en Français

• SLD — can mean the following:* In Polish, SLD is short for Sojusz Lewicy Demokratycznej which is a Polish political party. In English, this party is called the Democratic Left Alliance . * In British politics, the party currently known as the Liberal… …   Wikipedia

• SLD — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. SLD est un acronyme : Sauver Le Darfour : association française contre les massacres du Darfour (l analogue du Save Darfur Coalition américain)… …   Wikipédia en Français

• Resolution (logic) — In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem proving technique for sentences in propositional logic and first order logic. In other words, iteratively applying the… …   Wikipedia

• Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… …   Wikipedia

• Prolog — Pour les articles homonymes, voir Prolog (homonymie). Prolog Apparu en 1972 Auteur …   Wikipédia en Français

• Prolog — infobox programming language paradigm = Logic programming year = 1972 designer = Alain Colmerauer implementations = BProlog, ECLiPSe, Ciao Prolog, GNU Prolog, Quintus, SICStus, Strawberry, SWI Prolog, YAP Prolog, tuProlog dialects = ISO Prolog,… …   Wikipedia

• Horn clause — In mathematical logic, a Horn clause is a clause (a disjunction of literals) with at most one positive literal. They are named after the logician Alfred Horn, who first pointed out the significance of such clauses in 1951. Horn clauses play a… …   Wikipedia