Różnice między wybraną wersją a wersją aktualną.
|
pl:prolog:pllib:proof_explanation [2019/06/27 15:50] |
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 ===== | ||
| + | <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 ===== | ||
