Rule interpreter 2

Description

A two-level rule interpreter with proof trees

Source: The Art of Prolog

Program source code: rule_interpreter_2.pl

Listing

```/*
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``` 