Informatikmaterialien 
von Tino Hempel

Startseite | Informatik | Physik | Mathematik | Sonstiges |

| Inhalt | Vorherige Seite | Nächste Seite


Richard-Wossidlo-Gymnasium Ribnitz-Damgarten
Fachbereich Informatik


Resolution, Backtracking und Unifikation
(Hinweis: Visualisierung erfolgt mit dem Programm ProVisor. 
Erwerbbar über URL:   http://www.bildung.hessen.de/abereich/inform/skii/material/prolog.htm)


Wie arbeitet eigentlich PROLOG? Wieso findet es Lösungen, die richtig aber nicht sofort zu sehen sind? Das Geheimnis liegt in den grundlegenden Prinzipien des deklarativen Programmierens. 

Erläuterndes Beispiel

Im folgenden sollen die Prinzipien an konkreten Beispielen anschaulich erarbeitet werden. Dazu wird folgende Wissensbasis vorausgesetzt:

Beispiel (aus Röhner, 1995): 

maennlich(paul).
maennlich(fritz).
maennlich(steffen).
maennlich(robert).

weiblich(karin).
weiblich(lisa).
weiblich(maria).
weiblich(sina).

vater_von(steffen, fritz).
vater_von(fritz, karin).
vater_von(steffen, lisa).
vater_von(paul, maria).

mutter_von(karin, maria).
mutter_von(sina, paul).

elternteil_von(X,Kind):- vater_von(X,Kind).
elternteil_von(X,Kind):- mutter_von(X,Kind).

Matchen

An das System wird die Entscheidungsfrage ?– maennlich(steffen). gestellt. 

PROLOG vergleicht diese Anfrage mit den in der Wissensbasis gespeicherten Fakten und Regeln, wobei zunächst geprüft wird, ob der Funktor mit gleicher Stelligkeit vorhanden ist. In diesem Fall führt es zu den Fakten:

maennlich(paul).
maennlich(fritz).
maennlich(steffen).
maennlich(robert).

Nun werden das in der Frage vorkommende Term steffen mit denen der Fakten nacheinander verglichen. 

Findet PROLOG so wie hier eine Übereinstimmung, ergibt sich die Antwort yes, man spricht man vom Matchen (engl. zusammenpassen). Sollte in der gesamten Datenbasis keine Übereinstimmung vorhanden sein, so erscheint no

Unifikation eines Terms mit einer ungebundenen Variable

An das System wird die Ergänzungsfrage ?– vater_von(fritz,X). gestellt. 

Wiederum werden alle Fakten und Regeln benutzt, die den gleichen Funktor vater_von besitzen.

vater_von(steffen, fritz).
vater_von(fritz, karin).
vater_von(steffen, lisa).
vater_von(paul, maria).

Nun wird versucht, das erste Argument der Anfrage fritz mit steffen zu matchen. Dies hat aber keinen Erfolg. Damit kommt der zweite Fakt an die Reihe. Hier kommt es zur Übereinstimmung der jeweils ersten Argumente und es erfolgt die Bindung des Argumentes karin an die freie Variable X. Diese wird damit gebunden (instanziert). Diesen Vorgang bezeichnet man als Unifikation oder Instantiierung. Da es keine weitere freie Variable gibt, hat das System eine Lösung gefunden und gibt sie als X = karin aus.

Unter der Unifikation/Instantiierung zweier Terme versteht man die Ersetzung der in ihnen vorkommenden Variablen durch Terme derart, dass die so entstandenen Terme als Zeichenfolge gleich sind. 

Zwei Terme heißen unifizierbar, wenn sie durch geeignete Ersetzung der Variablen in diesem Sinne gleich gemacht werden können.

Damit ist die Lösungssuche aber nicht beendet, da ja noch ungeprüfte Klauseln existieren. 

Backtracking ist die Fortsetzung der Lösungssuche beginnend am letzen Alternativpunkt. Dazu werden alle ab diesem Punkt gebundenen Variablen wieder frei.

Zunächst wird die Bindung der Variablen X aufgehoben und X wieder frei.

Die nachfolgende zweimalige Unifikation bleibt jedoch erfolglos, so dass vom System ein no ausgegeben wird. 

Im Falle der Anfrage ?- vater_von(steffen,X). ergeben sich zwei Lösungen.

Unifikation zweier Variablen

An das System wird die Anfrage ?- elternteil_von(Elter,maria). gestellt. Damit ergibt sich

Das System findet zwei Regelköpfe, die der Anfrage entsprechen und verwendet den ersten Regelkopf. In diesem stehen aber die Variablen X und Kind. PROLOG benennt diese Variablen zunächst zu X_1 und Kind_1 um. Anschließend unifiziert es die Variable X_1 mit der ungebundenen Variablen Elter und die Variable Kind_1 mit dem Argument maria.

Unifikation ist das Gleichsetzen von Variablen. Hierfür gilt:

  • sind beide Variablen ungebunden, dann stehen sie für den gleichen Wert, d. h. 
    erhält eine Variable einen Wert, wird dieser automatisch der zweiten Variablen zugewiesen.

  • ist eine Variable gebunden und die andere nicht, so erhält die freie Variable den Wert der gebundenen.

  • sind beide Variablen gebunden, so ist die Unifikation gleich der von Termen.

Resolution

An das System wird folgende Anfrage gestellt: ?- weiblich(Kind),elternteil_von(Elter,Kind). Es ergibt sich das folgende Bild:

Das System versucht, das erste Teilziel weiblich(Kind)mit einem Faktum zu unifizieren, d. h. das Teilziel zu erfüllen. Es wird erfüllt durch die Bindung von karin an die Variable Kind. Damit wird die Anfrage reduziert auf ?- elternteil_von(Elter,karin).

Mit der gebundenen Variable Kind wird nun versucht, das zweite Teilziel elternteil_von(Elter,karin)zu erfüllen. 

Da es zwei Regeln elternteil_von/2 gibt, ersetzt das System intern die Anfrage ?- elternteil_von(Elter,karin). durch ?- vater_von(Elter,karin); mutter_von(Elter,karin).beachte: Semikolon steht für ODER. Es fand also ebenfalls eine Unifikation der Variablen X mit Elter statt.

Das System unifiziert das Teilziel vater_von(Elter,karin), so dass letztlich fritz an Elter gebunden wird. Damit gibt es keine freien Variablen mehr, die ODER-Bedingung ist erfüllt und PROLOG gibt als erste gefundene Lösung Kind = karin und Elter = fritz aus.

PROLOG konnte aber nicht alle Fakten für die Lösungssuche verwenden, somit setzt Backtracking am letzen Alternativpunkt ein. Es ergibt sich: 

Jedoch kann in der vater_von-Klausel keine Lösung mehr gefunden werden. Das System geht in den ODER-Zweig mutter_von und wird fündig. Damit ist die Lösungssuche immer noch nicht beendet, denn im mutter_von-Zweig gab es noch unbenutzte Fakten. Somit setzt erneut Backtracking ein, das zu keinem weiteren Erfolg im mutter_von-Zweig führt. 

Das System hat aber zu Beginn bei der Bestimmung der Variablenwertes für weiblich(Kind) einen Backtrackingpunkt gesetzt. Somit geht die Lösungssuche weiter, usw. 

Resolution ist ein Beweisprinzip, das eine Anfrage durch  schrittweise Ersetzung der Teilziele durch Fakten oder Regelrümpfe in die leere (wahre) Behauptung ?- . unter Ausgabe der zwischenzeitlich gebundenen Variablen überführt.  

Notwendig sind dabei die Prinzipien der Unifikation und des Backtrackings.

 



zur Startseite
© Tino Hempel 1997 - 2003 Im Web vertreten seit 1994.
Eine Internet-Seite aus dem Angebot von Tino Hempel.

Für alle Seiten gilt der 
Haftungsausschluss/Disclaimer.