Resolution

[ Zum Seminar "Programmierkonzepte und Programmiersprachen" ] ↔ [ Zum Inhalt ] ↔ [ Unifikation ]

Übersicht:


Was ist Resolution ?


Resolution ist die Vorgehensweise von PROLOG bei der Lösung von Anfragen.
Ob eine Zielanweisung zutrifft/erfüllbar ist wird durch den Widerspruch bewiesen.


Wie funktioniert Resolution ?


Grundvorraussetzung für eine korrekte Arbeitsweise der Resolution ist eine Wissenbasis mit vollständigen, nicht widersprüchlichen Formeln.
Da das Resolutionsverfahren korrekt ist wird es immer aus einer Formelmenge einen Widerspruch ableiten wenn sich darin einer befindet.
Die Anfrage an eine Wissenbasis ist also nichts anderes als dass eine negierte Formel in die bereits vorhandene Menge gebracht wird. Trifft die Anfrage zu, so findet die Resolution einen Widerspruch und beweist somit deren Richtigkeit.
Dabei benutzt die Resolution das sogenannte Ableitungsverfahren.
Dieses regelt das Zusammenfassen von Klauseln und geht dabei so vor:
Wenn der Kopf der 1.Klausel im Körper der 2.Klausel vorkommt, so kann an dieser Stelle der Köper der 1.Klausel eingesetzt werden.
Zur Verdeutlichung:
1.Klausel: A ← B,C,D
2.Klausel: G ← E,F,A,K
ergibt
G ← E,F,B,C,D,K

PROLOG geht dabei von oben nach unten vor, wenn also mehrere abgleichbare Formeln vorhanden sind, so wird die "oberste" genommen, bei Nichterfolg wird die nächste versucht.
Sind mehrere Formel durch UND verknüpft, so wird dabei von links nach rechts vorgegangen, solange eine Beantwortung möglich ist. Bei verschiedenen möglichen Antworten wird immer die zuerst gefundene ausgegeben.


Ein Beispiel zur Vorgehensweise
Gegebene Wissensbasis:
legs(X,2) ← mammal(X),arms(X,2).
legs(X,4) ← mammal(X), arms(X,0).
mammal(horse).
arms(horse,0).

Stellt man nun die Anfrage:
?- legs(horse,4).
geht PROLOG folgendermassen vor
diese Anfrage entspricht dem Kopf der 2. Regel, wenn man also nun X mit horse "unifiziert"(dazu später mehr) und den Kopf durch den Körper der Regel ersetzt erhält man folgendes
:- mammal(horse), arms(horse,0).
nun wird mammal(horse)(da es ganz links steht kommt es zuerst dran) mit dem Fakt mammal(horse). aus der Wissenbasis 'gestrichen'.
Ebendies passiert dannach mit dem arms(horse,0) welches nach der ersten "Streichung" geblieben ist und nun gestrichen wird.
Übrig bleibt die leere Klausel, d.h. der Widerspruch, womit die Zielanweisung als 'wahr' bewiesen wäre.

[ Zum Seminar "Programmierkonzepte und Programmiersprachen" ] ↔ [ Zum Inhalt ] ↔ [ Seitenanfang ] ↔ [ Unifikation ]