Algorithmus zur Skolemisierung

Solange die Formel noch einen Existenzquantor enthält gehe folgendermaßen vor:

Suche den nächsten Existenzquantor von Rechts. Verwende ein neues, bisher nicht verwendetes Funktionssymbol und ersetze jedes Vorkommen der durch den Existenzquantor gebundenen Variable durch die Funktion dieser Variable und aller bisher ersetzten Variablen.