SLD resolution
Encyclopedia
SLD 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 clause
s.
with selected literal
, and an input definite clause:
whose positive literal (atom)
unifies with the atom 
of the selected literal 
, 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 
is applied:
In the simplest case, in propositional logic, the atoms
and 
are identical, and the unifying substitution 
is vacuous. However, in the more general case, the unifying substitution is necessary to make the two literals identical.
. 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:
where the "top clause"
is an input clause, and every other clause 
is a resolvent one of whose parents is the previous clause 
. The proof is a refutation if the last clause 
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
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.
, however, an SLD refutation also has a computational interpretation. The top clause
can be interpreted as the denial of a conjunction of subgoals 
. The derivation of clause 
from 
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 
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.
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 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.
and the top-level goal:
the search space consists of a single branch, in which
In clausal logic, the program is represented by the set of clauses:
and top-level goal is represented by the goal clause with a single negative literal:
The search space consists of the single refutation:
where
represents the empty clause.
If the following clause were added to the program:
then there would be an additional branch in the search space, whose leaf node
If the clause
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.
, 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 
as top clause. The selected subgoal 
succeeds if the subproof fails, and it fails if the subproof succeeds.
Logic programming
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 representation language, and a...
. It is a refinement of resolution
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...
, which is both sound
Soundness
In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
and refutation complete
Completeness
In general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
for Horn clause
Horn clause
In mathematical logic, a Horn clause is a clause 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...
s.
The SLD inference rule
Given a goal clause:with selected literal
, and an input definite clause:whose positive literal (atom)
unifies with the atom of the selected literal , 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 is applied:In the simplest case, in propositional logic, the atoms
and are identical, and the unifying substitution 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 KowalskiRobert Kowalski
Robert "Bob" Anthony Kowalski is a British logician and computer scientist, who has spent most of his career in the United Kingdom....
. 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:
where the "top clause"
is an input clause, and every other clause is a resolvent one of whose parents is the previous clause . The proof is a refutation if the last clause 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
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 PrologProlog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
. 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 programmingLogic programming
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 representation language, and a...
, however, an SLD refutation also has a computational interpretation. The top clause
can be interpreted as the denial of a conjunction of subgoals . The derivation of clause from 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 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 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 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
And-or tree
An and–or tree is a graphical representation of the reduction of problems to conjunctions and disjunctions of subproblems .-Example:The 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 pand the top-level goal:
qthe 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:
and top-level goal is represented by the goal clause with a single negative literal:
The search space consists of the single refutation:
where
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 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, 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 as top clause. The selected subgoal succeeds if the subproof fails, and it fails if the subproof succeeds.External links
- http://foldoc.org/?SLD+resolution Definition from the Free On-Line Dictionary of Computing