====== Proof explanation ======
{{tag>proof operators}}
===== Description =====
Explaining a proof

**Source**:  The Art of Prolog
===== Download =====
Program source code: {{proof_explanation.pl}}
===== Listing =====
<code prolog>
/*
    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
</code>
===== Comments =====