proof_tree(:Goal, -Tree)

Run Goal, capturing the derivation tree. Tree is a hierarchical structure of nodes of this shape:

g(Frame, Level, Goal, CRef, Complete, Children)

Here, Frame is the reference to the Prolog stack frame that ran the goal. This has no meaning to the user. Level is the nesting depth of the call, Goal is the executed goal as it is after the entire derivation succeeded, CRef is the clause that produced this answer, Complete is internal (means we have seen the "exit" port) and Children is a list of children in reverse order.

Re-satisfying re-satisfies Goal and on success Tree reflects the proof tree of the new answer.

 pt_children(+Tree, -Children) is det

 pt_goal(+Tree, -Goal) is det

 pt_clause(+Tree, -ClauseRef) is semidet

Get the interesting components from the proof tree. pt_children/2 reverses the recorded child nodes to restore the order of execution.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 pt_goal(Arg1, Arg2)

 pt_clause(Arg1, Arg2)