Proof Tree

Opens a supplementary window in which program execution can be seen in progress. The main branch of the proof tree under construction for the goal being processed is displayed. The subgoals that have already been successfully satisfied appear in blue or in green . Those but partly satisfied (which are satisfying at the moment) appear in red, and the ones not yet reached appear in black .

Information in this window duplicates that in Stack window and other trace windows but it is easier to interpret.

You can double click on blue goals to see how they are satisfied. Note that the terms that instantiate variables in these branches can be seen too. If you double click a subgoal and hear sound beep, this means that this subgoal is instantiated with an axiom. If you want to receive the normal view of the Proof Tree again then double click on the last red subgoal. If you double click on a green subgoal then you will close its subtree.

You can use buttons Home, End and Insert for horizontal scrolling of this window.

Home scrolls to the beginning (the most left point).
End scrolls to the end (the most right point).
Insert scrolls to the middle.

Use also Page Up , Page Down and arrows .

Warning: The numbers of the variables in the subgoals which are in black may be not real in some sense. The reason: If this number is bigger than the maximum in the Variables window, then this is a not-instantiated variable with temporal number. The numbers of other variables are real and they are shown in the Variables window. Of course, these numbers are real but not constant because after backtracking they can change.