Citation Hunt

"

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

Logische Formeln ${\displaystyle F}$ 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 ${\displaystyle F}$ in die Klausel-Normalform umgeformt werden soll, oder bei der Erzeugung eines Herbrand-Universums.

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