Explaining a proof

Source: The Art of Prolog

Program source code: proof_explanation.pl

/*
    explain(Goal)  :-
       Explains how the goal Goal was proved.
*/
    explain(Goal) :-  monitor(Goal,Proof), interpret(Proof).
 
:- op(40,xfy,&).
:- op(30,xf,is_true).
:- op(40,xfy,because).
:- op(40,xfy,with).
 
%    monitor(Goal,Proof)   See Program 17.21.
 
    interpret(ProofA&ProofB) :-
       interpret(ProofA), interpret(ProofB).
    interpret(failed(A,Branches)) :-
       nl, writeln([A,' has failed with the following failure branches:']),
       interpret(Branches).
    interpret([Fail|Fails]) :-
       interpret(Fail), nl, write('NEW BRANCH'), nl,
       interpret(Fails).
    interpret([ ]).
    interpret(fact(A)) :-
       nl, writeln([A,' is a fact in the database.']).
    interpret(A because B with Proof) :-
       nl, writeln([A,' is proved using the rule']),
       display_rule(rule(A,B)), interpret(Proof).
    interpret(no_match(A)) :-
       nl, writeln([A,' has no matching fact or rule in the rule base.']).
    interpret(unsearched) :-
       nl, writeln(['The rest of the conjunct is unsearched.']).
 
    display_rule(rule(A,B)) :-
       write('IF '), write_conjunction(B), writeln(['THEN ',A ]).
 
    write_conjunction(A&B) :-
       write_conjunction(A), write(' AND '),
       write_conjunction(B).
 
    write_conjunction(A is_true) :-  write(A).
 
     writeln([X|Xs]) :- write(X), writeln(Xs).
     writeln([]) :- nl.
 
%    Program 17.22: Explaining a proof