Resolution on set of clauses

Question

Given this set of clauses: $\neg \phi = (\neg T \lor \neg Y)\land (S \lor \neg X ) \land (\neg X \lor Z \lor \neg Y) \land(X \lor T) \land (Y \lor U) \land (Y \lor \neg V)\land \neg S \land V$

I want to reach the empty set in order to prove a tautology using resolution. Starting with any of the clauses I can reach the empty set except one, which is the clause: $(\neg X \lor Z \lor \neg Y)$

$\neg X \lor Z \lor \neg Y \\ T \lor Z \lor \neg Y\\ X \lor Z \lor \neg Y \\ S \lor Z \lor \neg Y \\ Z \lor\neg Y \\ Z \lor \neg V \\ Z $

And then I'm stuck I can't infer more clauses. Why is this? Shouldn't resolution work with any starting clause?

Answer 1

See Resolution :

The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture follows from the axioms.

We can apply the rule to show that $γ⊨α$, that is to show that $⊨γ→α$ (i.e. $γ→α$ is valid) and this amounts to prove that $γ∧¬α$ is unsatisfiable.

Or we can use ti to show that a formula $\alpha$ is valid, applying it to $\lnot \alpha$.

---

Thus, applying the rule to :

1) $(¬T∨¬Y)$

2) $(S∨¬X)$

3) $(¬X∨Z∨¬Y)$

4) $(X∨T)$

5) $(Y∨U)$

6) $(Y∨¬V)$

7) $¬S$

8) $V$

we have :

9) $¬X$ --- from 7) and 2)

10) $T$ --- from 4) and 9)

11) $¬Y$ --- from 1) and 10)

12) $¬V$ --- from 6) and 11)

13) $\{ ¬V, V \} = \square$ --- from 8) and 12)

---

If we want to apply the "systematic" procedure, we have to start with the set of clauses :

$\{ 1-6 \}$

We apply resolution to the "simple" cases :

• 6) and 8) : replaced by $Y$, and

• 7) and 2) : replaced by $\lnot X$

After the first two moves, the set of clauses is :

$\{ ¬T∨¬Y, ¬X∨Z∨¬Y, X∨T, Y∨U, \lnot X, Y \}$.

Now we have to use $Y$ with the first two, producing : $\lnot T$ and $¬X∨Z$, and use $\lnot X$ with the third one, producing $T$.

After the new couple of moves the set of clauses has been reduced to :

$\{ ¬T, ¬X∨Z, T, Y∨U \}$.

And now we have finished; there is no truth assignment to the propositional variables that can simultaneously satisfy all the clauses in the set, because it contains both $T$ and $\lnot T$.

Answer 2

In your example, you don't start with "¬X∨Z∨¬Y". You start with the set of clauses which has as its members each conjunct of the the conjunction you've listed.

If you check your other proofs you'll almost surely find that "¬X∨Z∨¬Y" does not appear anywhere in the proof. If it did, then you would have to have some way to cancel Z or equivalently, you would have some clause which has ¬Z in it. However, you don't have this, and consequently there is no way to resolve what you have to the empty set. Therefore, you can't write a proof using resolution which has "¬X∨Z∨¬Y" in it.