 # Keep track of which clause is involved in a certain proof

Hi!

Maybe somebody can help me with this? I have the code below where i want to know which clauses are involved in deducing a certain conclusion. For example, for `?path(X, Y, ID)` then one solution is `ID = [clause1, clause2, clause3], X = a, Y = d`. But i would like to drop the last argument about clause in the `link/3` predicate in the facts section for space reasons. I.e. instead of `link(a, b, [clause1]).` i would like `link(a, b).`

Is there any way to this?

Thanks/JCR

``````link(a, b, [clause1]).

path(X, Y, ID):- link(X, Y, ID).
path(X, Y, ID):- link(X, Z, ID1), path(Z, Y, ID2), append(ID1, ID2, ID).``````
1 Like

Based on A Couple of Meta-interpreters in Prolog specifically `Showing proofs`.

``````:- op(750, xfy, =>).

mi_clause(G, Body) :-
clause(G, B),
defaulty_better(B, Body).

defaulty_better(true, true).
defaulty_better((A,B), (BA,BB)) :-
defaulty_better(A, BA),
defaulty_better(B, BB).
defaulty_better(G, g(G)) :-
G \= true,
G \= (_,_).

mi_tree(true, true).
mi_tree((A,B), (TA,TB)) :-
mi_tree(A, TA),
mi_tree(B, TB).
mi_tree(g(G), TBody => G) :-
mi_clause(G, Body),
mi_tree(Body, TBody).
``````
``````link(a, b).

path(X, Y) :- link(X, Z), path(Z, Y).
``````
``````?- mi_tree(g(path(X,Y)), T).
X = a,
Y = b,
T =  ((true=>link(a, b))=>path(a, b)) ;
X = b,
Y = c,
T =  ((true=>link(b, c))=>path(b, c)) ;
X = c,
Y = d,
T =  ((true=>link(c, d))=>path(c, d)) ;
X = b,
Y = e,
T =  ((true=>link(b, e))=>path(b, e)) ;
X = a,
Y = c,
X = a,
Y = e,
X = a,
Y = d,
X = b,
Y = d,
false.
``````

Thanks a lot Eric 1 Like

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).``````

Separate writes use their independent variable numbering. Use numbervars/3 to number the whole term before writing the parts.

1 Like

Thank you very much for taking time to respond! I appreciate it very much.

When i do:

`?- prove(happy(somebody, _), Proof), numbervars(Proof, 0, _), portray_clause(Proof).`

I get an error about the expression containing attributed variables:

``````ERROR: Type error: `subproof(happy(somebody,_20634{geler = ...}),(subproof(rich(somebody,_20762{itf = ..., geler = ...}),(subproof(wins(somebody,_20888{itf = ...}),true),subproof({_20762{itf = ..., geler = ...}=0.5*_20888{itf = ...}},true))),subproof(healthy(somebody,_20724{geler = ...}),true),subproof({_20634{geler = ...}=_20762{itf = ..., geler = ...}*_20724{geler = ...}},true)))' contains attributed variables
ERROR: In:
ERROR:    numbervars(subproof(happy(somebody,_21152),(...,...)),0,_21138,[])
ERROR:     '\$syspreds':numbervars(subproof(happy(somebody,_21204),(...,...)),0,_21192) at /Applications/SWI-Prolog.app/Contents/swipl/boot/syspred.pl:1370
ERROR:     '<meta-call>'(user:(...,...)) <foreign>
ERROR:     <user>
``````

I then tried:

`?- prove(happy(somebody, _), Proof), numbervars(Proof, 0, _, [attvar(bind)]), portray_clause(Proof).`

But this results in:

`ERROR: Unhandled exception: type_error(nf(A,_25754),1,'a numeric expression',A)`

Maybe that `numbervars/4` gets confused by clpr expressions of the type `{_4423 = _44223 * _88778}`? Still, portray_clause/1 seems to handle it really well:

With:

`?- prove(happy(somebody, _), Proof), portray_clause(Proof).`

I get the beautiful:

`subproof(happy(somebody, C), (subproof(rich(somebody, A), (subproof(wins(somebody, B), true), subproof({A=0.5*B}, true))), subproof(healthy(somebody, D), true), subproof({C=A*D}, true))).`

I don’t know enough about the internal workings of clpr and numbervars to find a constructive solution.

Cheers/JCR

Also you can try print_term/2.

1 Like

Use copy_term_nat/2 (?) to get rid of the attributes first. You can also look at portray_clause/1 to see what happens. It is all pure Prolog 1 Like

Thanks @jan and @swi! Now it works.

Here is the complete code

``````:-use_module(library(clpr)).

main:-prove(happy(somebody, _), Proof), copy_term_nat(Proof, Proof2), numbervars(Proof2, 0, _, [attvar(bind)]), showProof(Proof2).

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}.

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).

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