We now use the same example program to show how the proof tree grows. We choose a proof tree because we can delete any parts of the tree which do not contribute to the final solution (which is not the case for the execution tree).
The search space as an AND/OR tree is shown in figure 5.4.
Figure 5.4: The AND/OR Tree for the Goal a(X,Y)
We now develop the AND/OR proof tree for the same goal. We show ten stages in order in figure 5.5. The order of the stages is indicated by the number marked in the top left hand corner.
The various variable bindings ---both those made and unmade--- have not been represented on this diagram.
Figure 5.5: The Development of the AND/OR Proof Tree