Making explicit the implicit proof tree

Hello,

Is it possible to make explicit the implicit proof tree embodied in the prolog stack and choice points. Or, is it necessary to carry along a proof tree in the arguments?

I am doing some graph searches and when a certain condition occurs, i’d like have a trace - or path – from where the search started to the node where the condition was recognized.

Choice points are often selection of outgoing links in a graph.

I guess i could carry along a kind of stack where, i push down a selection whenever it occurs, and the stack items get undone during backtracking – but isn’t this info included in the stack itself somewhere / somehow?

thank you,

Dan

If you want to keep track of a path followed during search, add a list and store your path there. Yes, some of this may be in the stack, but there is no portable way to get it out there and some may be lost due to last-call optimization. SWI-Prolog does allow you to look around in the system stack (see prolog_current_frame/1 and friends). Use with care. It is not really hard to crash the system or make it completely misbehaving using these predicates.

Try searching for prolog metacircular interpreter

The Craft of Prolog has a chapter on this. (And, IIRC a long long time ago Richard O’Keefe also wrote some posts in comp.lang.prolog, but in a quick search I couldn’t find it in the arc, sives.)