Si è già visto che, per ogni formula del primo ordine $H$, esiste una formula $Ex^S(H)$ chiusa e in forma normale di Skolem tale che
$$ H \text{ è soddisfacibile}\iff Ex^S(H) \text{ è soddisfacibile} $$
Poi, considerando una formula in forma di Skolem,
$$ \varphi=\forall x_1\dots \forall x_n\psi $$
siccome la matrice $\psi$ non contiene quantificatori, la si può trasformare in una CNF.
Dunque, complessivamente, data una qualunque formula del primo ordine, si può costruire una formula chiusa in forma di Skolem con matrice in CNF, che è equisoddisfacibile alla formula di partenza e può essere rappresentata come insieme di clausole (supponendo implicitamente che tutte le variabili presenti nelle clausole di tale insieme siano quantificate universalmente).
Cià consente di applicare il calcolo di risoluzione per studiare la soddisfacibilità di una qualunque formula del primo ordine. Per estendere la risoluzione al caso prediativo, bisogna però introdurre alcune modifiche, che riguardano essenzialmente la gestione dei termini.
Ad esempio, se si considera la formula (in questo caso già chiusa)
$$ \forall x(A(x)\lor B(x))\land \forall z(A(f(c))\rarr C(x)) $$
e la si trasforma in forma di Skolem con matrice in CNF,
$$ \varphi=\forall x((A(x)\lor B(X))\land (\neg A(f(c))\lor C(x))\} $$
si ha che $\varphi$ è rappresentata dall’insieme di clausole:
Alle clausole $\cal C_1$ e $\cal C_2$ è possibile applicare la regola di risoluzione (analogamente al caso proposizionale) se si istanzia la variabile $x$ con il termine $f(c)$:
$$ S_\varphi[f(c)/x]=\{\{A(f(c)), B(f(c))\}, \{\neg A(f(c)), C(f(c))\}\} $$
Adesso le due clausole contengono i letterali complementari $A(f(c))$ e $\neg A(f(c))$, sui quali si applica la risoluzione:
$$ \cfrac{\{A(f(c)), B(f(c))\} \ \ \ \ \{\neg A(f(c)), C(f(c))\}}{B(f(c)), C(f(c))}\small{\text{ris}} $$
Per generalizzare il ragionamento, bisogna introdurre un metodo per individuare le sostituzioni da effettuare al fine di poter applicare la regola di risoluzione.