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 mit Variablen, die keinen Quantifikator, kurz Quantor zur Existenz hat, also ohne „es existiert“. Diese Form wurde nach dem norwegischen Mathematiker Albert Thoralf Skolem (1887–1963) benannt.

Logische Formeln 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 in die Klausel-Normalform umgeformt werden soll oder bei der Erzeugung eines Herbrand-Universums.

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

Algorithmus zum Erzeugen der Skolemform

Eine Formel 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 wird der folgende Algorithmus anwendet:

  1. habe die Form
  2. Setze
  3. Die Schritte werden wiederholt, bis keinen Existenzquantor mehr enthält.

steht für eine beliebige Formel , in der durch ersetzt wurde. ist ein in noch nicht vorkommendes -stelliges Funktionssymbol. Die Stelligkeit von ist bestimmt durch die Anzahl der Allquantoren vor dem zu skolemisierenden Symbol. Nullstellige Funktionssymbole sind Konstanten. heißt auch Skolemfunktion, im Fall ist eine Skolemkonstante.

Als Ergebnis erhält man die Formel in Skolemform . Andere Bezeichnungen sind Skolemisierung von 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

ist in bereinigter Pränexform. Der oben aufgeführte Algorithmus führt zu folgenden Schritten:

  • Zuerst wird durch die neu eingeführte nullstellige Funktion ersetzt:
  • wird danach als Ersetzung für eingeführt:
  • Dann wird ersetzt. Dafür wird die einstellige Funktion eingeführt. Sie erhält als Argument die per Allquantor gebundene Variable , da der Allquantor vor dem Existenzquantor steht.

Nun liegt die Formel in Skolemform mit den Konstanten , und dem einstelligen Funktionssymbol vor.