Pro použití rezoluční metody na úsudky v PL1 je třeba nejdříve úsudek převést do Skolemovy klauzulární formy, což je konjunktivní normální forma.
Tuto následně rozepíšeme na řádky podobně jako u výrokové logiky.
Abychom mohli použít rezoluční pravidlo, tak musíme provádět tzv. unifikaci, tedy náhradu proměnných za termy.
