Complétude de la méthode de résolution

Soit $\Sigma$ un ensemble de clauses contradictoires. Alors il existe un arbre de réfutation de $\Sigma$.