The user may issue commands via either the keyboard or the popup context menu. All commands apply to the currently selected node. The user can move the selection handles (focus) to a node by simply moving the mouse pointer over it or using the directional keys.

Below are two different stages in the process of exploring ~guilty. The window on the left shows that the expansion of ~guilty halts at seen_elsewhere (shown in dark red), since there is no matching clause for seen_elsewhere in our program. (Less abstractly,we may say there is nothing in the set of evidence concerning the claim that the defendant was seen elsewhere.) However, there is an alternative clause, or rule, for alibi, namely, being incapacitated is also considered a valid alibi. The existence of unexplored alternative(s) is indicated by an inverted 3D look.
The window on the right shows the tree after alibi has been 'redone'. Since incapacitated also fails, we see that neither ~guilty nor alibi is evident. What's more, all possible alternatives have been exhausted.

The last example (below) illustrates the fact that nodes may be expanded in any order. (Nodes not yet expanded have a raised 3D look). Also shown is an example of a popup context menu. Though not shown here, any subtree can be collapsed to keep large trees from becoming unwielding.

Clause trees, though finite, may become arbitrarily large. Therefore, Explore mode does not pre-compute the trees but contructs them dynamically. Here, XPCE's object-oriented structure is exploited to good effect. For instance, one of the early questions was how, or more precisely when, a node should be verified for 'evident.' The solution: when a green node (a true node or an ancestor-resolved node) is created, it sends a message to each of its ancestors to check whether the latter is at the root of a closed clause tree. In the avove example, unobserved was verified as evident (albeit somewhat trivially); it's therefore shown in blue.

Explore mode can be viewed as a sort of tracer/debugger for logic programs. It is more flexible than the Prolog inference engine in that it is not restricted to depth first expansion of terms/nodes. [On the other hand, turning Explore into a full tracer/debugger for Prolog would involve (at the least) handling of the cut -- probably a non-trivial task.]