Informatikmaterialien 
von Tino Hempel

Startseite | Informatik | Physik | Mathematik | Sonstiges |

| Inhalt | Vorherige Seite | Nächste Seite


Richard-Wossidlo-Gymnasium Ribnitz-Damgarten
Fachbereich Informatik


UND-ODER-Beweisbaum


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. 

Beispielwissensbasis

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

Beispiel (nach 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).

bruder_von(X,Y):- vater_von(V,X),mutter_von(M,X),
                  vater_von(V,Y),mutter_von(M,Y),
                  maennlich(Y),Y\==X.

grossvater(X,Y):- maennlich(X),elternteil_von(X,Z),elternteil_von(Z,Y).

Beispiel 1

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

Es ergibt sich folgender Beweisbaum, der nur aus einem ODER-Zweig besteht: 

Nun wird versucht, das erste Argument der Anfrage, also fritz mit steffen zu matchen. Dies hat aber keinen Erfolg. 

Damit wird der zweite Fakt benutzt. Hier stimmen die ersten Argumente von Anfrage und Fakt überein, PROLOG bindet nun das Argument karin an die freie Variable X. Diesen Vorgang  bezeichnet man als Unifikation oder Instantiierung. Da das System noch weitere Alternativen prüfen kann, setzt das System einen Backtracking-Punkt, also eine "Rücksprung-Markierung".
Somit sind alle Variablen gebunden und das System hat eine Lösung gefunden, die es als X = karin ausgibt.

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. Es existieren ja noch ungeprüfte Klauseln. 

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.

Beispiel 2

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

Für elternteil_von/2 gibt es zwei unterschiedliche Regeln, die somit als ODER-Knoten gekennzeichnet werden. Jede Regel kann aus einem oder mehreren Prädikatenaufrufen bestehen, die durch "UND" verknüpft sind. Hier ist es allerdings jeweils nur ein Prädikat, nämlich vater_von/2 bzw. mutter_von/2. Es handelt sich um einen entarteten UND-Knoten.

Das System startet die Lösugssuche, in dem es im Beweisbaum nach links geht, setzt aber bereits einen Backtrackingpunkt, da auf der rechten Seite zu untersuchende Alternativen vorhanden sind. 

Nun bindet es die Variable Elter an X und Kind an maria. Das System versucht nun eine Unifikation zu finden und geht dazu die vater_von-Klausen durch. In der letzten Klausel gelingt die Unifikation und es erfolgt die Bindung von paul an X. Damit gibt es keine freien Variablen mehr. Das System hat eine erste Lösung gefunden Elter = paul. 

Nach Ausgabe der ersten Lösung setzt Backtracking ein. Die Bindungen werden aufgehoben und das System fährt mit der Lösungssuche am letzten Backtrackingpunkt fort. Eine erneute Unifikation liefert schließlich Elter = karin und einen weiteren Backtrackingpunkt, da es noch eine zu untersuchende Klausel gibt. Nach Ausgabe der zweiten Lösung setzt erneut Backtracking ein, das jedoch keine weiteren Lösungen ermittelt.

Hier muss noch weiter geschrieben werden, wahrscheinlich besser: dynamische Präsentation! 

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

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 - 2005 Im Web vertreten seit 1994.
Eine Internet-Seite aus dem Angebot von Tino Hempel.

Für alle Seiten gilt der 
Haftungsausschluss/Disclaimer.