Proving unsatisfiability with propositional resolution

Question

I'm having trouble understanding how to use the resolution rule to prove if a statement is satisfiable or unsatisfiable.

I watched this course lecture on propositional resolution and unsatisfiability (linked with a time stamp to skip to the part in question):
"5.4 - Resolution Method - Propositional Resolution - [Introduction To Logic] By Michael Genesereth" https://www.youtube.com/watch?v=IpixwNupBIs#t=2m21s

For those that don't want to watch the video, my understanding is that he is saying that for a statement in conjunctive normal form (CNF) we can test whether the statement is satisfiable by repeatedly applying the simplifying resolution rule:
If there is a pair of clauses of the form $$(a \vee X)$$ $$(\neg a \vee Y)$$ this can be replaced by a single clause $$(X \vee Y)$$

The claim is that a statement is unsatisfiable if and only if repeated application of this rule leads to an empty clause.

But this doesn't make sense to me. I think there are some important details that are left out. For instance in the example given in the video, consider the statement with the clauses

1. $(p \vee q)$
2. $(p \vee \neg q)$
3. $(\neg p \vee q)$
4. $(\neg p \vee \neg q)$

By inspection, this is unsatisfiable. But let's find this using the resolution rule, following along with the video...

Applying the resolution rule on pair 1,2 gives: $p$

Then applying the resolution rule on pair 3,4 gives $\neg p$

So now we just have the clauses $p, \neg p$, which after applying the resolution rule one more time gives the empty clause.

That is how the example goes in the video. But look what happens if we apply the rule in another order:

Applying the resolution rule on pair 1,4 gives: $q \vee \neg q$

Then applying the resolution rule on pair 2,3 gives $\neg q \vee q$

So now we are just left with two clauses which are tautologies. So we simplified the statement to just $\top$. So by this order, it claims the statement is satisfiable.

Clearly something is wrong. What am I misunderstanding? Or is the course lecture leaving out something crucial?

Answer 1

You can see :

• Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990), Ch.3.3 Propositional Resolution, page 45-on

for a complete treatment of the proof system based on the Resolution Rule.

The proof system "expands" the set of cluases, applying the Resoultion Rule in order to add e new clause (a disjunction) to the original set of clauses. The rule has the property that "preserves stisfiability", i.e. the new set of clauses is satisfiable iff the original one is.

Thus, if after iterated applications of the rule the empty clause is produced, being it unsatisfiable (it is another way of writing $\bot$, i.e. a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.