% Meta-Interpreter Returning Proofs (or "Explanations")
% Oct. 1999, by Kazunori Ueda

:- op(1150, xfx, <=).
:- op(950,xfy, &).

solve(A) :- solve(A,PA), print_proof(PA,0).

solve(true, true).
solve((A & B), and(PA,PB)) :- 
    solve(A,PA), solve(B,PB).
solve(A, known(A)) :- builtin(A), call(A).
solve(A, because(A,PB)) :- (A <= B), solve(B,PB).

builtin(is(_,_)).   builtin(dif(_,_)).

print_proof(true,_).
print_proof(and(PA,PB),L) :-
    print_proof(PA,L), print_proof(PB,L).
print_proof(known(_),L) :-
    tab(2*L), write(' (known)'), nl.
print_proof(because(A,PB),L) :- 
    tab(2*L), write(A), nl,
    L1 is L+1, print_proof(PB,L1).