Database Reference
In-Depth Information
← Tante
(
susanne,t
)
.
Tante
(
x
1
,y
1
)
← Weiblich
(
y
1
)
, Vater
(
x
1
,z
1
)
, Geschwister
(
y
1
,z
1
)
.
σ
1
=
{x
1
/susanne,y
1
/t}
← Weiblich
(
t
)
, Vater
(
susanne,z
1
)
, Geschwister
(
t, z
1
)
.
Weiblich
(
sabine
)
.
σ
2
=
{t/sabine}
← Vater
(
susanne,z
1
)
, Geschwister
(
sabine,z
1
)
.
Vater
(
susanne, hans
)
.
σ
3
=
{z
1
/hans}
← Geschwister
(
sabine, hans
)
.
Geschwister
(
v
2
,w
2
)
← Vater
(
v
2
,q
2
)
, Vater
(
w
2
,q
2
)
.
σ
4
=
{v
2
/sabine,w
2
/hans}
← Vater
(
sabine,q
2
)
, Vater
(
hans,q
2
)
.
Vater
(
sabine, franz
)
.
σ
5
=
{q
2
/franz }
← Vater
(
hans, franz
)
.
Vater
(
hans, franz
)
.
σ
6
=
{}
Abbildung 9.3
SLD-Ableitung zu Beispiel 9.13
Beispiel 9.13 (SLD-Resolution)
Programm und Anfrage seien wie folgt:
P
:
Vater
(
hans
,
franz
).
Vater
(
sabine
,
franz
).
Vater
(
susanne
,
hans
).
Weiblich
(
sabine
).
Weiblich
(
susanne
).
Geschwister
(v, w) ←
Vater
(v, q),
Vater
(w, q).
Tante
(x, y) ←
Weiblich
(y),
Vater
(x, z),
Geschwister
(y, z).
Tante
(
susanne
,t).
Dabei sind q, t, v, w, x, y, z Variablen,
Vater
,
Geschwister
,
Tante
binare Pradikaten-
symbole,
Weiblich
ist unares Pradikatensymbol und
hans
,
franz
,
sabine
,
susanne
sind Konstantensymbole.
Wir leiten nun die leere Klausel mittels SLD-Resolution aus der gegebenen
Klauselmenge ab. Fur jeden Resolutionsschritt erzeugen wir eine Variante der ver-
wendeten Programmklausel, indem wir durch Indizieren die darin auftretenden Va-
riablen zu neuen Variablen umbenennen (s. Abbildung 9.3). Wendet man die dabei
verwendeten Unifikatoren σ
1
,...σ
6
auf das Literal in der Anfrage an, so erhalt man
G:
←
σ
6
◦···◦
σ
1
(
Tante
(
susanne
,t)) =
Tante
(
susanne
,
sabine
)
