The term resolution in logic refers to a mechanical method for proving statements in first-order logic. It is applied to two clauses in a sentence, and by unification, it eliminates a literal that occurs positive in one clause and negative in the other. A literal stated in the antecedent of an implication is negative because an implication P → Q is equivalent to ¬P v Q. Therefore, in
(man(X) → mortal(X)) ʌ man(socrates)
we can unify socrates with X. This will give us
(man(socrates) → mortal(socrates)) ʌ man(socrates)
which is equivalent to
(¬man(socrates) v mortal(socrates)) ʌ man(socrates)
By distribution, we have
(¬man(socrates) ʌ man(socrates)) v (mortal(socrates) ʌ man(socrates))
Since ¬man(socrates) ʌ man(socrates) is false, we have
mortal(socrates) ʌ man(socrates)
Through this resolution process, we proved mortal(socrates). Resolution with backtracking is the basic control mechanism in Prolog.
SLD resolution is a term used in logic programming to refer to the control strategy used in such languages to resolve issues of nondeterminism. By definition, SLD resolution is 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.