How add finitely failed branches to a Prolog visualizer?

Question

Assume we want to visualize this Prolog execution. No goals from the fidschi islands, or something else exotic assumed, only good old SLDNF with the default selection rule:

p(a).
p(b).

?- \+ p(c).
Yes

But we have only a Prolog visualizer that can show derivations without negation as failure, like here. How can we boost the Prolog visualizer to also show negation as failure?

Answer 1

The good thing about negation as failure, writing a meta interpreter for negation as failure is much easier, than writing a meta interpreter for cut (!). So basically the vanilla interpreter for SLDNF can be derived from the vanilla interpreter for SLD by inserting one additional rule:

solve(true) :- !.
solve((A,B)) :- !, solve(A), solve(B).
solve((\+ A)) :- !, \+ solve(A). /* new */
solve(H) :- functor(H, F, A), sys_rule(F/A, H, B), solve(B).

We can now go on and extend solve/3 from here in the same vain. But we do something more, we also write out failure branches in the search tree, similar like Prolog visualizer does by strikethrough of a clause. So the amended solve/3 is as follows:

% solve(+Goal, +Assoc, +Integer, -Assoc)
solve(true, L, _, L) :- !.
solve((A, B), L, P, R) :- !, solve(A, L, P, H), solve(B, H, P, R).
solve((\+ A), L, P, L) :- !, \+ solve(A, L, P, _). /* new */
solve(H, L, P, R) :- functor(H, F, A), sys_rule(F/A, J, B),
   callable_property(J, sys_variable_names(N)),
   number_codes(P, U), atom_codes(V, [0'_|U]), shift(N, V, W),
   append(L, W, M), 
   (H = J -> true; offset(P), write(fail), nl, fail),  /* new */
   reverse(M, Z), triage(M, Z, I, K),
   offset(P), write_term(I, [variable_names(Z)]), nl,
   O is P+1, solve(B, K, O, R).

Here is an example run:

?- ?- \+ p(c).
fail
fail
Yes

See also:

AI Algorithms, Data Structures and Idioms
CH6: Three Meta-Interpreters
Georg F. Luger - Addison-Wesley 2009
https://www.cs.unm.edu/~luger/