Skólem normálformára hozásnál az egzisztenciális kvantorral ellátott változót egy megfelelően választott konstansra vagy függvényre cseréljük.

Változók standardiázálása során a kvantorral ellátott változókat átnevezzük, hogy a formulában minden változó megegyezzen.

Rezolúció segítségével ellentmondásos klózhalmazból az üres klóz levezethető.

Ha az logikai következménye, akkor   kontradikció.