SLD resolution, or **Selective Linear Definite clause resolution**, is a key concept in the field of logic programming and automated theorem proving. It is a refinement of the resolution principle that is used to infer conclusions from a set of logical clauses. SLD resolution specifically applies to definite clauses, which are expressions in propositional logic or predicate logic that have a specific format.
Articles by others on the same topic
SLD resolution is a goal-directed inference rule for definite first-order Horn clauses. It selects an atom from the current goal, matches it with a suitably renamed clause head using a most general unifier, and replaces it by that clause's body, applying the same first-order substitution throughout the goal. Reaching the empty goal supplies a successful derivation.[ref]
For example, the rule
ancestor(X,Y) :- parent(X,Y) reduces the query ancestor(ada,Y) to parent(ada,Y). Matching the fact parent(ada,ben) then gives Y=ben. Alternative matching clauses create a search tree. Prolog normally selects the leftmost goal and searches clauses in order with backtracking; a recursive branch can therefore run indefinitely before another branch's valid answer is reached. The logical inference rule and the strategy traversing its alternatives are separate choices.