% Construct a proof tree and explain the proof tree to a user-specified depth 

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)) :-
	clause(A, B),
	solve(B, Proof).

explain((A :- Proof)) :-
	write('To what depth? '), read(DMax),
	write(A), write(' is true'),
	explain(Proof, 1, DMax).

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