Skończony, skolemizowany zbiór klauzul rachunku predykatów pierwszego rzędu odpowiada nieskończonemu zbiorowi wynikłemu z wszystkich możliwych podstawień zmiennych. „Dowolne” modele są jednak zbyt trudne – mogą one np. być nieprzeliczalne. Na szczęście zachodzi twierdzenie: Jeśli istnieje model dla danego zbioru formuł rachunku predykatów pierwszego rzędu, to istnieje taki model Herbranda.
Modele Herbranda są przeliczalne i składają się z termów. Tak więc nieskończony zbiór klauzul będzie przeliczalnym zbiorem klauzul rachunku zdań.
Dodajmy do rezolucji dodatkową zasadę – zasadę substytucji – mówiącą, że możemy podstawić dowolne wyrażenie za daną zmienną – i będziemy podstawiać w taki sposób że kiedyś podstawimy wszystko co podstawić można w każde możliwe miejsce (czyli nałożymy na podstawienia jakiś porządek i będziemy podstawiać w końcu do każdej klauzuli którą mamy). Zgodnie z twierdzeniem o zwartości każdy sprzeczny zbiór formuł rachunku zdań ma sprzeczny podzbiór skończony. Tak więc odpowiednio podstawiając w końcu uzyskamy taki podzbiór, a że dla rachunku zdań rezolucja jest zupełna, razem z taką regułą dostajemy system zupełny.