Database Reference
In-Depth Information
assoziativ, kommutativ und idempotent sind, ist die
Reihenfolge der Elemente in einer Disjunktion bzw. einer Konjunktion irrelevant,
und jedes mehrfache Auftreten eines Elements kann eliminiert werden. Genau diese
Eigenschaften leistet gerade die Mengendarstellung, bei der z.B. eine Disjunktion
von Literalen L
1
∨
Da die Junktoren
∨
und
∧
...
∨
L
n
dargestellt wird als Menge
{
L
1
,...,L
n
}
.
Definition 3.67 (Klausel, Klauselform)
Die Mengendarstellung der konjunkti-
ven Normalform heißt
Klauselform
.EineKNF-Formel
(L
1,1
∨
L
1,2
∨
...
∨
L
1,n
1
)
∧
...
∧
(L
m,1
∨
...
∨
L
m,n
m
)
wird in Klauselform also als
{{
L
1,1
,L
1,2
,...,L
1,n
1
}
, ...,
{
L
m,1
,...,L
m,n
m
}}
geschrieben. Die inneren Mengen von Literalen
werden als
Klauseln
bezeichnet; die gesamte Menge der Klauseln heißt
Klauselmenge
.
8
{
L
i,1
,L
i,2
,...,L
i,n
i
}
Zu jeder aussagenlogischen Formel gibt es also auch eine aquivalente Formel in Klau-
selform. Durch die angegebenen Umformungsschritte konnen wir daruber hinaus je-
de PL1-Formel in eine erfullbarkeitsaquivalente Formel in Klauselform uberfuhren.
Dies ist eine der Grundlagen fur das Resolutionsverfahren (Abschnitt 3.6).
Selbsttestaufgabe 3.68 (Haustier 3)
Reprasentieren
Sie
die
Formeln
aus
Selbsttestaufgabe 3.24 in Klauselform.
Uberfuhren Sie die Formel
Selbsttestaufgabe 3.69 (Normalform)
¬
(
¬
(A
⇒
(B
∨
C))
⇒
((B
∧
C)
⇒
A))
zunachst in konjunktive Normalform und dann in Klauselform.
Selbsttestaufgabe 3.70 (Klauselform)
Uberfuhren Sie die Formel
(
∀
x
Mensch(x)
⇒
sich-irren(x)
)
∧
Mensch(Max)
∧¬
(
∃
y
sich-irren(y)
)
in Klauselform.
Selbsttestaufgabe 3.71 (Normalformen)
Uberfuhren Sie die Formel
∃
y(
¬
P (y)
∨
R(y))
⇔∀
yS(y)
in Pranexform, verneinungstechnische Normalform, DNF und KNF.
8
Zur Beachtung: In einer Klauselform sind die Literale innerhalb einer Klausel implizit
disjunktiv
verknupft, wahrend die Klauseln
konjunktiv
verknupft sind! Da die Variablen in einer Klausel-
form implizit allquantifiziert sind, konnen gemaß Theorem 3.58 die Variablen in einer Klausel
umbenannnt werden, ohne dass sich die Sematik der Klauselform andert.
