Kategorie

A B C D E
F G H I J
K L M N O
P Q R S T
U V W X Y
Z 0      

skolemform

sa sb sc sd se sf sg sh si sj sk sl sm
sn so sp sq sr ss st su sv sw sx sy sz

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.
Als Ergebnis erhält man die Formel F in Skolemform(el). Andere Bezeichnungen sind Skolemisierung von F oder auch Skolemsche Normalform.

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.

Impressum

Datenschutzerklärung