證明樹

證明樹（也是搜尋樹或派生樹）是一個顯示 Prolog 程式執行的樹。這棵樹有助於視覺化 Prolog 中的時間順序回溯過程。樹的根表示初始查詢，並在出現選擇點時建立分支。因此，樹中的每個節點都代表一個目標。當在所需（一組）目標中證明 true / false 時，分支僅成為葉子，並且 Prolog 中的搜尋以從左到右的深度優先方式執行。

請考慮以下示例：

% 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).

當我們現在查詢：

?- grandfather_grandchild(paul,peter).

以下證明樹視覺化深度優先搜尋過程：

                                   ?- 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  

（*）對於 mother_child(ellen,angie) 失敗，其中’angie’未能匹配’peter'