Database Reference
In-Depth Information
Der Resolutionskalkul arbeitet im Gegensatz z.B. zu der Methode der Wahr-
heitstafeln nicht auf beliebigen Formeln, sondern auf Formeln in Klauselform (vgl.
Def. 3.67). Der Resolutionskalkul (fur die Aussagenlogik) hat nur eine einzige Infe-
renzregel, die Resolutionsregel.
10
Die (aussagenlogische Variante der)
Resolutions-
regel
ist:
{
L, K
1
,...,K
n
}
{¬
L, M
1
,...,M
m
}
{
K
1
,...,K
n
,M
1
,...,M
m
}
Dabei heißen die Klauseln
{
L, K
1
,...,K
n
}
und
{¬
L, M
1
,...,M
m
}
Elternklauseln
,
die abgeleitete Klausel
{
K
1
,...,K
n
,M
1
,...,M
m
}
heißt
Resolvente
, und die Lite-
rale L und
L sind die
Resolutionsliterale
.
Ziel der Resolution ist es, einen elementaren Widerspruch abzuleiten, der der
leeren Klausel
¬
entspricht. Im Resolutionskalkul wird die leere Klausel meistens
durch reprasentiert. Jede abgeleitete Resolvente kann wieder als Elternklausel fur
einen neuen Resolutionsschritt verwendet werden. Gelingt es, aus einer Klauselmen-
ge
{}
K
die leere Klausel abzuleiten, so ist
K
unerfullbar. Umgekehrt gibt es fur jede
unerfullbare Klauselmenge
K
eine Resolutionsableitung der leeren Klausel aus
K
.
Dies bedeutet, dass der Resolutionskalkul
korrekt
und
widerlegungsvollstandig
ist.
Graphisch stellen wir einen Resolutionsschritt so dar, dass wir die Resolvente
mit den daruber stehenden Elternklauseln durch Kanten miteinander verbinden und
dabei die Resolutionsliterale durch Unterstreichen markieren. Z.B. stellen
{
A,
¬
B,C
}
{
A, B,
¬
D
}
{
A
}
{¬
A
}
{
A, C,
¬
D
}
zwei Resolutionsschritte dar. Der rechts dargestellte Resolutionsschritt leitet die
leere Klausel
ab; daraus folgt, dass die Klauselmenge
{{
A
}
,
{¬
A
}}
(die ja A
∧¬
A
reprasentiert) unerfullbar ist.
Selbsttestaufgabe 3.77 (Haustier 4)
Beweisen Sie mittels Resolution, dass die
Vermutung von Herrn Meier eine logische Folgerung aus seinen drei Uberlegungen
ist (vgl. Selbsttestaufgaben 3.24, 3.32 und 3.68).
Die pradikatenlogische Version der Resolution berucksichtigt, dass die Literale
in der Klauseldarstellung einer PL1-Formel Terme mit Variablen enthalten konnen.
Statt Resolutionsliterale L und
¬
L mit identischem L zu verlangen, wird von zwei
L
ausgegangen, so dass L und L
Literalen L und
¬
unifizierbar sind. Die (volle)
Resolutionsregel
lautet damit
L, K
1
,...,K
n
}
{¬
{
L
,M
1
,...,M
m
}
σ(L)= σ(L
)
{
σ(K
1
),...,σ(K
n
),σ(M
1
),...,σ(M
m
)
}
10
Fur PL1 wird auch noch die so genannte
Faktorisierung
benotigt (vgl. Seite 66).
