Proving unsatisfiability with propositional resolution 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


*

*$(p \vee q)$

*$(p \vee \neg q)$

*$(\neg p \vee q)$

*$(\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?
 A: 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.
A: I think this algorithm should help you . You need to add the resolved clause to your set of clauses everytime you resolve and so your set of clauses grow. Also before adding, you need to make sure that when you resolve you do not end up generating the clause which you might have already generated before in the process of resolution or( which already exists in your set of clauses). Look the algorithm pictures
Unsatisfiability algo pic
Saturation Algo pic
