I would like to collect all the clauses included in a successful refutation sequence of a goal. In more imperative terms, I’d like to collect a list of the clauses that were “called” during execution of a query. This is also known as building a proof tree.
I know I can do this with a meta-interpreter, in fact I think I’ve done it a few times already. I would like however to take advantage of Swi-Prolog’s internal machinery, most notably tabling, but also anything that would have to be coded from scratch in a meta-interpreter.
Is there a way to do what I want in Swi without a meta-interpreter?
I was recently reading this older thread:
Where Jan Wielemaker suggests using prolog_current_frame/1 and prolog_frame_attribute/3 with a bit of a hack in front, and I thought that I could somehow use this to keep track of the clause indices or clause references of the clauses in a refutation sequence- but I couldn’t find out how to make it work.
Is there something else that is possible to do?
EDIT: After the conversation below, I realised I would have saved us all a lot of time if I had given an example. I redress this below.
Consider the following program:
odd(A):-s(A,B),even(B) % Clause 1 s(s(X),X). even(0). even(s(X)):- odd(X).
I would like to write a predicate rs/2 to collect all the successful refutation sequences that included clauses of odd/1 (and only keep the clauses of odd/1 in those sequences). For example, suppose I called rs/2 as shown below:
?- G = odd(s(s(s(0)))), rs(G, Ss).
Then rs/2 should respond as follows:
Ss =  ; false.
Where “1” is the clause index of Clause 1 in the odd/1 definition. Or in other words, it’s the sequence of clauses “visited” during a successful refutation, by resolution, of the goal
G = odd(s(s(s(0)))).