kus s on literaalide L ja L' üldiseim unifikaator. Resolutsioonireegel on (koos skolemiseerimisega) täielik esimest järku klassikalises predikaatarvutuses: valem A on tuletatav parajasti siis, kui tema eitusega samaväärsest disjunktide hulgast on resolutsioonmeetodil tuletatav tühi disjunkt.