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, represented as the negation of a problem to be solved :
[math]\displaystyle{ \neg L_1 \lor \cdots \lor \neg L_i \lor \cdots \lor \neg L_n }[/math]
with selected literal [math]\displaystyle{ \neg L_i }[/math], and an input definite clause:
[math]\displaystyle{ L \lor \neg K_1 \lor \cdots \lor \neg K_m }[/math]
whose positive literal (atom) [math]\displaystyle{ L\, }[/math] unifies with the atom [math]\displaystyle{ L_i \, }[/math] of the selected literal [math]\displaystyle{ \neg L_i \, }[/math], 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 [math]\displaystyle{ \theta \, }[/math] is applied:
[math]\displaystyle{ (\neg L_1 \lor \cdots \lor \neg K_1 \lor \cdots \lor \neg K_m\ \lor \cdots \lor \neg L_n)\theta }[/math]
In the simplest case, in propositional logic, the atoms [math]\displaystyle{ L_i \, }[/math] and [math]\displaystyle{ L \, }[/math] are identical, and the unifying substitution [math]\displaystyle{ \theta \, }[/math] 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.[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:
[math]\displaystyle{ C_1, C_2, \cdots, C_l }[/math]
where the "top clause" [math]\displaystyle{ C_1 \, }[/math] is an input clause, and every other clause [math]\displaystyle{ C_{i+1} \, }[/math] is a resolvent one of whose parents is the previous clause [math]\displaystyle{ C_i \, }[/math]. The proof is a refutation if the last clause [math]\displaystyle{ C_l \, }[/math] 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 [math]\displaystyle{ C_i \, }[/math] 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 [math]\displaystyle{ \neg L_1 \lor \cdots \lor \neg L_i \lor \cdots \lor \neg L_n }[/math] can be interpreted as the denial of a conjunction of subgoals [math]\displaystyle{ L_1 \land \cdots \land L_i \land \cdots \land L_n }[/math]. The derivation of clause [math]\displaystyle{ C_{i+1} \, }[/math] from [math]\displaystyle{ C_i \, }[/math] 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 [math]\displaystyle{ \theta \, }[/math] 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.
SLD resolution strategies
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 no positive literal of definite clauses in the program.
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 computing resources, but is incomplete if the search space contains infinite branches and the search strategy searches these in preference to finite branches: the computation does not terminate. 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:
[math]\displaystyle{ q \lor \neg p }[/math]
[math]\displaystyle{ p \, }[/math]
and top-level goal is represented by the goal clause with a single negative literal:
[math]\displaystyle{ \neg q }[/math]
The search space consists of the single refutation:
[math]\displaystyle{ \neg q, \neg p, \mathit{false} }[/math]
where [math]\displaystyle{ \mathit{false} \, }[/math] 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 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
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 [math]\displaystyle{ not(p) \, }[/math], 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 [math]\displaystyle{ p \, }[/math] as top clause. The selected subgoal [math]\displaystyle{ not(p) \, }[/math] succeeds if the subproof fails, and it fails if the subproof succeeds.
See also
References
- ↑ Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, University of Edinburgh. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574.
- ↑ Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function Artificial Intelligence, Vol. 2, 1971, pp. 227-60.
- ↑ 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
- Jean Gallier, SLD-Resolution and Logic Programming chapter 9 of Logic for Computer Science: Foundations of Automatic Theorem Proving, 2003 online revision (free to download), originally published by Wiley, 1986
- John C. Shepherdson, SLDNF-Resolution with Equality, Journal of Automated Reasoning 8: 297-306, 1992; defines semantics with respect to which SLDNF-resolution with equality is sound and complete
External links
- [1] Definition from the Free On-Line Dictionary of Computing
 |  |
