Die Idee der Skolemisierung besteht darin, die Objekte, deren Existenz postuliert wird, mit Termen zu benennen, die mit dem eingeführten Funktionssymbol gebildet werden. Die eingeführten neuen Funktionssymbole werden Skolem-Funktionssymbole genannt. Den Vorgang der Umformung einer Formel F nennt man die Skolemisierung von F, das Ergebnis der Umformung die Skolemform von F. Ist M eine Formelmenge, spricht man ebenfalls von der Skolemform von M und meint damit die Menge aller Skolemformen der Elemente von M.

Seien M eine Formelmenge und
            Msko eine Skolemform von M.

            M ist (un)erfüllbar genau dann wenn
            Msko (un)erfüllbar ist.

Umwandlung einer Formelmenge in Klauselform:

1. Skolemisierung: (siehe oben).
2. Pränexform:

   All x ( p(x) /\ All y q(x,y) )

   wird umgeformt in:

   All x All y ( p(x) /\ q(x,y) )

   Der Teil All x All y wird Präfix, der Teil p(x) /\ q(x,y) Matrix genannt.

3. Matrix in konjunktiver Normalform:

   Konjunktive Normalform = Konjunktion von Disjunktionen.

   All x All y ( p(x,y) => (q(x,y) /\ r(x,y)) )

   wird umgeformt in:

   All x All y ( [ ¬p(x,y) \/ q(x,y) ] /\ [ ¬p(x,y) \/ r(x,y) ] )

4. Klauselform:

   Die Formelmenge

   { All x All y ( [ ¬p(x,y) \/ q(x,y) ] /\ [ ¬p(x,y) \/ r(x,y) ] ) }

   wird umgeformt in die Formelmenge:

   { All x All y [ ¬p(x,y) \/ q(x,y) ],
  All x All y [ ¬p(x,y) \/ r(x,y) ] }

   Die Quantifikation wird als implizit angesehen, was die folgende Klauselmenge ergibt:

   { [ ¬p(x,y) \/ q(x,y) ], [ ¬p(x,y) \/ r(x,y) ] }

5. Rektifikation oder "standardization apart":

   Die Variablen in der Klauselmenge werden so umbenannt, daß keine zwei Klauseln eine gemeinsame Variable haben.

6. Implikative Darstellung von Klauseln oder Klauseln in Implikationsform:

   Die Klausel

   L1 \/ L2 ... \/ Lk

   wird dargestellt als

   C1 /\ ... /\ Cn => D1 \/ ... \/ Dm

   wobei

   • alle Ci und Dj positive Literale (Atome) sind,
   • wenn n = 0 ist (also kein Lh negativ), ist true die Prämisse der Implikation,
   • wenn m = 0 ist (also kein Lh positiv), ist false die Konklusion der Implikation,

Im folgenden wird stets die Klauselform angenommen

Darüber hinaus wird angenommen, daß alle Klauseln in Implikationsform bereichsbeschränkt sind, d.h. jede Variable, die in einem Dj vorkommt, kommt auch in einem Ci vor. Man kann jede Klauselmenge in eine bereichsbeschränkte Klauselmenge transformieren. Für viele Anwendungen ist das aber gar nicht nötig, weil die gegebene Formelmenge sowieso schon einer bereichsbeschränkten Klauselmenge entspricht.

Darstellung in PROLOG: Eine Klausel in Implikationsform wird wie folgt in PROLOG dargestellt: d. h. die Konjunktion und Disjunktion werden dargestellt wie in PROLOG üblich und die Implikation wie in den vorangehenden Kapiteln. Die positiven Literale (atomaren Formeln) true und false werden in PROLOG so dargestellt. Variablen werden als PROLOG-Variablen, Funktionssymbole und Konstanten als PROLOG-Funktionssymbole und PROLOG-Atome dargestellt.

Ein fehlerfreier Ablauf des Programmes P₉₃ setzt voraus, daß die Relationssymbole, die in Köpfen von Klauseln vorkommen, als dynamisch vereinbart werden.

Das Cut in der ersten Klausel von satisfiable ist notwendig, damit die zweite Klausel nicht zu früh aufgerufen wird, sondern erst, wenn alle vorhandenen Klauseln in Implikationsform erfüllt sind.

In assume kann der Aufruf von asserta nicht durch einen Aufruf von assert ersetzt werden: die "angenommenen" Fakten sollen kellerartig gespeichert werden, so daß zunächst das Faktum gelöscht wird, das zuletzt hinzugefügt wurde.

Das Programm P₉₅ ist korrekt und und vollständig für die Unerfüllbarkeit von endlichen Mengen von bereichsbeschränkten Klauseln in Implikationsform: Wenn satisfiable_level scheitert, dann ist die Klauselmenge unerfüllbar. Wenn die Klauselmenge unerfüllbar ist, dann scheitert satisfiable_level nach endlich vielen Schritten.

Das Programm ist außerdem korrekt für die Erfüllbarkeit, aber nicht vollständig für die Erfüllbarkeit: Wenn satisfiable_level erfolgreich terminiert, dann ist die Klauselmenge erfüllbar, und die Fakten in der PROLOG-Datenbasis repräsentieren ein Modell. Aber satisfiable_level terminiert nicht für jede erfüllbare Klauselmenge, zum Beispiel nicht für P₉₁. Es kann grundsätzlich auch kein Programm geben, das in allen Fällen mit der korrekten Antwort terminiert. Die Unerfüllbarkeit ist nur semi-entscheidbar, aber nicht entscheidbar.

Oft ist man nicht an der (Un)Erfüllbarkeit interessiert, sondern an der sogenannten Folgerungsbeziehung zwischen Formelmengen oder Formeln der Prädikatenlogik erster Stufe: ob aus einer Axiomenmenge A eine Formel F folgt.