Skolemform - LinkFang.de





Skolemform


Dieser Artikel oder Abschnitt ist nicht allgemeinverständlich formuliert. Die Mängel sind unter Diskussion:Skolemform beschrieben. Wenn du diesen Baustein entfernst, begründe dies bitte auf der Artikeldiskussionsseite und ergänze den automatisch erstellten Projektseitenabschnitt Wikipedia:Unverständliche Artikel#Skolemform um {{Erledigt|1=~~~~}}.
Dieser Artikel oder Abschnitt ist nicht ausreichend belegt.

Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will.

In der Skolemform sind keine Existenzquantoren ([math]\exists[/math]) mehr enthalten. Variablen, die an Existenzquantoren gebunden waren, werden durch neue Funktionssymbole ersetzt. Als Argumente bekommen die neuen Funktionssymbole die Variablen der Allquantoren ([math]\forall[/math]), die vor dem entfernten Existenzquantor standen.

Algorithmus zum Erzeugen der Skolemform

Man erhält eine Formel nach Skolem, wenn man auf eine bereinigte, pränexe Formel F folgende Umformungen anwendet:

Solange F einen Existenzquantor enthält:

{
F habe die Form:
[math]F=\forall y_1\forall y_2...\forall y_n \exists xG[/math]
Setze:
[math]F := \forall y_1\forall y_2...\forall y_nG\left[x/f\left(y_1,...,y_n\right)\right][/math]
Dabei sei f ein in F noch nicht vorkommendes n-stelliges Funktionssymbol. Die Stelligkeit der Funktion wird dabei bestimmt durch die Allquantoren vor dem zu skolemisierenden Symbol, wobei die Funktion jeweils auf den nächsten vorhergehenden Allquantor zu beziehen ist. Nullstellige Funktionssymbole sind Konstanten.
}

Hinweis: [math]G\left[x/w\right][/math] steht hier für die Formel G, in der x durch w ersetzt wurde. f heißt Skolemfunktion, im Fall [math]n = 0[/math] Skolemkonstante.

Als Ergebnis erhält man die Formel F in Skolemform. 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. Sie erhält zwar die Erfüllbarkeit der Formel und ist somit erfüllbarkeitsäquivalent, ist aber nicht modellerhaltend. Dies bedeutet, dass eine Interpretation, welche die ursprüngliche Formel erfüllt, nicht notwendigerweise auch die skolemisierte Formel erfüllt (siehe hierzu auch Logik), was aufgrund des neu zu interpretierenden Funktionssymbols auch nicht verwunderlich ist.

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 (BPF).

Durch Anwendung des oben aufgeführten Algorithmus erhält man:

  • Im ersten Schritt wird [math]\exists{x}[/math] durch die neu eingeführte nullstellige Funktion [math]a[/math] ersetzt:

[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:

[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.

[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 einem einstelligen Funktionssymbol [math]f(w)[/math] vor.


Kategorien: Logik

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Skolemform (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.