La estategia de resolución SLD es un caso particular de resolución lineal en la que, dado un programa P y un objetivo G, para probar la inconsistencia de P U {G} partimos del objetivo G, tomado como inicial, y se resuelve con alguna cláusula de P.[4]

Dado un objetivo G≡←A₁ ^ ... ^ A_j ^ ... A_n y una cláusula C≡A←B₁ ^ ... ^ B_m, entonces G' es un resolvente de G y C por resolución SLD, usando la regla de computación P si se cumple que:

1. Aj=P(G) es el átomo de G seleccionado por P;

2. θ=mgu(A,A_j)

3. G'≡←θ(A₁ ^ ... ^ A_j-1 ^ B₁ ^ ... ^ B_m ^ A_j+1 ^ ... ^ A_n).

También se dice que G' se deriva de G y C, y se representa en símbolos mediante la notación:

G→_SLD G'