8.3.2 Refutation theorem

Refutation theorem says that $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$.

In words: the set of formulas $\Gamma$ (gamma) has as consequence $A$ if and only if the system composed by $\Gamma$ together with $\neg A$ 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.