Keep track of which clause is involved in a certain proof

Help!
4

Hi!

I am trying to format the output from the meta interpreter to a more readable form. When using main0 below which has portray_clause/1 i get a nice replacement of clpr variables as A, B, etc; the problem with main0 is that the proof just gets printed on a long line with a lot of nesting which is hard to read. With main1 i get the desired readability, but the problem is that i somehow loose variable names (A, B, etc).

Does anybody know how to fix this?

Cheers/JCR

:-use_module(library(clpr)).

wins(somebody, _).
healthy(somebody, _).
rich(X, P1):-
   wins(X, P0), {P1 = 0.5 * P0}.
happy(X, P3):-
   rich(X, P1), healthy(X, P2), {P3 = P1 * P2}.

main0:-prove(happy(somebody, _), Proof), portray_clause(Proof).
main1:-prove(happy(somebody, _), Proof), showProof(Proof).


showProof(X):-
   X = subproof(G, P),
   \+(P = true),
   write('Prove: '), portray_clause(G), nl,
   write('Proof: '), portray_clause(P), nl, nl,
   showProof(P).
showProof(X):-
   X = subproof(G, true),
   write('Prove: '), portray_clause(G), nl,
   write('Proof: '), write(true), nl, nl.
showProof(X):-
   X = ','(A, B),
   \+(A = true), \+(B = true),
   showProof(A),
   showProof(B).

prove(true, true):-!.
prove((G1, G2), (P1, P2)) :- 
   !,
   prove(G1, P1), 
   prove(G2, P2).
prove((G1;_), P1) :- prove(G1, P1).
prove((_;G2), P2) :- prove(G2, P2).
prove(G, P):- G = {_}, !, call(G), P = subproof(G, true).
prove(H, subproof(H, Subproof)) :- clause(H, Body), prove(Body, Subproof).
1 Like