Skolemform

Die Skolemform gehört zu den mathematischen Darstellungen der Prädikatenlogik, um Argumente zu formalisieren und auf ihre Gültigkeit zu überprüfen. Die Skolemform ist eine logische Formel $F$ mit Variablen, die keinen Quantifikator, kurz Quantor zur Existenz hat, also ohne $\exists$ „es existiert“. Diese Form wurde nach dem norwegischen Mathematiker Albert Thoralf Skolem (1887–1963) benannt.

Logische Formeln $F$ sind erfüllbar, wenn mindestens eine Belegung der Variablen zu einer wahren Aussage führt. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform, da jede Formel genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Die Skolemform ist ferner ein praktischer Zwischenschritt, wenn eine logische Formel $F$ in die Klausel-Normalform umgeformt werden soll oder bei der Erzeugung eines Herbrand-Universums.

Die Skolemform hat keine Existenzquantoren $\exists$, alle Ausdrücke $\exists x$ sind aufgelöst. $\exists x$ bedeutet „es existiert mindests ein $x$“ – mit einer bestimmten Eigenschaft. Variablen $x$, die an Existenzquantoren $\exists$ gebunden sind, werden durch neue Funktions- oder Konstantensymbole ersetzt. Die Argumente der neuen Funktionssymbole haben Allquantoren $\forall {}x$ – sprich: "es gilt für alle $x$".

Algorithmus zum Erzeugen der Skolemform

Eine Formel $F_{0}$ wird in die Skolemform gebracht, indem sie als bereinigte Normalform in der Pränex-Normalform dargestellt wird, kurz als bereinigte Pränexform. Auf diese Formel $F$ wird der folgende Algorithmus anwendet:

1. $F$ habe die Form $F=\forall y_{1}\forall y_{2}...\forall y_{n}\exists xG$
2. Setze $F':=\forall y_{1}\forall y_{2}...\forall y_{n}G\left[x/f\left(y_{1},...,y_{n}\right)\right]$
3. Die Schritte werden wiederholt, bis $F'$ keinen Existenzquantor $\exists$ mehr enthält.

$G\left[x/w\right]$ steht für eine beliebige Formel $G$, in der $x$ durch $w$ ersetzt wurde. $f$ ist ein in $F$ noch nicht vorkommendes $n$-stelliges Funktionssymbol. Die Stelligkeit $n$ von $f$ ist bestimmt durch die Anzahl der Allquantoren $\forall$ vor dem zu skolemisierenden Symbol. Nullstellige Funktionssymbole sind Konstanten. $f$ heißt auch Skolemfunktion, im Fall $n=0$ ist $f$ eine Skolemkonstante.

Als Ergebnis erhält man die Formel $F$ in Skolemform $F'$. Andere Bezeichnungen sind Skolemisierung von $F$ oder auch Skolem’sche Normalform.

Zu beachten ist, dass bei der beschriebenen Umformung nicht notwendigerweise die logische Äquivalenz erhalten bleibt. Die Umformung erhält zwar die Erfüllbarkeit der Formel und ist somit erfüllbarkeitsäquivalent, ist aber nicht modellerhaltend: Weil das Funktionssymbol neu interpretiert werden muss, erfüllt eine Interpretation, welche die ursprüngliche Formel erfüllt, nicht notwendigerweise auch die skolemisierte Formel.

Beispiel

$F:=\exists x\exists y\forall w\exists z\left(P\left(x,y,w\right)\vee Q\left(z,x\right)\right)$ ist in bereinigter Pränexform. Der oben aufgeführte Algorithmus führt zu folgenden Schritten:

• Zuerst wird $\exists {x}$ durch die neu eingeführte nullstellige Funktion $a$ ersetzt:
  $F':=\exists y\forall w\exists z\left(P\left(a,y,w\right)\vee Q\left(z,a\right)\right)$
• $b$ wird danach als Ersetzung für $\exists {y}$ eingeführt:
  $F'':=\forall w\exists z\left(P\left(a,b,w\right)\vee Q\left(z,a\right)\right)$
• Dann wird $\exists {z}$ ersetzt. Dafür wird die einstellige Funktion $f$ eingeführt. Sie erhält als Argument die per Allquantor gebundene Variable $w$, da der Allquantor vor dem Existenzquantor steht.
  $F''':=\forall w\left(P\left(a,b,w\right)\vee Q\left(f\left(w\right),a\right)\right)$

Nun liegt die Formel in Skolemform mit den Konstanten $a$, $b$ und dem einstelligen Funktionssymbol $f(w)$ vor.