Вы можете попытаться расширить простой «ванильный» мета-интерпретатор, отслеживая информацию о доказательствах.
По сути, простой ванильный интерпретатор выглядит следующим образом:
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),[]).
Вы можете добавить дополнительный аргумент в интерпретатор, чтобы отслеживать шаги разрешения ...
Возможно, вы захотите использовать встроенное предложение / 2 вместо my_clause (чтобы вам не приходилось вручную вставлять программу, которую вы хотите отследить).
Я фактически написал (черновик) решение для SICStus Prolog для своих лекций. Его можно запустить из командной строки.
Это должно быть легко адаптироваться к SWI.
Он может генерировать точечное представление дерева SLD или дерева And-Or-Tree.
Я могу отправить вам исходный код по запросу.
Но, может быть, есть более простое решение, встроенное в SWI, я не знаю.