SLD resolution (Selective Linear Definite clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution that 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:
¬ L 1 ∨ ⋯ ∨ ¬ L i ∨ ⋯ ∨ ¬ L n {\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}
with selected literal ¬ L i {\displaystyle \neg L_{i}} , and an input definite clause:
L ∨ ¬ K 1 ∨ ⋯ ∨ ¬ K m {\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}
whose positive literal (atom) L {\displaystyle L\,} unifies with the atom L i {\displaystyle L_{i}\,} of the selected literal ¬ L i {\displaystyle \neg L_{i}\,} , 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 θ {\displaystyle \theta \,} is applied:
( ¬ L 1 ∨ ⋯ ∨ ¬ K 1 ∨ ⋯ ∨ ¬ K m ∨ ⋯ ∨ ¬ L n ) θ {\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }
In the simplest case, in propositional logic, the atoms L i {\displaystyle L_{i}\,} and L {\displaystyle L\,} are identical, and the unifying substitution θ {\displaystyle \theta \,} 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. Its name is derived from SL resolution, 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 , ⋯ , C l {\displaystyle C_{1},C_{2},\cdots ,C_{l}}
where the "top clause" C 1 {\displaystyle C_{1}\,} is an input clause, and every other clause C i + 1 {\displaystyle C_{i+1}\,} is a resolvent one of whose parents is the previous clause C i {\displaystyle C_{i}\,} . The proof is a refutation if the last clause C l {\displaystyle 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 {\displaystyle 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.
… excerpt ends here. Continue reading the full article.
