Simplest use of resolution is in
demonstrating unsatisfiability. In clausal
form a contradiction takes the form of the
empty clause which is equivalent to the
disjunction of no literals. Thus to
automate the determination of
unsatisfiability, all we need to do is to
use resolution to derive consequences from
the set to be tested Terminating when the
empty clause is finally generated. Let's
start with a simple example. Suppose we
have four premises which are jointly
unsatisfiable. P of A or B, or Q of AC. P
of XY implies R of X. Q of XY implies R of
X And not R is Z. The derivation of the
empty clause in this case is easy. We
resolve the first clause with the second,
to get the clause shown on line five. In
this case x is bound to a, y is bound to
b. Next we resolve the result with the
third clause to get the unit clause on
line six. Note that r of a is the
remaining literal from clause three after
the resolution And r of a is also the
remaining literal from clause five after
the resolution. Since the two clauses,
literals are identical, they appear only
once in the result Because, of course, the
result is set With literals. Finally, we
resolve this result with the clause in
line four to produce the empty clause.