Prolog Language
Herleitung von Bäumen

Beweisbaum

Der Beweisbaum (auch Suchbaum oder Ableitungsbaum) ist ein Baum, der die Ausführung eines Prolog-Programms zeigt. Dieser Baum dient zur Visualisierung des in Prolog vorhandenen chronologischen Rückverfolgungsprozesses. Die Wurzel der Baumstruktur stellt die ursprüngliche Abfrage dar und Verzweigungen werden erstellt, wenn Auswahlpunkte auftreten. Jeder Knoten im Baum repräsentiert somit ein Ziel. Zweige werden nur dann zu Blättern, wenn entweder Wahr / Falsch für die erforderlichen Ziele festgelegt wurde und die Suche in Prolog von links nach rechts durchgeführt wird .

Betrachten Sie folgendes Beispiel:

% Facts
father_child(paul,chris).        % Paul is the father of Chris and Ellen
father_child(paul,ellen).
mother_child(ellen,angie).       % Ellen is the mother of Angie and Peter
mother_child(ellen,peter).


% Rules
grandfather_grandchild(X,Y) :-
    father_child(X,Z),
    father_child(Z,Y).

grandfather_grandchild(X,Y) :-
    father_child(X,Z),
    mother_child(Z,Y).

Wenn wir jetzt fragen:

?- grandfather_grandchild(paul,peter).

Der folgende Nachweisbaum visualisiert den Tiefensuchvorgang:

                                   ?- grandfather_grandchild(paul,peter).
                                       /                             \
                                      /                               \
  ?- father_child(paul,Z1),father_child(Z1,peter).            ?- father_child(paul,Z2),mother_child(Z2,peter).
             /                   \                                    /                              \
      {Z1=chris}             {Z1=ellen}                         {Z2=chris}                        {Z2=ellen}
           /                       \                                /                                  \      
?- father_child(chris,peter).  ?- father_child(ellen,peter).  ?- mother_child(chris,peter). ?- mother_child(ellen,peter).
         |                         |                               |                               /              \ 
       fail                      fail                            fail                          fail(*)          success  

(*) schlägt für mother_child(ellen,angie) fehl, wenn "angie" nicht mit "peter" übereinstimmt