First-order resolution is a theorem-proving technique that condenses the traditional syllogisms of logical inference down to a single rule.
To understand how resolution works, consider the following example syllogism of term logic:
All Greeks are Europeans. Homer is a Greek. Therefore, Homer is a European.Or, more generally:
∀X, P(X) implies Q(X). P(A). Therefore, Q(A).To recast the reasoning using the resolution technique, first the clauses must be converted to Conjunctive normal form. In this form, all quantification becomes implicit: universal quantifiers on variables (X, Y...) are simply omitted as understood, while existentially-quantified variables are replaced by atoms (A, B...) (in the Prolog sense):
¬P(X) ∨ Q(X) P(A) Therefore, Q(A)So the question is, how does the resolution technique derive the last clause from the first two? The rule is simple:
- Find two clauses containing the same predicate, where it is negated in one clause but not in the other.
- Perform a unification on the two predicates. (If the unification fails, you made a bad choice of predicates. Go back to the previous step and try again.)
- If any unbound variables which were bound in the unified predicates also occur in other predicates in the two clauses, replace them with their bound values (atoms) there as well.
- Discard the unified predicates, and combine the remaining ones from the two clauses into a new clause, also joined by the "∨" operator.
¬P(X)in the first clause, and in non-negated form
P(A)in the second clause. X is an unbound variable, while A is a bound value (atom). Unifying the two produces the substitution
X => ADiscarding the unified predicates, and applying this substitution to the remaining predicates (just Q(X), in this case), produces the conclusion:
Q(A)For another example, consider the syllogistic form
All Cretans are islanders. All islanders are liars. Therefore all Cretans are liars.Or more generally,
∀X P(X) implies Q(X) ∀X Q(X) implies R(X) Therefore, ∀X P(X) implies R(X)In CNF, the antecedents become:
¬P(X) ∨ Q(X) ¬Q(Y) ∨ R(Y)(Note I renamed the variable in the second clause to make it clear that variables in different clauses are distinct.)
Now, unifying Q(X) in the first clause with ¬Q(Y) in the second clause means that X and Y become the same variable anyway. Substituting this into the remaining clauses and combining them gives the conclusion:
¬P(X) ∨ R(X)The resolution rule similarly subsumes all the other syllogistic forms of traditional logic.