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
Search WWH ::




Custom Search