Is there a way to make swi prolog print its currently working inference tree?

Question

It would be a great help on my course.

Answer 1

You could try and extend the plain "vanilla" meta-interpreter by keeping track of the proof information. Basically, the plain vanilla interpreter looks as follows:

solve([]).
solve([A|T]) :- solve_atom(A), solve(T).

solve_atom(A) :- my_clause(A,B), solve(B).

my_clause(doubleapp(X,Y,Z,R),[app(X,Y,I),app(I,Z,R)]).
my_clause(app([],L,L),[]).

You can add an extra argument to the interpreter to keep track of resolution steps, ... Probably, you will want to use the built-in clause/2 rather than my_clause (so that you don't have to manually insert the program you wish to trace).

I have actually written a (draft) solution for SICStus Prolog for my lectures. It can be run from the command-line. It should be easy to adapt for SWI. It can generate a dot representation of the SLD-tree or of an And-Or-Tree. I can send you the source code upon request.

But maybe there is an easier solution built into SWI, I don't know.