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