Derivation in the Resolution Proof System

Question

The clauses of our problem: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}

How can we conclude from these clauses to {}?

I can see that this cannot be satisfied, but I am unable to find a solution in the Resolution Proof System as it seems that [{x,y},{{¬x,¬y}] results in {x,y,¬y} or {y,x,¬x} and then we can derive {x,¬x} and {y,¬y}. It seems that this is obvious as (T or F) will be always T.

I know that this is not satisfiable because there is no solution that satisfies the problem.

Answer 1

You can apply Davis-Putnam. This applies resolution in an exhaustive fashion that eliminates propositional variables one at a time. It is a complete method that is able to deduce {} iff a propositional CNF formula is unsatisfiable.

Here is a good introduction https://www.fi.muni.cz/~popel/lectures/complog/slides/davis-putnam.pdf . To produce the proof one just needs to track the resolutions it does that contribute to the final derivation.

For this problem if you apply it in the order x, y, z one gets the proof:

 1. {x,y}   . input
 2. {x,z}   . input
 3. {y,z}   . input
 4. {~x,~y} . input
 5. {~x,~z} . input
 6. {~y,~z} . input
 7. {y,~z}  . resolve(x, 1, 5)
 8. {~y,z}  . resolve(x, 2, 4)
 9. {~z}    . resolve(y, 7, 6)
10. {z}     . resolve(y, 3, 8)
11. {}      . resolve(z, 10, 9)