Logisches Programmieren und Anwortmengen - Methoden Wissensbasierter Systeme - page 277

C 1

G

σ 1

G 1 C 2

σ 2

.

G 2

.

G n−1

C n

σ n

G n

Abbildung 9.2 SLD-Resolution

9.3.1 SLD-Ableitungen

Jede Programmklausel (d.h. Fakt oder Regel) enthalt genau ein positives Literal,
wahrend die Zielklausel (Anfrage) nur negative Literale enthalt. Resolution zwi-
schen zwei Programmklauseln allein kann daher niemals zur leeren Klausel fuhren.
Andererseits fuhrt ein Resolutionsschritt zwischen einer Zielklausel und einer defini-
ten Klausel immer wieder zu einer neuen Zielklausel (bzw. zur leeren Klausel). Die
SLD-Resolution beruht gerade auf diesen Eigenschaften. Der Name SLD-Resolution
steht fur “ SL -Resolution for D efinite clauses”, wobei SL-Resolution fur “ L inear re-
solution with S election function” steht.
Bei der SLD-Resolution erfolgt jeder Resolutionsschritt zwischen einer definiten
Klausel und einer Zielklausel. Fur eine Menge von definiten Klauseln und eine

Zielklausel G als Anfrage muss eine SLD-Resolution aus

P

und G daher wie in
Abbildung 9.2 skizziert aussehen. Dabei sind die C i Varianten von Klauseln aus P
mit jeweils neuen Variablen (d.h. variablen-umbenannte Klauseln von P,sodass
kein C i einen Variablennamen enthalt, der schon vorher einmal benutzt wurde,
und daher insbesondere alle Elternklauseln variablendisjunkt sind), und die G i sind
Zielklauseln.
Anstelle der allgemeinen Resolutionsregel wird fur die SLD-Resolution die SLD-
Resolutionsregel im Allgemeinen wie folgt angegeben, wobei

P

P wieder eine Menge

von definiten Klauseln ist:

falls H B 1 ,...,B m eine

Variante einer Klausel aus

←

← A 1 ,...,A k−1 ,A k ,A k+1 ,...,A n .

P
ist und σ der allgemeinste
Unifikator von A k und H.

σ( ← A 1 ,...,A k−1 ,B 1 ,...,B m ,A k+1 ,...,A n .)