Talk:SLD resolution

I wrote this article in part because I had a little trouble quickly finding what the letters SLD in SLDNF stood for. I know now, but I still don't fully understand why why Selected, Linear, Definite was chosen by its inventor.

I would love to see this article expanded in various ways:

• Briefly expand on the meaning of Selected, Linear, Definite.
• Provide the main properties of SLD resolution that logicians consider "nice".
• A section on the history of SLD resolution, including its basis on SL resolution, and the addition of negation as failure.
• Contrast SLD with other methods of resolution.
• Expand the External Links section. I considered adding some PDF links found in a Google search, but I currently lack experience in what would be the definitive sources.

PaulBrinkley 20:52, 4 June 2007 (UTC)

     *  Briefly expand on the meaning of Selected, Linear, Definite.

"Definite" refers to the fact that, in comparison with the general first-order case, where clauses can be written as implications, such as $(a\land b)\to (c\lor d)$, which have "indefinite" conclusions, such as $(c\lor d)$, Horn clauses have "definite" conclusions in which there is no disjunction $(\lor )$.

"Linear" refers to the fact that, in contrast with general unrestricted resolution proofs, which have the form of trees, resolution can be restricted, even in the general first-order case, to proofs where one of the parents of a resolution inference step is either an input clause or an ancestor clause earlier in the proof. In the case of Horn clauses (or definite clauses), ancestor resolution is unnecessary, and every resolvent has one parent that is an input clause.

"Selected" refers to the fact that the literal that is resolved upon in the non-input clause can be freely selected from among the literals occurring in the clause. There are two alternatives to "selection". One alternative is that every literal is selected in every order, so that a clause containing n literals could have n! (factorial) equivalent resolvents. This was the case, with ordinary linear resolution. The other alternative is that literals are selected in some fixed order, which can be specified by writing the literals in the order in which they are to be selected. This is the case with ordinary Prolog.

   * Provide the main properties of SLD resolution that logicians consider "nice".

From a logical point of view, it is nice both to eliminate the redundancy of unrestricted linear resolution and to allow more flexible selection of literals (not exploited in Prolog). From a computational point of view, it is nice that the top clause and the non-input clauses in a proof can be viewed as sets of goals or procedure calls, and SLD resolution can be viewed as goal-reduction or procedure execution. From a psychological point of view, it is nice that proofs can be understood in terms of backward reasoning from a top-level goal to sub-goals, and do not have to be understood in the usual resolution manner, in which the top-level query is negated.

   * A section on the history of SLD resolution, including its basis on SL resolution, and the addition of negation as failure.

 * Contrast SLD with other methods of resolution.

In the beginning there was unrestricted resolution, which is very nice, but has two big problems. One problem is that it is incredibly redundant. The other is that it generates resolvents that are irrelevant to the problem to be solved. The second problem was addressed early on in the form of the "set of support" strategy, which imposed the restriction that at least one parent of every resolvent should be a descendant of some input clause that is, informally speaking, directly relevant to the problem to be solved.

The redundancy problem took longer to solve, and gave rise to several different solutions. There are two main kinds of solutions - ones that use resolution bottom-up ("forwards", from what is given to what is desired), like hyper-resolution, and ones that use resolution top-down ("backwards", from the query or goal). Linear resolution is mostly used top-down, but in some cases (for example for integrity checking, when a new clause is added to an existing set of clauses believed to be consistent), it can also be used for bottom-up reasoning.

A number of resolution systems were developed in the early 1970s, which independently discovered linear resolution. Some of these had no restriction on the choice of selected literal and were therefore exceedingly redundant. Others used a fixed ordering (as in Prolog) to eliminate redundancy.

Independently, Donald Loveland developed the model elimination procedure in 1968. By comparison with resolution, it had already solved the redundancy and irrelevancy problems, but it was technically difficult, and its relationship with resolution was not clear. It was not until 1970-71, that the relationship between model elimination and linear resolution was independently discovered by Loveland and by Kowalski and Kuehner. SL-resolution, developed by Kowalski and Kuehner was a form of linear resolution, which could also be viewed as a variant of model-elimination. It introduced the use of a selection function to select the literal to be resolved upon. However, the selected literal was restricted to one of the literals most recently introduced into the clause. There is no such restriction in SLD, due to its restriction to definite clauses.

The terms SLD and SLDNF were introduced by Apt and van Emden in 1982. SLD was their name for the unnamed proof procedure introduced by Kowalski in 1974 and called LUSH (linear unrestricted selection for Horn clauses) by Robert Hill in Edinburgh.

SLDNF stands for SLD with negation as failure. In SLDNF, the top-level query/goal and non-input resolvents can contain negation as failure literals, say of the form not(p). These may be selected if they contain not variables. To show not(p), SLDNF tries to show p. If p finitely fails, then not(p) succeeds. If p succeeds, then not(p) fails.

One, further important point: Resolution and all its variants only define a search space of all the possible inferences that potentially need to be generated to find a desired solution to some initially given problem. They do not specify what search strategy should be used to search that space. Prolog uses a depth-first search, which is very efficient in space, but which can be incomplete if the search space contains infinite branches. Other search strategies are also possible, including breadth-first search, as well as best-first search and branch and bound.

   * Expand the External Links section. 

I have two papers on my webpage, http://www.doc.ic.ac.uk/~rak/, the 1974 paper in which SLD was introduced, http://www.doc.ic.ac.uk/~rak/papers/IFIP74.pdf, without name, and the SL-resolution paper,http://www.doc.ic.ac.uk/~rak/papers/sl.pdf, which includes a comparison with model elimination. Robert Kowalski 11:37, 2 July 2007 (UTC)

The term SLD was coined by van Emden as an alternative to Robert Hill's term LUSH when it was presented in a talk in Edinburgh in 1975. It was intended to stand for "SL resolution with Definite clauses". So it is an acronym derived from an acronym. At that time a term for a Horn clause with a positive literal, though needed, seemed to be missing. At the same time, van Emden coined the term "definite clause" for that. The terminology first appeared in published form in "Computation and Deductive Information Retrieval" by van Emden, a paper in a 1977 conference, published in 1978 in "Formal Description of Programming Concepts", edited by Erich Neuhold. The terminology only gained general currency with "Contributions to the Theory of Logic Programming" by Apt and van Emden. Vanemden 15:15, 17 July 2007 (UTC) Vanemden 15:15, 17 July 2007 (UTC)

In the section "SLD Inference Rule", I think the L_i and L are backwards in the sentence "whose positive literal L_i ...". I have trouble making sense of the section otherwise. SamRushing (talk)