W rachunku predykatów pierwszego rzędu, niech jeśli jest spełnialne, to spełnialne jest też dowolne podstawienie W szczególności jeśli rezolwujemy z a \sigma jest unifikatorem i to oraz są spełnialne. Dalej prowadzi to do przypadku analogicznego do rachunku zdań: jeśli są spełnialne przez model gdzie jest prawdziwe, to jest spełnialne, a więc również osłabione jeśli są spełnialne przez model, gdzie jest faszywe, to jest spełnialne, a więc również osłabione
Dowód zupełności rezolucji w rachunku zdań Udowodnijmy, że jeśli dany zbiór klauzul (po zastosowaniu wszystkich reguł dla eliminacji spójników) jest sprzeczny, dojdziemy za pomocą rezolucji do klauzuli pustej.
Weźmy dowolną zmienną Są trzy grupy klauzul: zawierające zawierające oraz nie zawierające ani jednego ani drugiego. Klauzule zawierające zarówno jak i są oczywiście spełnialne i nie będziemy się nimi zajmować:
Dla każdego wartościowania sprzeczne jest albo któreś albo któreś albo też któreś Utwórzmy wszystkie klauzule przez rezolucje względem
Teraz udowodnijmy, że sprzeczny jest zbiór
Jeśli w wartościowaniu któreś nie było spełnione, to nowy zbiór – ponieważ też zawiera tę klauzulę – też nie spełnia tego wartościowania.