# Proof explanation

## Description

Explaining a proof

Source: The Art of Prolog

Program source code: proof_explanation.pl

## Listing

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