1
00:00:00,000 --> 00:00:05,463
Simplest use of resolution is in
demonstrating unsatisfiability. In clausal

2
00:00:05,463 --> 00:00:11,290
form a contradiction takes the form of the
empty clause which is equivalent to the

3
00:00:11,290 --> 00:00:16,025
disjunction of no literals. Thus to
automate the determination of

4
00:00:16,025 --> 00:00:22,144
unsatisfiability, all we need to do is to
use resolution to derive consequences from

5
00:00:22,144 --> 00:00:28,847
the set to be tested Terminating when the
empty clause is finally generated. Let's

6
00:00:28,847 --> 00:00:35,780
start with a simple example. Suppose we
have four premises which are jointly

7
00:00:35,780 --> 00:00:43,169
unsatisfiable. P of A or B, or Q of AC. P
of XY implies R of X. Q of XY implies R of

8
00:00:43,169 --> 00:00:50,020
X And not R is Z. The derivation of the
empty clause in this case is easy. We

9
00:00:50,020 --> 00:00:55,512
resolve the first clause with the second,
to get the clause shown on line five. In

10
00:00:55,512 --> 00:01:03,725
this case x is bound to a, y is bound to
b. Next we resolve the result with the

11
00:01:03,725 --> 00:01:09,889
third clause to get the unit clause on
line six. Note that r of a is the

12
00:01:09,889 --> 00:01:14,654
remaining literal from clause three after
the resolution And r of a is also the

13
00:01:14,654 --> 00:01:19,301
remaining literal from clause five after
the resolution. Since the two clauses,

14
00:01:19,301 --> 00:01:24,126
literals are identical, they appear only
once in the result Because, of course, the

15
00:01:24,126 --> 00:01:33,680
result is set With literals. Finally, we
resolve this result with the clause in

16
00:01:33,680 --> 00:01:36,340
line four to produce the empty clause.