Skolemform

existenquantor-freie Darstellung in der Prädikatenlogik

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 „für alle gilt“.

Algorithmus zum Erzeugen der Skolemform

Bearbeiten

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

Bearbeiten

  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.