Skolemization

Logik hat Quantoren: "Für alle" ($\forall$) und "Es existiert" ($\exists$). Existenz-Quantoren sind nervig für Computer. "Es existiert ein x, sodass x > 5." Computer wollen Namen. Welches x? Thoralf Skolem (1920) hatte die Idee: Wir erfinden einfach einen Namen (eine Skolem-Konstante). Aus "Es gibt ein Monster" wird "Monster_1 existiert". Aus "Zu jedem Menschen gibt es einen Vater" ($\forall m \exists v $) wird "Vater(m)". Hier wird v zu einer Skolem-Funktion. Wir eliminieren alle $\exists$ und ersetzen sie durch Funktionen. Das macht die Formel einfacher zu verarbeiten (für Resolution).

Merksatz: Ein Verfahren in der Prädikatenlogik, bei dem Existenzquantoren durch neu eingeführte Funktionssymbole (Skolem-Funktionen) ersetzt werden, um eine Formel in eine rein universell quantifizierte Form zu überführen.

Wenn du eine SQL-Datenbank designst (ID-Generation). "Jeder Kunde hat eine ID." Du sagst nicht "Es existiert eine ID". Du sagst: getID(Customer). Das ist eine Skolem-Funktion. Sie erzeugt das Objekt, das existieren muss.

1. Erhalt der Erfüllbarkeit

Skolemization ist nicht äquivalent. $A \not\equiv Skolem(A)$. Aber sie ist erfüllbarkeitsäquivalent. $A$ hat ein Modell $\iff Skolem(A)$ hat ein Modell. Das reicht für Beweise (Widerspruchsbeweis). Wenn $Skolem(A)$ unerfüllbar ist, war auch $A$ unerfüllbar.

2. Dependency

Wichtig: Die Skolem-Funktion hängt von allen All-Quantoren ab, die davor stehen. $\forall x \exists y (y > x)$. -> $y = f(x)$. (Abhängig). $\exists y \forall x (y > x)$. -> $y = c$. (Konstante, unabhängig).

1. Skolem-Normalform (SNF)

Die SNF ist eine Formel, die nur noch All-Quantoren am Anfang hat ($\forall x \forall y \dots$) und deren Body in Konjunktiver Normalform (CNF) vorliegt. Der Prozess:

Prenex-Form: Alle Quantoren nach vorne.
Skolemization: Alle $\exists$ durch Funktionen ersetzen.
Matrix-Transformation: Den Rest in CNF bringen. In der Produktion (SAT/SMT-Solver wie Z3) ist dies der erste Schritt. Ohne Skolemization könnten diese Tools keine komplexen mathematischen Beweise führen, da sie intern nur mit Klauseln (Mengen von Literalen) arbeiten können.

2. Functional Replacement & Search Space

Warum ist die Skolem-Funktion $f(x)$ besser als der Quantor $\exists y$? Weil der Algorithmus nun Unifikation nutzen kann. Anstatt zu "suchen", welcher Wert für $y$ passt, "rechnet" der Computer mit dem Symbol $f(x)$. Wenn er später auf $f(5)$ trifft, weiß er: "Aha, das ist das $y$, das zu $x=5$ gehört." Das schneidet riesige Äste des Suchraums ab, weil wir nicht mehr raten müssen, ob $y$ existiert – wir behandeln es wie einen festen (wenn auch unbekannten) Wert.

3. Preservation of Satisfiability (Equisatisfiability)

Ein häufiger Experten-Fehler: Zu glauben, Skolemization sei logisch äquivalent. Betrachte $\exists x P(x)$. Skolemisiert: $P(c)$. Wenn $P(c)$ wahr ist, ist auch $\exists x P(x)$ wahr. Aber: Wenn $P(c)$ falsch ist, könnte $\exists x P(x)$ trotzdem wahr sein (für ein anderes $x \neq c$). Deshalb ist Skolemization nur für den Widerspruchsbeweis geeignet: Wenn wir zeigen, dass $Skolem(F)$ niemals wahr sein kann (unerfüllbar), dann wissen wir sicher, dass auch die Originalformel $F$ niemals wahr sein kann. Für "Vorwärts-Beweise" ist sie gefährlich und meist falsch.