Database Reference
In-Depth Information
In dieser Notation der SLD-Resolutionsregel kommt zum Ausdruck, dass ein
Atom A
k
der Anfrage nur mit dem Kopf einer Klausel aus
resolviert werden
kann. A
k
selbst wird dann gerade durch den Rumpf B
1
,...,B
m
der betreffenden
Klausel ersetzt. Dabei muss auf die resultierende Resolvente noch die Substitution
σ = mgu(A
k
,H) angewandt werden. A
k
heißt dabei das
ausgewahlte Atom
(
selek-
tiertes Atom
,
selected atom
).
Achten Sie auf die notwendige
Variablenumbenennung
: Bevor mit einer Pro-
grammklausel resolviert werden darf, muss diese mit neuen Variablen variablendis-
junkt zur vorliegenden Zielklausel umbenannt werden!
P
Selbsttestaufgabe 9.9 (Resolution und SLD-Resolution)
Geben Sie die
SLD-Resolutionsregel in der Form der vollen Resolutionsregel fur PL1 (Seite 65)
an.
Definition 9.10 (abgeleitete Zielklausel)
In der Zielklausel
G
A
1
,...,A
k−1
,A
k
,A
k+1
,...,A
n
.
sei A
k
das selektierte Atom. Sei
C
=
←
B
1
,...,B
m
.
eine (zu G variablendisjunkte Variante einer) Klausel aus
=
H
←
P
,sodassA
k
und H
unifizierbar sind. Dann ist die Zielklausel
G
A
1
,...,A
k−1
,B
1
,...,B
m
,A
k+1
,...,A
n
.)
abgeleitet aus
G
und
=
σ(
←
P
mit der Klausel C und der Substitution σ,wobeiσ =
mgu(A
k
,H).
Definition 9.11 (SLD-Ableitung, SLD-Beweis)
Eine
SLD-Ableitung
fur ein
Hornklauselprogramm
P
und eine Hornanfrage G
0
ist eine endliche oder unend-
liche Folge
G
0
,G
1
,G
2
,...
von Zielklauseln, so dass G
i
(fur i
(mit der Substitution σ
i
)
abgeleitet ist. Diese Folge ist ein
SLD-Beweis
, falls sie endlich ist und das letzte
Element G
l
der Folge die leere Klausel ist.
≥
1) aus G
i−1
und
P
9.3.2
Berechnete Antwortsubstitutionen
Bei jeder SLD-Ableitung fallt eine Folge von Substitutionen an. Die Komposition
dieser Substitutionen bei einem SLD-Beweis konnen wir als Antwort zu der gege-
benen Anfrage interpretieren.
Definition 9.12 (berechnete Antwortsubstitution)
Sei G
0
,G
1
,...,G
l
ein
SLD-Beweis wie in Definition 9.11. Dann heißt die Komposition der verwendeten
Substitutionen eingeschrankt auf die in G
0
auftretenden Variablen
Vars
(G
0
)
σ
l
◦
...
◦
σ
2
◦
σ
1
|Vars (G
0
)
berechnete Antwortsubstitution
fur
P
und G
0
.
