Database Reference
In-Depth Information
d.h., σ
6
◦···◦
σ
1
(t)=
sabine
lasst sich als Antwort auf die Frage “Wer ist eine Tante
von Susanne” interpretieren. Die folgende Tabelle enhalt einige weitere Anfragen an
das Programm und die zugehorigen Antwortsubstitutionen:
verbale Formulierung
Anfrage
Antwortsubstitutionen
“Wessen Tante ist Sabine?”
←
Tante
(n,
sabine
).
n =
susanne
“Wer ist Vater von Sabine?”
←
Vater
(sabine, p).
p =
franz
“Wessen Vater ist Franz?”
←
Vater
(k,
franz
).
k =
hans
k =
sabine
“Wer ist Vater von wem?”
←
Vater
(k, p).
k =
hans
,p=
franz
k =
sabine
,p=
franz
k =
susanne
,p=
hans
Beachten Sie, dass auf alle Anfragen in diesem Beispiel ein PL1-Kalkul wie et-
wa das Resolutionsverfahren lediglich die Antwort “Ja” generieren wurde, wahrend
mittels SLD-Resolution die sehr viel informativeren konstruktiven Antworten gege-
ben werden.
Ist A ein Grundatom uber der Signatur eines logischen Programms
P
,dann
ist A eine logische Folgerung von
P
genau dann, wenn es eine SLD-Ableitung fur
P
A. gibt. Damit ist die SLD-Resolution korrekt und vollstandig.
Die Korrektheit und Vollstandigkeit der SLD-Resolution gilt aber auch hinsichtlich
der Antwortsubstitutionen. Jede berechnete Antwortsubstitution ist eine korrekte
Antwortsubstitution, und fur jede korrekte Antwortsubstitution σ gibt es eine be-
rechnete Antwortsubstitution σ
b
,sodassσ
b
allgemeiner als oder gleich σ ist; diese
letztgenannte Eigenschaft wird
Antwortvollstandigkeit
der SLD-Resolution genannt.
Wegen der Aquivalenz der logischen Semantik eines Programms, die durch die
Menge seiner Modelle definiert ist, und der operationalen Semantik, die durch die
SLD-Resolution gegeben ist, wird das logische Programmieren auch als
deklaratives
Programmieren
bezeichnet.
und G
=
←
9.3.3
Suchraum bei der SLD-Resolution
In diesem Abschnitt fuhren wir aus, dass die zuletzt aufgefuhrten Eigenschaften der
SLD-Resolution selbst dann noch gelten, wenn man den aufgespannten Suchraum
bei der Auswahl des zu resolvierenden Anfrageatoms einschrankt.
Bei der SLD-Resolutionsregel gibt es zwei Indeterminismen:
1. Auswahl des Atoms A
k
2. Auswahl der Programmklausel H
←
B
1
,...,B
m
.
Diese beiden Auswahlmoglichkeiten bestimmen den Suchraum bei der SLD-
Resolution. Ein wichtiges Theorem besagt, dass es fur
jede
Auswahlmoglichkeit fur
A
k
immer noch eine erfolgreiche SLD-Ableitung gibt - falls es denn uberhaupt eine
erfolgreiche SLD-Ableitung gibt (
don't care nondeterminism
). Die Auswahl von A
k