Next: 8.4 Com demostrar la Up: 8.3 Altres formes de Previous: 8.3.1 Força bruta Contents
El teorema de refutació diu que
.
En paraules: el conjunt de fórmules 
(gamma) té com
conseqüència a 
si i només si el sistema format per
junt amb 
és insatisfactible.
El com demostrar la insatisfactibilitat és un altre tema, bastant llarg, tal com el seu nom suggereix. Un dels mètodes fàcils d'usar és el de l'arbre de resolució clausular.