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

**URL:** <https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325>\
**Category:** Help!\
**Created:** [September 28, 2019, 12:09pm UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325 "2019-09-28T12:09:36Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![JCR](https://avatars.discourse-cdn.com/v4/letter/j/258eb7/32.png) [@JCR](https://swi-prolog.discourse.group/u/JCR)\
**Post date:** [September 28, 2019, 12:09pm UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/1 "2019-09-28T12:09:37Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![EricGT](https://avatars.discourse-cdn.com/v4/letter/e/f1d935/32.png) [@EricGT](https://swi-prolog.discourse.group/u/EricGT)\
**Post date:** [September 28, 2019, 1:00pm UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/2 "2019-09-28T13:00:27Z")

</div>

Based on [A Couple of Meta-interpreters in Prolog](https://www.metalevel.at/acomip/) specifically `Showing proofs`.

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

```

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

```

```prolog
?- 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.

```

---

<div class="post-metadata">

**Author:** ![JCR](https://avatars.discourse-cdn.com/v4/letter/j/258eb7/32.png) [@JCR](https://swi-prolog.discourse.group/u/JCR)\
**Post date:** [September 28, 2019, 1:17pm UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/3 "2019-09-28T13:17:52Z")

</div>

Thanks a lot Eric 🙂

---

<div class="post-metadata">

**Author:** ![JCR](https://avatars.discourse-cdn.com/v4/letter/j/258eb7/32.png) [@JCR](https://swi-prolog.discourse.group/u/JCR)\
**Post date:** [November 4, 2019, 7:06am UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/4 "2019-11-04T07:06:04Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [November 5, 2019, 1:34am UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/5 "2019-11-05T01:34:32Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![JCR](https://avatars.discourse-cdn.com/v4/letter/j/258eb7/32.png) [@JCR](https://swi-prolog.discourse.group/u/JCR)\
**Post date:** [November 5, 2019, 5:29am UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/6 "2019-11-05T05:29:38Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![swi](https://avatars.discourse-cdn.com/v4/letter/s/51bf81/32.png) [@swi](https://swi-prolog.discourse.group/u/swi)\
**Post date:** [November 5, 2019, 7:26pm UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/7 "2019-11-05T19:26:29Z")

</div>

Also you can try [print\_term/2](https://www.swi-prolog.org/pldoc/doc_for?object=prolog_pretty_print%3Aprint_term/2).

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [November 6, 2019, 1:17am UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/8 "2019-11-06T01:17:23Z")

</div>

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 🙂

---

<div class="post-metadata">

**Author:** ![JCR](https://avatars.discourse-cdn.com/v4/letter/j/258eb7/32.png) [@JCR](https://swi-prolog.discourse.group/u/JCR)\
**Post date:** [November 6, 2019, 2:15am UTC](https://swi-prolog.discourse.group/t/keep-track-of-which-clause-is-involved-in-a-certain-proof/1325/9 "2019-11-06T02:15:58Z")

</div>

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