% Construct a Proof Tree and explain the proof tree  (use sicstus3)

why(G) :-
	solve(G, P),
	explain(P).

%--------------------------------------------------------------

solve(true, true).
solve((A, B), (ProofA, ProofB)) :-
	solve(A, ProofA), 
	solve(B, ProofB).
solve(A, (A :- Proof)) :-
	A \= true,
	A \= (_,_),
	clause(A, B),
	solve(B, Proof).

%--------------------------------------------------------------

explain((A :- Proof)) :-
	write(A), write(' is true'),
	explain(Proof, 1).

explain(true, _).
explain((A :- Proof), Depth) :-
	nl, T is Depth*3, tab(T), write('because '),
	write(A), write(' is true'), 
	D is Depth + 1,
	explain(Proof, D).
explain((A, B), Depth) :-
	explain(A, Depth),
	explain(B, Depth).


% Sample Goal:  | ?- why(anc(bob,sue)).