1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ Thank you, but I know how to do that as I said: "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)$", and my question is shouldn't resolution work starting with any clause? $\endgroup$ – εν οίδα ότι ουδέν οίδα Nov 28 '14 at 11:50
  • $\begingroup$ @Panayiotis - refer to the quotatio from Wiki above : "resolution rule is applied to all possible pairs of clauses that contain complementary literals". So, if you use intelligence, you can folow the "path" that gives you teh solution, but the procedure is designed to be "automatized". In this case, you have to "join" all couples of clauses containig complementary literals. In this way, however you start, you will get always the same result. $\endgroup$ – Mauro ALLEGRANZA Nov 29 '14 at 20:05
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ But in principle, we can apply the resolution method also to a single formula. Recall that $\square$ is only a shorthand for $\bot$, i.e. for $p \land \lnot p$. Thus, if we apply the method to a formula that is a disjunction of formulae like $p \land \lnot p$, the method shows that it is unsatisfiable, i.e. the negation of a tautology. Otherwise, with a formula like $¬X∨Z∨¬Y$ the procedure simply shows us taht it is satisfiable (what was already easy to show without it ...). $\endgroup$ – Mauro ALLEGRANZA Nov 29 '14 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.