/* monitor(Goal,Proof) :- Succeeds if a result of yes is returned from solving Goal at the solve level, in which case Proof is a proof tree representing the successful computation, or when the end of the computation is reached, in which case Proof is a list of failure branches since the last success. */ :- op( 900, fy, not). :- op(40,xfy,&). :- op(30,xf,is_true). monitor(Goal,Proof) :- set_search_tree, solve(Goal,Result,Proof), filter(Result,Proof). monitor(Goal,Proof) :- collect_proof(P), reverse(P,P1), Proof = failed(Goal,P1). filter(yes,Proof) :- reset_search_tree. filter(no,Proof) :- store_proof(Proof), fail. /* solve(Goal,Result,Proof) :- Given a set of rules of the form rule(A,B,Name), Goal has Result yes if it follows from the rules and no if it does not. Proof is a proof tree if the result is yes and a failure branch of the search tree if the result is no. */ :- op(40,xfy,because). :- op(30,xfy,with). solve(A,yes,Tree) :- fact(A), Tree = fact(A). solve(A,Result,Tree) :- rule(A,B,Name), solve_body(B,Result,Proof), Tree = A because B with Proof. solve(A,no,Tree) :- not fact(A), not rule(A,B,Name), Tree = no_match(A). solve_body(A&B,Result,Proof) :- solve_body(A,ResultA,ProofA), solve_and(ResultA,B,Result,ProofB), Proof = ProofA & ProofB. solve_body(A is_true,Result,Proof) :- solve(A,Result,Proof). solve_and(no,A,no,unsearched). solve_and(yes,B,Result,Tree) :- solve(B,Result,Tree). % The following predicates use side effects to record and remove % branches of the search tree. collect_proof(Proof) :- retract('search tree'(Proof)). store_proof(Proof) :- retract('search tree'(Tree)), assert('search tree'([ProofjTree])). set_search_tree :- assert('search tree'([ ])). reset_search_tree :- retract('search tree'(Proof)), assert('search tree'([ ])). reverse([],[]). reverse([X|Xs],Zs) :- reverse(Xs,Ys), append(Ys,[X],Zs). % Program 17.21: A two-level rule interpreter with proof trees