证明树（也称为搜索树或派生树）是显示Prolog程序执行的树。该树有助于可视化Prolog中存在的按时间顺序回溯过程。树的根代表初始查询，并在选择点出现时创建分支。因此，树中的每个节点都代表一个目标。仅当证明所需（一组）正确/错误goal(s)并且在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)“天使”与“彼得”不符而失败