Refutation theorem says that .

In words: the set of formulas (gamma) has as consequence if and only if the system composed by together with is unsatisfiable.

That about proving unsatisfiability is a different topic, and a rather long one, like its name suggests. One of the easiests methods to do that is using clause resolution trees.

Daniel Clemente Laboreo 2005-05-17