Database Reference
In-Depth Information
Fur die (pradikatenlogische Variante der) Resolution (s. Abschnitt 3.6) mussen wir
die Formeln noch weiter vereinfachen. Existenzquantoren werden durch
Skolemi-
sierung
eliminiert. Tritt ein Existenzquantor nicht im Geltungsbereich eines All-
quantors auf, wird der Existenzquantor einfach weggelassen und alle Auftreten der
quantifizierten Variablen werden durch eine
neue
Konstante - eine sog.
Skolemkon-
stante
- ersetzt. Ist c eine neue Konstante, so ist z.B. P (c) die Skolemisierung von
∃
xP (x).
Tritt dagegen
x im Geltungsbereich der allquantifizierten Variablen y
1
,...,y
n
auf, so werden alle Auftreten von x durch den Term f (y
1
,...,y
n
) ersetzt. Dabei
muss f ein
neues
Funktionssymbol sein; f wird auch
Skolemfunktion
genannt (vgl.
z.B. [83]). Ist f ein neues Funktionssymbol, so ist z.B.
∃
∀
yP(f (y),y) die Skolemi-
sierung von
xP(x, y). Die folgende Tabelle gibt weitere Beispiele zur Skolemi-
sierung an, wobei c, c
,f,g jeweils neue Skolemkonstanten bzw. Skolemfunktionen
sind:
∀
y
∃
Formel
skolemisierte Formel
yP(y, c, c
)
∃
x
∃
v
∀
yP(y, x, v)
∀
∃
x
∀
y
∃
vP(y, x, v)
∀
yP(y, c, f(y))
∀y ∃x ∃vP(y, x, v)
∀yP(y, g(y),f(y))
Q(f (y
1
,y
2
),y
2
)
Die vollstandige Skolemisierung einer Formel F entfernt alle Existenzquantoren aus
F und liefert eine Formel F
,die
erfullbarkeitsaquivalent
zu F ist, d.h. F ist erfull-
bar genau dann, wenn F
erfullbar ist. Die beiden folgenden Schritte schließen nun
an die vier obigen an:
∀
y
1
∀
y
2
∃
xP(x, y
1
)
∨
Q(x, y
2
)
∀
y
1
∀
y
2
P (f (y
1
,y
2
),y
1
)
∨
5. Alle Existenzquantoren werden durch Skolemisierung entfernt.
6. Da alle auftretenden Variablen jetzt allquantifiziert sind, konnen alle Allquan-
toren weggelassen werden.
Die so erhaltene Formel enthalt nur noch Literale und die Junktoren
.
Mithilfe der de Morganschen Regeln (Theorem 3.35) konnen die folgenden Normal-
formen erzeugt werden.
∧
und
∨
Definition 3.66 (disjunktive und konjunktive Normalform)
Eine Formel F
ist in
disjunktiver Normalform (DNF)
, wenn sie von der Form
K
1
∨
...
∨
K
n
ist, wobei die K
i
Konjunktionen von Literalen sind. F ist in
konjunktiver Normal-
form (KNF)
,wennsievonderForm
D
1
∧ ...∧ D
n
ist, wobei die D
i
Disjunktionen von Literalen sind.
