When we use the Resolution Principle we try to deduce a logical consequences from 2 clauses.

The set of clauses is unsatisfable , if we get a empty clause.

What i dont understand is : in practice, an empty clause is simply false. So, what proof that the set of clauses is unsatisfable is a paradox , am i correct ?

ps:i intend the paradox as the fact that a model of the clauses should be the model of a false statement.

pss: if it's true. How is possible that a logical consequence can lead to a paradox ? This seems mathematically strange to me :S

  • 2
    $\begingroup$ The empty clause is simply a contradiction: thus, by definition, it is unsatisfiable. $\endgroup$ – Mauro ALLEGRANZA Feb 13 '18 at 12:50
  • $\begingroup$ The resolution rule resolves two clauses $\lnot p \lor q$ and $p \lor r$ deriving the "resolvent" $q \lor r$. It is a logical rule, and thus it is sound, i.e. derives true conclusion from true premises. Thus, if we derive the empty clause, i.e. $\bot$, we have proved that the originals et $S$ of clauses is unsatisfiable (i.e. contradictory) because only a contradiction con entail $\bot$. $\endgroup$ – Mauro ALLEGRANZA Feb 13 '18 at 13:00
  • $\begingroup$ Recall that $S \vDash \alpha$ (reading: the formula $\alpha$ is a logical consequence of the set $S$) means: every interpretation that satisfies all of $S$ also satisfies $\alpha$. If $\alpha$ is $\bot$, it is unsatisfiable. Thus, if we have $S \vDash \bot$, we have to conclude that also $S$ is unsat. $\endgroup$ – Mauro ALLEGRANZA Feb 13 '18 at 13:01
  • $\begingroup$ Conclusion: no paradox at all. $\endgroup$ – Mauro ALLEGRANZA Feb 13 '18 at 13:07
  • $\begingroup$ @MauroALLEGRANZA Sorry but I don't quite understand why 'Only a contradiction can entail ⊥'...the definition of logic entailment/consequence as I understand is that, (for $\psi \vDash \phi$)for all the truth assignments that satisfies $\psi$, they also satisfy $\phi$. But for ⊥ it will always be false, so how can there be any truth assignment that satisfies it? Even if $\psi$ is always false, the best we could say seem to be that $\psi$ is logically equivalent to ⊥, instead of entailing ⊥. $\endgroup$ – Daniel Mak Mar 22 '18 at 5:19

When you derive the empty clause from a set of clauses that indeed means that that set of clauses is not satisfiable.

However, when you try to figure out whether some statement $\varphi$ follows from a set of statements $\Gamma$, you first negate the statement $\varphi$, and then put everything into clauses. Then, when you derive the empty clause, you have shown that the set of statements $\Gamma \cup \{ \neg \varphi \}$ is unsatisfiable, and that means that $\varphi$ is a logical consequence of $\Gamma$.

In other words, to use the resolution method to check for logical consistency you set it up as kind of a proof by contradiction: assume that $\varphi$ is not true, and if that leads to a contradiction, then you have proven $\varphi$


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.