** Resolution Step for Propositional Calculus**

A * clause* is a disjunction of literals (atoms or negations of atoms).

Select two clauses *C*_{1} and *C*_{2} that have * exactly one* atom
that is positive in one clause and negated in the other.

Form a new clause, consisting of all literals of both clauses except for
the two complementary literals, and add it to the set of clauses.

Theorem: The new clause produced by resolution is a logical consequence
of the two parent clauses.

Proof: Let the parent clauses be *C*_{1} = L &or C_{1}' and
*C*_{2} = ¬ L &or C_{2}'; the resolvent is *H = C*_{1}' &or C_{2}'.
Suppose that *C*_{1} and *C*_{2} are true in an interpretation *I*.

Case 1: *L* = true in *I*. Then since *C*_{2} = ¬ L &or C_{2}',
*C*_{2}' must be true in *I* and *H* is true in *I*.

Case 2: *L* = false in *I*. Then since *C*_{1} = L &or C_{1}',
*C*_{1}' must be true in *I* and *H* is true in *I*.

Contents
Page-10
Prev
Next
Page+10
Index