/*
solve(Goal,Tree) :-
Tree is a proof tree for Goal given the program
defined by clause/2.
*/
solve(true,true) :- !.
solve((A,B),(ProofA,ProofB)) :- !,
solve(A,ProofA), solve(B,ProofB).
solve(A,(A:-builtin)) :- builtin(A), !, A.
solve(A,(A:-Proof)) :-
clause(A,B), solve(B,Proof).
% Program 17.8 A meta-interpreter for building a proof tree