Keep track of which clause is involved in a certain proof

Help!
1

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]).
link(b, c, [clause2]).
link(c, d, [clause3]).
link(b, e, [clause4]).

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
2

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).
link(b, c).
link(c, d).
link(b, e).

path(X, Y) :- link(X, Y).
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,
T =  ((true=>link(a, b), (true=>link(b, c))=>path(b, c))=>path(a, c)) ;
X = a,
Y = e,
T =  ((true=>link(a, b), (true=>link(b, e))=>path(b, e))=>path(a, e)) ;
X = a,
Y = d,
T =  ((true=>link(a, b), (true=>link(b, c), (true=>link(c, d))=>path(c, d))=>path(b, d))=>path(a, d)) ;
X = b,
Y = d,
T =  ((true=>link(b, c), (true=>link(c, d))=>path(c, d))=>path(b, d)) ;
false.
3

Thanks a lot Eric :slight_smile:

1 Like
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
5

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

1 Like
6

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:   [10] numbervars(subproof(happy(somebody,_21152),(...,...)),0,_21138,[])
ERROR:    [9] '$syspreds':numbervars(subproof(happy(somebody,_21204),(...,...)),0,_21192) at /Applications/SWI-Prolog.app/Contents/swipl/boot/syspred.pl:1370
ERROR:    [8] '<meta-call>'(user:(...,...)) <foreign>
ERROR:    [7] <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

7

Also you can try print_term/2.

1 Like
8

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 :slight_smile:

1 Like
9

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