# Różnice

Różnice między wybraną wersją a wersją aktualną.

 — pl:prolog:pllib:proof_explanation [2019/06/27 15:50] (aktualna) Linia 1: Linia 1: + ====== Proof explanation ====== + {{tag>​proof operators}} + ===== Description ===== + Explaining a proof + + **Source**: ​ The Art of Prolog + ===== Download ===== + 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 + ​ + ===== Comments =====
pl/prolog/pllib/proof_explanation.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna)