Różnice między wybraną wersją a wersją aktualną.
|
pl:prolog:pllib:interpreter_for_hypotheses [2019/06/27 15:50] |
pl:prolog:pllib:interpreter_for_hypotheses [2019/06/27 15:50] (aktualna) |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| + | ====== Interpreter for hypotheses ====== | ||
| + | {{tag>interpreter hypothesis proof}} | ||
| + | ===== Description ===== | ||
| + | A loop-avoiding interpreter for hypotheses. | ||
| + | |||
| + | **Source**: PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7. | ||
| + | ===== Download ===== | ||
| + | Program source code: {{interpreter_for_hypotheses.pl}} | ||
| + | ===== Listing ===== | ||
| + | <code prolog> | ||
| + | % Figure 19.3 A loop-avoiding interpreter for hypotheses. | ||
| + | |||
| + | |||
| + | % Interpreter for hypotheses | ||
| + | % prove( Goal, Hypo, Answ): | ||
| + | % Answ = yes, if Goal derivable from Hypo in at most D steps | ||
| + | % Answ = no, if Goal not derivable | ||
| + | % Answ = maybe, if search terminated after D steps inconclusively | ||
| + | |||
| + | prove( Goal, Hypo, Answer) :- | ||
| + | max_proof_length( D), | ||
| + | prove( Goal, Hypo, D, RestD), | ||
| + | (RestD >= 0, Answer = yes % Proved | ||
| + | ; | ||
| + | RestD < 0, !, Answer = maybe % Maybe, but it looks like inf. loop | ||
| + | ). | ||
| + | | ||
| + | prove( Goal, _, no). % Otherwise Goal definitely cannot be proved | ||
| + | |||
| + | % prove( Goal, Hyp, MaxD, RestD): | ||
| + | % MaxD allowed proof length, RestD 'remaining length' after proof; | ||
| + | % Count only proof steps using Hyp | ||
| + | |||
| + | prove( G, H, D, D) :- | ||
| + | D < 0, !. % Proof length overstepped | ||
| + | |||
| + | prove( [], _, D, D) :- !. | ||
| + | |||
| + | prove( [G1 | Gs], Hypo, D0, D) :- !, | ||
| + | prove( G1, Hypo, D0, D1), | ||
| + | prove( Gs, Hypo, D1, D). | ||
| + | |||
| + | prove( G, _, D, D) :- | ||
| + | prolog_predicate( G), % Background predicate in Prolog? | ||
| + | call( G). % Call of background predicate | ||
| + | |||
| + | prove( G, Hyp, D0, D) :- | ||
| + | D0 =< 0, !, D is D0-1 % Proof too long | ||
| + | ; | ||
| + | D1 is D0-1, % Remaining proof length | ||
| + | member( Clause/Vars, Hyp), % A clause in Hyp | ||
| + | copy_term( Clause, [Head | Body] ), % Rename variables in clause | ||
| + | G = Head, % Match clause's head with goal | ||
| + | prove( Body, Hyp, D1, D). % Prove G using Clause | ||
| + | </code> | ||
| + | ===== Comments ===== | ||
