Proof as an output argument in Prolog meta interpreter

Question

I am putting together a simple meta interpreter which outputs the steps of a proof. I am having trouble with getting the proof steps as an output argument. My predicate explain1 returns the proof in the detailed form that i would like, but not as an output argument. My predicate explain2 returns the proof as an output argument but not with the level of detail that i would like. Can explain2 be modified so that it yields as much info as explain1? I don't need it to output text "Explaining..." and "Explanation...", just the actual explanans and explanandum.

The toy data at the bottom of the program ("if healthy and rich, then happy") is just an example and the idea is to have a database with more facts about other things. I want to try to make a predicate that accepts an effect, e.g. happy(john), and returns an explanation for it. So the E argument of explain is supposed to be entered by the user; another query might thus be explain(_, smokes(mary), _) and so on. I can't get what i want directly from the C and E variables in explain, because i want the program to output steps in the Proof process, where C and E vary, e.g. "rich and healthy, so happy; wins so rich; TRUE so rich; TRUE so happy" and so on. I.e. return all causal links that lead up to an effect.

The excellent site by Markus Triska has some details on this, but i am having trouble adapting that code to my problem.

Any help would be greatly appreciated!

Thanks/JCR

My program:

main1:-explain1(_, happy(john), _), fail.
main2:-explain2(_, happy(john), _, T), writeln(T), fail.

explain1(C, E, P):-
    C = ['True'],
    p(C, E, P),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.
explain1(C, E, P):-
    p(C, E, P),
    not(C = ['True']),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.
explain1(C, E, P):-
    p(C0, E, P0),
    maplist(explain1, C1, C0, P1),
    flatten(C1, C),
    append([P0], P1, P2),
    flatten(P2, P3),
    foldl(multiply, P3, 1, P),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.

explain2(C, E, P, T):-
    C = ['True'],
    p(C, E, P),
    T = [C, E, P].
explain2(C, E, P, T):-
    p(C, E, P),
    not(C = ['True']),
    T = [C, E, P].
explain2(C, E, P, T):-
    p(C0, E, P0),
    maplist(explain2, C1, C0, P1, _),
    flatten(C1, C),
    append([P0], P1, P2),
    flatten(P2, P3),
    foldl(multiply, P3, 1, P),
    T = [C, E, P].

multiply(V1, V2, R) :- R is V1 * V2.

p(['True'], wins(john), 0.7).
p([wins(john)], rich(john), 0.3).
p(['True'], healthy(john), 0.9).
p([rich(john), healthy(john)], happy(john), 0.6).

The output of main1:

Explaining happy(john). An explanation is: [rich(john), healthy(john)] with probability 0.6
Explaining rich(john). An explanation is: [wins(john)] with probability 0.3
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [wins(john), True] with probability 0.162
Explaining wins(john). An explanation is: [True] with probability 0.7
Explaining rich(john). An explanation is: [True] with probability 0.21
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [True, True] with probability 0.1134

The output of main2:

[[rich(john), healthy(john)], happy(john), 0.6]
[[wins(john), True], happy(john), 0.162]
[[True, True], happy(john), 0.1134]

Answer 1

I'm unclear on the probability portion of this metainterpreter, but I actually think it's incidental to your question so I'm going to try and sketch out how I would approach this.

You can think of call/1 as the prototypical interpreter for Prolog, because it simply proves a single goal. So it seems like the API you want is something like prove(+Goal, -Proof), where Goal gets proven just like it does with call/1, but you get a second thing back, a proof of some kind.

When normal Prolog sees an expression like Goal1, Goal2, you could think of it expanding into call(Goal1), call(Goal2). So what does your proof-returning metainterpreter do in this situation instead? It should prove both goals and then somehow combine those "subproofs".

All this suggests to me that something missing from your conception is, what is the structure of a proof? I would think hard about what kind of thing you're going to get back, because if you don't want a string, you'll want something you can traverse more easily. It will probably wind up having a tree structure similar to what Prolog does (except without the failure branches). I would thus expect it to have some kind of nesting and it could certainly "resemble" the call stack somehow, although I expect this would limit its utility for you (how are you going to traverse that tree usefully for a generic query?).

Let's consider your base case. It's probably something like this:

prove(true, true) :- !.

True is intrinsically true, because it is true.

The next case I would be interested in is "and".

prove((G1, G2), (P1, P2)) :- 
   !,
   prove(G1, P1), 
   prove(G2, P2).

This looks fairly tautological, but the key idea really is that we are combining the proofs of G1 and G2 with (P1, P2) in the proof.

The next case would be "or" probably:

prove((G1;_), P1) :- prove(G1, P1).
prove((_;G2), P2) :- !, prove(G2, P2).

This is the part where we are losing the failing branches. If the first branch succeeds, its proof will appear in the result; if the second branch succeeds instead, its proof will appear in the result. But they won't ever both appear in the result.

Finally we must handle builtins and user predicates, per a question I asked some time ago:

prove(H, subproof(H, Subproof)) :- clause(H, Body), prove(Body, Subproof).
prove(H, builtin(H)) :- call(H).

At this point we have a metainterpreter that produces very simple proofs. I'm going to add a few clauses and then try it with our metainterpreter:

mortal(X) :- man(X).
man(socrates).

Here's the query:

?- prove((member(X, [bread,socrates]), mortal(X)), Proof).
X = socrates,
Proof =  (builtin(member(socrates, [bread, socrates])), 
          subproof(mortal(socrates), 
                   subproof(man(socrates), true))) 

For reasons I do not yet understand, the use of member/2 will bomb out on a second query. I have opened a question about that on the SWI forum and will update this answer when I find out what's going on there.

Update. The issue is related to the autoloading of library(lists) which happens when you use member/2. On the first call, member/2 has no clauses, so it enters call/1, which invokes the autoloader and then invokes it as a built-in. On a subsequent attempt, member/2 has clauses, but their bodies involve predicates in the lists module, and this metainterpreter does not handle modules properly. A quick-and-dirty solution is to change the third clause to this:

prove(H, subproof(H, Subproof)) :- 
   \+ predicate_property(H, imported_from(_)), 
   clause(H, Body), 
   prove(Body, Subproof).

I hope this helps!