Skolemform
Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Die Skolemform ist ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will.Man erhält eine Formel nach Skolem, wenn man auf eine bereinigte, pränexe Formel F folgende Umformungen anwendet:
- WHILE F enthält einen Existenzquantor {
- F habe die Form:
- Setze:
- mit f sei ein in F noch nicht vorkommendes n-stelliges Funktionssysmbol. Nullstellige Funktionssymbole sind Konstanten.
- }
- Hinweis:
- steht hier für die Formel G in der x durch w ersetzt wurde. f heisst Skolemfunktion, im Fall n=0 Skolemkonstante.
Beispiel
- ist in bereinigter und pränexer Form. Durch Anwendung des oben aufgeführten Algorithmus erhält man:
- mit a, b Konstanten und f(w) ein 1-stelliges Funktionssymbol.