Resolution: We have introduced the inference rule Modus Ponens. Now we introduce another inference rule that is particularly significant, Resolution.
Since it is not trivial to understand, we proceed in two steps. First we introduce Resolution in the Propositional Calculus, that is, in a language with only truth valued variables. Then we generalize to First Order Logic.
Resolution in the Propositional Calculus: In its simplest form Resolution is the inference rule:
{A OR C, B OR (NOT C)}
----------------------
A OR B
More in general the Resolution Inference Rule is:
In symbols:
{C1, C2}
---------------------------------
(C1 - {L}) UNION (C2 - {(NOT L)})
Example: The following set of clauses is inconsistent:
1. (P OR (NOT Q))
2. ((NOT P) OR (NOT S))
3. (S OR (NOT Q))
4. Q
In fact:
5. ((NOT Q) OR (NOT S)) from 1. and 2.
6. (NOT Q) from 3. and 5.
7. FALSE from 4. and 6.
Notice that 7. is really the empty clause [why?].
Theorem: The Propositional Calculus with the Resolution Inference Rule is sound and Refutation Complete.
NOTE: This theorem requires that clauses be represented as sets, that is, that each element of the clause appear exactly once in the clause. This requires some form of membership test when elements are added to a clause.
C1 = {P P}
C2 = {(NOT P) (NOT P)}
C = {P (NOT P)}
From now on by resolution we just get again C1, or C2, or C.
Resolution in First Order Logic: Given clauses C1 and C2, a clause C is a RESOLVENT of C1 and C2, if
1. There is a subset C1' = {A1, .., Am} of C1 of literals of the same sign, say positive, and a subset C2' = {B1, .., Bn} of C2 of literals of the opposite sign, say negative,
2. There are substitutions s1 and s2 that replace variables in C1' and C2' so as to have new variables,
3. C2'' is obtained from C2 removing the negative signs from B1 .. Bn
4. There is an Most General Unifier s for the union of C1'.s1 and C2''.s2
and C is
((C1 - C1').s1 UNION (C2 - C2').s2).s
In symbols this Resolution inference rule becomes:
{C1, C2}
--------
C
If C1' and C2' are singletons (i.e. contain just one literal), the rule is called Binary Resolution.
Example:
C1 = {(P z (F z)) (P z A)}
C2 = {(NOT (P z A)) (NOT (P z x)) (NOT (P x z))
C1' = {(P z A)}
C2' = {(NOT (P z A)) (NOT (P z x))}
C2'' = {(P z A) (P z x)}
s1 = [z1/z]
s2 = [z2/z]
C1'.s1 UNION C2'.s2 = {(P z1 A) (P z2 A) (P z2 x)}
s = [z1/z2 A/x]
C = {(NOT (P A z1)) (P z1 (F z1))}
Notice that this application of Resolution has eliminated more than one literal from C2, i.e. it is not a binary resolution.
Theorem: First Order Logic, with the Resolution Inference Rule, is sound and refutation complete.
We will not develop the proof of this theorem. We will instead look at some of its steps, which will give us a wonderful opportunity to revisit Herbrand. But before that let's observe that in a sense, if we replace in this theorem "Resolution" by "Binary Resolution", then the theorem does not hold and Binary Resolution is not Refutation Complete. This is the case when in the implementation we do not use sets but instead use bags.This can be shown using the same example as in the case of propositional logic.
Given a clause C, a subset D of C, and a substitution s that unifies D, we define C.s to be a Factor of C. The Factoring Inference Rule is the rule with premise C and as consequence C.s.
Theorem: For any set of clauses S and clause C, if C is derivable from S using Resolution, then C is derivable from S using Binary Resolution and Factoring.
When doing proofs it is efficient to have as few clauses as possible. The following definition and rule are helpful in eliminating redundant clauses:
A clause C1 Subsumes a clause C2 iff there is a substitution s such that C1.s is a subset of C2.
Subsumption Elimination Rule: If C1 subsumes C2 then eliminate C2.
