imported>Cheongnyangni-dong: Dieser Artikel braucht sicherlich Belege, aber doch bitte Fachliteratur und keine Folien, die nächstes Jahr vielleicht nicht mehr da sind. Die letzte Textänderung von Leher Brit wurde verworfen und die Version 245598096 von 132.231.141.109 wiederhergestellt.

2025-08-04T19:08:15Z

Dieser Artikel braucht sicherlich Belege, aber doch bitte Fachliteratur und keine Folien, die nächstes Jahr vielleicht nicht mehr da sind. Die letzte Textänderung von Leher Brit wurde verworfen und die Version 245598096 von 132.231.141.109 wiederhergestellt.

Neue Seite

{{Belege fehlen}}

Die '''Skolemform''' gehört zu den mathematischen Darstellungen der [[Prädikatenlogik]], um [[Argument]]e zu formalisieren und auf ihre Gültigkeit zu überprüfen. Die Skolemform ist eine [[logische Formel]] <math>F</math> mit [[Variable (Mathematik)|Variable]]n, die keinen Quantifikator, kurz [[Quantor]] zur Existenz hat, also ohne <math>\exists</math> „es existiert“. Diese Form wurde nach dem norwegischen Mathematiker [[Albert Thoralf Skolem]] (1887–1963) benannt.

Logische Formeln <math>F</math> sind erfüllbar, wenn mindestens eine Belegung der Variablen zu einer wahren [[Aussage (Logik)|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 <math>F</math> in die [[Klausel-Normalform]] umgeformt werden soll, oder bei der Erzeugung eines [[Herbrand-Universum]]s.

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

== Algorithmus zum Erzeugen der Skolemform ==
Eine Formel <math>F_0</math> 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 <math>F</math> wird der folgende Algorithmus anwendet:

# <math>F</math> habe die Form <math>F=\forall y_1\forall y_2 \ldots \forall y_n \exists xG</math>.
# Setze <math>F' := \forall y_1\forall y_2 \ldots \forall y_nG\left[x/f\left(y_1,\ldots,y_n\right)\right]</math>.
# Die Schritte werden wiederholt, bis <math>F'</math> keinen Existenzquantor <math>\exists</math> mehr enthält.

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

Als Ergebnis erhält man die Formel <math>F</math> in Skolemform <math>F'</math>. Andere Bezeichnungen sind Skolemisierung von <math>F</math> 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äquivalenz|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 ==
<math>F:=\exists x\exists y\forall w\exists z\left(P\left(x,y,w\right)\vee Q\left(z,x\right)\right)</math>
ist in bereinigter Pränexform. Der oben aufgeführte [[Algorithmus]] führt zu folgenden Schritten:

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

Nun liegt die Formel in Skolemform mit den Konstanten <math>a</math>, <math>b</math> und dem einstelligen Funktionssymbol <math>f</math> vor.

[[Kategorie:Logik]]
[[Kategorie:Normalform]]

Skolemform - Versionsgeschichte

imported>Cheongnyangni-dong: Dieser Artikel braucht sicherlich Belege, aber doch bitte Fachliteratur und keine Folien, die nächstes Jahr vielleicht nicht mehr da sind. Die letzte Textänderung von Leher Brit wurde verworfen und die Version 245598096 von 132.231.141.109 wiederhergestellt.