= SLD resolution
{c}
<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.<SLD-resolution in Simply Logical>[§3.1, selection rule, resolution steps and SLD trees]{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.
Back to article page
