SLD resolution definition logic, programming
(Selected, Linear, Definite) Linear resolution with a selection function for definite sentences.
A definite sentence has exactly one positive literal in each clause
and this literal is selected to be resolved upon, i.e. replaced in the goal
clause by the conjunction
of negative literals which form the body of the clause.
[Why is SLD resolution important?]