Database Reference
In-Depth Information
{¬
sich-irren
(y)
}
{¬
Mensch
(x),
sich-irren
(x)
}
σ
1
{¬
Mensch
(y)
}
{
Mensch
(
Max
)
}
σ
2
Abbildung 3.6
Resolutionsableitung mit
σ
1
=
{x/y}
und
σ
2
=
{y/Max}
wobei σ allgemeinster Unifikator von L und L
ist. Dabei ist zu beachten, dass
die beiden Elternklauseln eines Resolutionsschrittes keine gemeinsamen Variablen
haben. Dies kann immer leicht dadurch erreicht werden, dass vor einem Resolu-
tionsschritt gegebenenfalls
Variablenumbenennungen
in den Elternklauseln vorge-
nommen werden (vgl. die Anmerkungen in der Fußnote zu Definition 3.67).
Wahrend in der Aussagenlogik das mehrfache Auftreten derselben atomaren
Formel wie z.B. in A
A automatisch durch die Verwendung der Mengenschreibweise
in der Klauselform eliminiert wird, wird fur die Widerlegungsvollstandigkeit der
Resolution in PL1 noch die folgende
Faktorisierungsregel
benotigt
∨
{
L, L
,K
1
,...,K
n
}
σ(L)= σ(L
)
{
σ(L),σ(K
1
),...,σ(K
n
)
}
wobei σ allgemeinster Unifikator von L und L
ist. Alternativ kann man die Resolu-
tionsregel auch so erweitern, dass die Faktorisierung dort gleich mit berucksichtigt
wird.
Beispiel 3.78 (Resolution)
Wir wollen die Folgerung
(
∀
x
Mensch(x)
⇒
sich-irren(x)
)
∧
Mensch(Max)
|
=
∃
y
sich-irren(y)
mittels Resolution beweisen. Die Klauseldarstellung der Pramisse und der negierten
Schlussfolgerung ist
{{¬
Mensch(x)
,
sich-irren(x)
}
,
{
Mensch(Max)
}
,
{¬
sich-irren(y)
}}
.
Die in Abbildung 3.6 angegebene Resolutionsableitung ist in diesem Fall eine so ge-
nannte SLD-Resolutionsableitung, wie sie dem logischen Programmieren zugrunde
liegt (z. B. [225, 204]). Sie liefert nicht nur einen Beweis, sondern mit der Kompo-
sition σ
2
◦
σ
1
(y)=
Max
fur die existenzquantifizierte Variable y,fur die die instantiierte Schlussfolgerung
gilt. Um
σ
1
der verwendeten Unifikatoren auch eine Belegung σ
2
◦
y
sich-irren(y)
als gultige Schlussfolgerung zu zeigen, haben wir also mit-
tels (SLD-)Resolution einen konstruktiven Nachweis gefuhrt und
sich-irren(Max)
als Schlussfolgerung bewiesen.
∃
