% Construct and explain the proof tree to a user-specified depth with 
% English explanation of user predicates.  Also include primitive predicates 
% and provide special explanation for negation

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

solve(true, true) :- !.
solve((A, B), (ProofA, ProofB)) :- !,
	solve(A, ProofA), 
	solve(B, ProofB).

solve(not(A), (not(A) :- true)) :- !,
	not(solve(A, _)).

solve(A, (A :- true)) :-
	builtin(A), !, A.

solve(A, (A :- Proof)) :-
	clause(A, B),
	solve(B, Proof).

builtin(A) :- 
	A =.. [Pred | _],
	member(Pred, [arg, assert, asserta, assertz, atom, atomic,
		      bagof, call, clause, close, consult,
		      display, fail, functor, get, get0,
		      integer, is, nonvar, number, nl,
		      print, put, read, retract, see, seeing, seen,
		      setof, sort, tab, tell, telling, told, true, var, write,
		      '<', '=<', '>', '>=', '=', '=..', '==', '\==', '\+' ]).

member(X, [X|_]).
member(X, [_|T]) :- member(X, T).

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

explain(true, Depth, DMax) :- !.

explain((not(A) :- true), Depth, DMax) :-
	Depth < DMax, !,
	nl, tab(Depth*3), write('because it is not true that '), talk(A).

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

explain((A, B), Depth, DMax) :-
	Depth < DMax, !,
	explain(A, Depth, DMax),
	explain(B, Depth, DMax).

explain(_, _, _).

talk(A) :- ptalk(A), !.
talk(A) :- write(A).