Proof explanation


Explaining a proof

Source: The Art of Prolog


Program source code:


    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([Fail|Fails]) :-
       interpret(Fail), nl, write('NEW BRANCH'), nl,
    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(A is_true) :-  write(A).
     writeln([X|Xs]) :- write(X), writeln(Xs).
     writeln([]) :- nl.
%    Program 17.22: Explaining a proof


pl/prolog/pllib/proof_explanation.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna) Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0