2 % ailog2
.pl logic engine
for Artificial Intelligence http
://artint
.info
3 % Copyright
(C
) 1997-2012, David Poole
.
4 % This is subject to the GNU Public License
(GPL
). See user manual
for details
.
5 % Designed
for standard Prolog
, but only tested on SWI Prolog
.
6 % It is written
in one file to make it easy to
use:
7 % Get swi
-prolog
, double click on this file
and it should start
!
9 ailog_version
('2.3.6.2',2013).
11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
12 % SYSTEM DEPENDENT CODE
%
13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
15 %% the
keys to stastics don
't seem to be standard. This should cover the cases:
16 %% get_runtime(T,Units) gets accumulated runtime from the system
17 get_runtime(T,U) :- catch((statistics(cputime,T),U=secs),_,
18 (statistics(runtime,[T,_]),U=ms)). % Sicstus/Quintus Prolog
20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21 % OPERATOR DEFINITIONS %
22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25 :- op(1150, xfx, <- ).
26 % <= is the base-level "if" (it is not used here, but can be used in
28 :- op(1120, xfx, <= ).
29 % "&" is the conjunction.
35 % "#=" is can't be equal
37 % ":" is used
for probability declarations
.
40 :- op
(1170, fx
, tell).
42 :- op
(1170, fx
, whynot
).
45 :- op
(1170, fx
, help
).
47 :- op
(1170,fx
,prload
).
51 :- op
(1170,fx
,listing
).
53 :- op
(1170,fx
,askable
).
54 :- op
(1170,fx
,assumable
).
56 :- op
(1170,fx
,observe
).
57 :- op
(1170,fx
,unobserve
).
58 :- op
(1170,fx
,predict
).
59 :- op
(1170,fx
,deterministic
).
60 :- op
(1170,fx
,prob_threshold
).
61 :- op
(1170,fx
,arbitrary
).
66 :- dynamic depth_bound
/1.
68 :- dynamic assumabl
/1.
72 :- dynamic debugging_failure
/0.
73 :- dynamic answer_found
/0.
74 :- dynamic checking_runtime
/0.
75 :- dynamic lastruntime
/1.
77 :- dynamic explanations
/4.
80 :- dynamic
(prob_threshold
)/1.
81 :- dynamic pruned_prob
/1.
86 prob_threshold
(0.000001).
89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94 AILog Version ',V
,' Help','
96 A clause is of the form','
100 Body is an expression made up of','
102 ~ B1 negation as finite failure','
103 B1 & B2 conjunction B1 and B2','
104 where B1 and B2 are expressions.','
106 ***** Basic commands:','
108 tell CLAUSE. add the clause to the knowledge base','
109 askable Atom. makes Atom askable.','
111 ask QUERY. ask if expression QUERY is a consequence of the KB','
112 whynot QUERY. find out why an answer to QUERY was not returned.','
114 allow G. allow goal G to use the Prolog definition.','
115 bound N. set search depth-bound to N (default=30)','
116 listing. list all clauses in the knowledge base.','
117 listing H. list clauses in the knowledge base with head H.','
118 askables. list all askables.','
119 clear. clear the knowledge base','
120 clear asked. clear all user responses','
121 clear H. clear clauses with head H from knowledge base','
122 check. check the knowledge base for undefined predicates','
123 help. print this help message','
124 help prob. prints help on probabilistic reasoning','
125 help abduction. prints help on abductive reasoning','
126 stats runtime. turn on runtime statistics','
128 prolog. exit to Prolog. Type "start." to start ailog again.','
130 ***** Input/Output','
132 load ''Filename''. load the clauses in file Filename','
133 prload ''Filename''. load the clauses in Filename, using Prolog''s syntax.','
134 cd ''directory''. changes directory (folder) for loads']) :-
138 'AILog Version ',V
,' Probabilistic Reasoning Help','
140 This help is for probabilistic reasoning in Ailog. This is not useful
141 if you are a beginner interested in deductive reasoning.','
143 AILog implements a version of the independent choice logic that allows
144 for probabilities on atoms. These atoms should not be the head of clauses.','
146 prob a:p. makes atom a probabilistic with probability p.','
147 prob a1:p1,a2:p2,...,ak:pk. makes atoms ai probabilistic with probability pi.','
148 a''s are exclusive and covering; the p''s must sum to 1.','
150 probs. list all prob assertions.','
152 observe QUERY. observe that QUERY is true','
153 predict QUERY. ask the posterior probability that QUERY is true','
154 observations. list all observations made','
155 unobserve. undo whylast observation','
156 unobserve all. undo all observations','
157 explanations. describe the explanations of the observations','
158 worlds. describe the worlds of the observations','
160 prob_threshold V. set the probability threshold to V in range [0,1]','
161 prob_threshold. get the current probability threshold']) :-
164 help_message
(abduction
,[
165 'AILog Version ',V
,' Abductive Reasoning Help','
167 This help is for abductive reasoning in AILog. This is not useful if
168 you are a beginner interested in deductive reasoning.','
170 Abduction allows the system to make assumptions to prove a goal, as
171 long as the assumptions are consistent.',' The atoms that can be
172 assumed are called assumables.',' You use "false" at the head of a
173 clause to make constraints.',' After adding assumables or more
174 clauses, you need to create nogoods to make sure that inconsistent
175 sets of assumables are found.',' Abduction in AILog does not work
176 satisfactorily with negation as failure.','
178 assumable Atoms. makes (comma-separated) Atoms assumable.','
179 assumables. list all assumables.','
181 create_nogoods construct nogoods.','
182 nogoods list nogoods.'
187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
189 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
192 file_or_command
(C
,command
),!.
194 interpret
(help
) :- !,
197 interpret
(help What
) :-
198 help_message
(What
,Help
),!,
200 interpret
(help What
) :- !,
201 write_all
(['No help on "',What
,'". Type "help." for more information.']).
203 interpret
((tell _
:- _
)) :- !,
204 write_all
(['Illegal rule: ":-" is not a legal implication. Use "<-".']).
205 interpret
((tell C
)) :- !,
208 interpret
((ask Q
)) :- !,
209 retractall
(debugging_failure
),
210 retractall
(answer_found
),
214 interpret
((whynot Q
)) :- !,
216 (explanations
(_
,ETs
,_
,_
)
221 whynotb
(Q
,DB
,_
,ass
([],[],1),_
)
224 interpret
(clear
) :- !,
225 retractall
((_
<- _
)),
226 retractall
(assumabl
(_
)),
228 retractall
(choice
(_
,_
,_
)),
229 retractall
(askabl
(_
)),
230 retractall
(asked
(_
,_
)),
231 retractall
(nogood
(_
,_
)),
232 retractall
(anogood
(_
,_
)),
233 retractall
(explanations
(_
,_
,_
,_
)),
234 retractall
(pruned_prob
(_
)),
235 retractall
(arbit
(_
,_
)),
236 assert
(pruned_prob
(0.0)).
238 interpret
((clear asked
)) :- !,
239 retractall
(asked
(_
,_
)),
240 write_all
(['User responses cleared.']).
242 interpret
((clear H
)) :- !,
243 retractall
((H
<- _
)),
244 retractall
(assumabl
(H
)),
245 ( alt
(A
) , member
(H
:_
, A
)
248 forall
(member
(G
:_
, A
), retract
(choice
(G
,_
,_
)))
250 retractall
(askabl
(H
)),
251 retractall
(asked
(H
,_
)),
252 (H
=(X
,V
) -> retractall
(arbit
(X
,V
));true
).
254 interpret
((stats Cmd
)) :- !,
257 interpret
((prload File
)) :- !,
260 interpret
((load File
)) :- !,
263 interpret
((cd Dir
)) :- !,
264 working_directory
(_
,Dir
).
266 interpret
((cd
)) :- !,
267 working_directory
(_
,'~').
269 interpret
((bound
)) :- !,
271 write_all
(['Current depth bound is ',N
]).
273 interpret
((bound N
)) :- !,
275 retract
(depth_bound
(_
)),
276 asserta
(depth_bound
(N
))
277 ; write_all
(['Depth bound must be an integer'])).
282 interpret
(check
) :- !,
285 interpret
((observe G
)) :- !,
288 interpret
((predict G
)) :- !,
291 interpret
(askables
) :-
293 write_all
(['askable ',G
,'.']),
295 interpret
(askables
) :- !.
297 interpret
(assumables
) :-
299 write_all
(['assumable ',G
,'.']),
301 interpret
(assumables
) :- !.
303 interpret
(arbitraries
) :-
305 write_all
(['arbitrary ',X
=V
,'.']),
307 interpret
(arbitraries
) :- !.
313 write_all
(['prob ',A
,':',P1
,'.'])
316 writeAllDelim
(L
,', '),
321 interpret
(probs
) :- !.
323 interpret
((listing
)) :- !,
324 interpret
((listing _
)),
326 interpret
(assumables
),
328 interpret
(arbitraries
).
330 interpret
((listing H
)) :-
333 -> write_all
([H
,'.'])
334 ; write_all
([H
,' <- ',B
,'.'])
337 interpret
((listing _
)) :- !.
339 interpret
(unobserve all
) :- !,
340 retractall
(explanations
(_
,_
,_
,_
)),
341 retractall
(pruned_prob
(_
)),
342 assert
(pruned_prob
(0.0)).
344 interpret
(unobserve
) :- !,
345 (retract
(explanations
(_
,_
,_
,_
))
348 explanations
(_
,_
,_
,Err
)
350 retractall
(pruned_prob
(_
)),
351 assert
(pruned_prob
(Err
))
353 retractall
(pruned_prob
(_
)),
354 assert
(pruned_prob
(0.0))
358 write_all
(['No observations to undo.'])
361 interpret
(observations
) :- !,
362 (explanations
(Obs
,_
,_
,_
) ->
363 print_observations
(Obs
,_
)
364 ; write_all
(['There are no observations.'])).
366 interpret
(explanations
) :- !,
367 (explanations
(_
,ETs
,_
,_
) ->
368 print_explanations
(ETs
,0)
369 ; write_all
(['There are no observations.'])).
371 interpret
(worlds
) :- !,
372 (explanations
(Obs
,Expls
,Pr
,Err
) ->
373 extract_expls
(Expls
,Sexpls
),
374 make_disjoint
(Sexpls
,Worlds
),
375 print_worlds
(Worlds
,0),
378 write_all
(['P(',Obs
,') = ',Pr
])
381 write_all
(['P(',Obs
,') = [',Pr
,',',Max
,']'])
383 ; write_all
(['There are no observations.'])).
385 interpret
(prob_threshold V
) :-
386 (number
(V
), V
>=0.0, V
=<1.0)
388 retract
(prob_threshold
(_
)),
389 assert
(prob_threshold
(V
))
391 write_all
(['Argument to prob_threshold must be in range [0,1].']).
392 interpret
(prob_threshold
) :-
394 write_all
(['Probability threshold is ',V
]).
397 interpret
(nogoods
) :- !,
400 interpret
((A
<- B
)) :- !,
401 write_all
(['Illegal command, ',(A
<- B
),'. You have to "tell" a clause.']).
404 write_all
(['Unknown Command, ',C
,'. Type "help." for help.']).
406 % listifyProbs
(St
,L0
,L1
,S0
,S1
)
407 % St is a probability structure
408 % L1
-L0 is thhe list corresponding to the structure
409 % S1
-S0 is the sum of the probabilities
410 listifyProbs
((X
,Y
),L0
,L2
,S0
,S2
) :- !,
411 listifyProbs
(X
,L0
,L1
,S0
,S1
),
412 listifyProbs
(Y
,L1
,L2
,S1
,S2
).
413 listifyProbs
((A
:P
),L0
,[A
:P
|L0
],S0
,S1
) :-
414 % atomic
(A
), % we want it to mean its a ailog atom
419 % file_or_command
(C
,W
) C is a command that can be
in a file
or on the
420 % command line
, W is either command
or file
421 file_or_command
((askable G
),_
) :- !,
424 file_or_command
((assumable G
),_
) :- !,
427 file_or_command
((allow G
),_
) :- !,
428 assertz
(builtin
(G
,true
)).
431 file_or_command
((prob A
:P
),W
) :- !,
432 (number
(P
), P
>=0, P
=<1 ->
434 assertz
(alt
([A
:P
,~A
:P1
])),
435 assertz
(choice
(A
,P
,[~A
])),
436 assertz
(choice
(~A
,P1
,[A
]))
438 legal_arithmetic_expression
(P
) ->
439 assertz
(alt
([A
:P
,~A
:(1-P
)])),
440 assertz
(choice
(A
,P
,[~A
])),
441 assertz
(choice
(~A
,(1-P
),[A
]))
446 write_all
(['Error: ',(prob A
:P
)])
448 write_all
(['Probability must be a number or expression in range [0,1]'])
451 file_or_command
((prob APs
),W
) :- !,
452 ( (listifyProbs
(APs
,[],L
,0,Sum
) )%, Sum
> 0.9999999999999, Sum
< 1.0000000000001)
454 normalise
(L
,Sum
*1.0,LN
),
460 write_all
(['Error: ',(prob APs
)])
462 write_all
(['Error: command should be: prob a1:p1,a2:p2,...,ak:pk.']),
463 write_all
([' the pi''s must be nonnegative and sum to 1.0'])
466 file_or_command
((arbitrary A
),W
) :- !,
473 write_all
(['Error: ',(arbitrary A
)])
475 write_all
(['Error: command should be: arbitrary X=V.']).
478 file_or_command
((deterministic G
),_
) :- !,
481 file_or_command
(create_nogoods
,_
) :- !,
483 construct_nogoods
(DB
).
486 legal_arithmetic_expression
(N
) :- var
(N
),!.
487 legal_arithmetic_expression
(N
) :- number
(N
),!.
488 legal_arithmetic_expression
(E1
+E2
) :- !,
489 legal_arithmetic_expression
(E1
),
490 legal_arithmetic_expression
(E2
).
491 legal_arithmetic_expression
(E1
-E2
) :- !,
492 legal_arithmetic_expression
(E1
),
493 legal_arithmetic_expression
(E2
).
494 legal_arithmetic_expression
(E1
*E2
) :- !,
495 legal_arithmetic_expression
(E1
),
496 legal_arithmetic_expression
(E2
).
497 legal_arithmetic_expression
(E1
/E2
) :- !,
498 legal_arithmetic_expression
(E1
),
499 legal_arithmetic_expression
(E2
).
501 % make_assumable makes an atom
or a comma
-separated atoms assumable
.
502 make_assumable
((A
,B
)) :- !,
507 assertz
(assumabl
(G
)).
510 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
512 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
515 illegal_body
(Q
,Why
),!,
516 write_all
(['Illegal query: '|Why
]).
518 retractall
(failed
(_
)),
519 assert
(failed
(naturally
)),
521 solve
(Q
,DB
,Res
,[wrule
(yes
,true
,Q
,true
)],ass
([],[],1),Ass
),
522 (answer_found
-> true
; assert
(answer_found
)),
523 mynumbervars
((Q
,Res
,Ass
),0,_
),
528 -> write_all
(['No more answers.'])
529 ; write_all
(['No. ',Q
,' doesn''t follow from the knowledge base.'])),
535 write_all
(['Query failed due to depth-bound ',DB
,'.']),
537 writel
([' [New-depth-bound,where,ok,help]: ']),
538 flush_and_read
(Comm
),
539 interpret_failing_question
(Comm
,Q
,DB
).
541 % interpret_failing_question
(Comm
,Q
,DB
).
542 interpret_failing_question
(help
,Q
,DB
) :- !,
544 ' Give one of the following commands:',nl
,
545 ' an integer > ',DB
,' to use this depth bound.',nl
,
546 ' (use "bound N." to set it permanently).',nl
,
547 ' where. to explore the proof tree where the depth-bound was reached.',nl
,
548 ' ok. to return to the ailog prompt.',nl
,
549 ' help. to print this message.']),
551 interpret_failing_question
(end_of_file
,_
,_
) :- !.
552 interpret_failing_question
(ok
,_
,_
) :- !.
553 interpret_failing_question
(where
,Q
,DB
) :-
554 assert
(debugging_failure
),
556 interpret_failing_question
(Comm
,Q
,_
) :-
559 interpret_failing_question
(Comm
,Q
,DB
) :-
560 write_all
([' Unknown command, ',Comm
,' type "help." for help.']),
563 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
565 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
567 tell_clause
((~ H
<- B
)) :- !,
568 write_all
(['Illegal rule: ~',H
,' <- ',B
,'.',nl
,
569 'You cannot have negation in the head of a clause.']).
570 tell_clause
((H1
& H2
<- B
)) :- !,
571 write_all
(['Illegal rule: ',H1
& H2
,' <- ',B
,'.',nl
,
572 'You cannot have a conjunction in the head of a clause.']).
573 tell_clause
((H1
, H2
<- B
)) :- !,
574 write_all
(['Illegal rule: ',H1
,',', H2
,' <- ',B
,'.',nl
,
575 'You cannot have a "," in the head of a clause.']).
576 tell_clause
((H
<- B
)) :-
579 write_all
([H
,' is built-in. It cannot be redefined.'])
580 ; illegal_body
(B
,Why
) ->
581 write_all
(['Illegal rule: ',H
,'<-',B
,'. '|Why
])
582 ; assertz
((H
<- B
))).
583 tell_clause
((H
:- B
)) :-
585 write_all
(['Illegal rule: ',H
,':-',B
,'. ":-" is not a legal implication. Use "<-".']).
586 tell_clause
((A
, B
)) :-
588 write_all
(['Error: ',(A
,B
),' is not a valid clause.']).
589 tell_clause
((A
& B
)) :-
591 write_all
(['Error: ',(A
&B
),' is not a valid clause.']).
594 write_all
(['Error: ',~A
,' is not a valid clause.']).
597 write_all
([H
,' is built-in. It cannot be redefined.']).
600 assertz
((H
<- true
)).
602 illegal_body
(X
,['Variables cannot be atoms. Use call(',X
,').']) :- var
(X
).
603 illegal_body
((_
,_
),[' "," is not a legal conjunction. Use "&".']).
604 illegal_body
((\
+ _
),[' "\\+" is not a legal negation. Use "~".']).
605 illegal_body
(!,[' "!" is not supported.']).
606 illegal_body
([_
|_
],[' Lists cannot be atoms.']).
608 illegal_body
((A
&_
),Why
) :-
610 illegal_body
((_
&A
),Why
) :-
612 illegal_body
((A
;_
),Why
) :-
614 illegal_body
((_
;A
),Why
) :-
616 illegal_body
((~A
),Why
) :-
619 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
621 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
623 % solve
(Goal
,DepthBnd
,PfTree
,WhyTree
,Ass0
,Ass1
)
624 % Goal is the goal to be proved
625 % DepthBnd is the depth bound
626 % PfTree is the proof tree returned
627 % Whytree is a list of wrule
(Head
,LeftTree
,Current
,RightBody
)
628 % Ass0 is the assumables coming
in.
629 % This is structure of the form ass
(As
,PAs
,P
)
630 % Ass1 is the assumables coming out
631 solve
(true
,_
,true
,_
,Ass
,Ass
) :- !.
632 solve
((A
&B
),N
,(AT
&BT
),[wrule
(H
,LT
,_
,RB
)|WT
],A0
,A2
) :- !,
633 solve
(A
,N
,AT
,[wrule
(H
,LT
,A
,(B
&RB
))|WT
],A0
,A1
),
634 solve
(B
,N
,BT
,[wrule
(H
,(LT
&AT
),B
,RB
)|WT
],A1
,A2
).
636 % The following is tempting
, but doesn
't work if A makes assumptions...
637 % solve((A -> B ; C),N,(AT -> BT;CT),[wrule(H,LT,_,RB)|WT],A0,A2) :-
638 % solve(A,N,AT,[wrule(H,LT,A,(B&RB))|WT],A0,A1) % why rules is wrong
640 % solve(B,N,BT,[wrule(H,(LT&AT),B,RB)|WT],A1,A2)
642 % solve(C,N,CT,[wrule(H,LT,C,RB)|WT],A0,A2).
644 solve(A \= B,_,if(A \= B,builtin),_,A0,A0) :- !,
646 solve(A #= B,_,if(A #= B,builtin),_,A0,A0) :- !,
648 solve(call(G),_,_,WT,A0,A0) :-
650 debug_error([' Error
: argument to call must be bound
when evaluated
.'],
652 solve(call(G),N,T,WT,A0,A1) :- !,
653 solve(G,N,T,WT,A0,A1).
654 solve((~ G),N,if(~G,T),WT,A0,A1) :- !,
656 failtoprove(G,N,T,WT,A0,A1)
658 debug_error([' Error
: ',~G,' needs to be ground
when called
.'],
662 solve(G,_,if(G,assumed),_,ass(A0,PAs,P),ass(A0,PAs,P)) :-
665 % ; debug_error([' Error
: assumable
',G,' needs to be ground
when called
.'],
668 solve(G,_,if(G,assumed),_,ass(A0,PAs,P),ass(A1,PAs,P)) :-
671 % ; debug_error([' Error
: assumable
',G,' needs to be ground
when called
.'],
675 insert_into_sorted_list(G,A0,A1).
676 solve(G,_,if(G,assumed),_,ass(A0,PAs0,P0),ass(A0,PAs1,P1)) :-
679 % ; debug_error([' Error
: assumable
',G,' needs to be ground
when called
.'],
682 insertUpdateProbs(PAs0,P0,G,P,PAs1,P1),
683 prob_threshold(Bound),
686 retract(pruned_prob(PP)),
688 asserta(pruned_prob(PP1)),
694 solve(G=V,_,if(G=V,assumed),_,ass(A0,PAs,P),ass(A1,PAs,P)) :-
700 nonvar(V) -> % this seems to be necessary to get it to work.
701 % The arbitrary choice has not been made, but this call
702 % isn't making the choice
.
710 solve
(G
,_
,if(G
,asked
),WT
,A0
,A0
) :-
713 Ans \
== unknown
,!, % fail
if Ans
=unknown
, otherwise don
't try clauses
715 solve(H,_,if(H,builtin),WT,A0,A0) :-
717 (C -> catch(H,_,debugging_builtin_error(H,WT))
718 ; write_all(['Error
: "',H,'" can
''t be called
in this form
, as
',C,' isn
''t true
.']),
719 debugging_builtin_error(H,WT)
721 solve(H,N0,if(H,BT),WT,A0,A1) :-
726 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1), !.
727 solve(H,N0,if(H,BT),WT,A0,A1) :-
731 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1).
732 solve(H,0,if(H,asked),WT,ass(A0,PAs0,P0),ass(A0,PAs0,P0)) :-
734 debugging_failure_goal(H,WT,P0).
735 solve(_,0,_,_,ass(_,_,P),_) :-
736 retractall(failed(_)),
737 assert(failed(unnaturally)),
739 retract(pruned_prob(PP)),
741 asserta(pruned_prob(PP1)),
744 % report(Query,Res,Ass) report an answer after an ask
745 report(Q,Res,ass([],[],1)) :- !,
746 write_all(['Answer
: ',Q,'.']),
748 writel([' [ok
,more
,how
,help
]: ']),
749 flush_and_read(Comm),
750 interpret_report(Comm,Q,Res,ass([],[],1)).
752 write_all(['Answer
: ',Q,'.']),
753 ( Ass=ass(A0,[],1) ->
754 write_all(['Assuming
: ',A0,'.'])
755 ; write_all(['Assuming
: ',Ass,'.'])),
757 writel([' [more
,ok
,how
,help
]: ']),
758 flush_and_read(Comm),
759 interpret_report(Comm,Q,Res,Ass).
761 % interpret_report(Comm,Q,Res,Ass) interprets the answer given by the user
762 % to an answer given after and ask
763 interpret_report(ok,_,_,_) :- !.
764 interpret_report(more,_,_,_) :- !,
766 interpret_report(end_of_file,_,_,_) :- !,
768 interpret_report(how,Q,Res,Ass) :- !,
770 ( (Rep = top; Rep=up)
773 -> reset_runtime,fail
776 ; write_all(['This shouldn
''t occur
. Traverse reported
',Rep])
778 interpret_report(help,Q,Res,Ass) :- !,
780 ' The
system has proven an instance of your query
.',nl,
781 ' You can give the following commands
:',nl,
782 ' more
. for more answers
',nl,
783 ' ok
. for no more answers
',nl,
784 ' how
. to enter a dialog to determine how the goal was proved
.']),
786 interpret_report(Comm,Q,Res,Ass) :-
788 write_all(['Unknown command
; ',Comm,'. Type
"help." if you need help
.']),
791 % Depth-bound reached
792 % debugging_failure_goal(H,WT,P)
793 % H is the current goal
795 % P is the probability of this proof
796 debugging_failure_goal(H,WT,P) :-
797 write_all([' Depth
-bound reached
. Current subgoal
: ',H,'.']),
798 writel([' [fail
,succeed
,proceed
,why
,ok
,help
]: ']),
799 flush_and_read(Comm),
800 interpret_debugging_failure_command(Comm,H,WT,P).
803 % interpret_debugging_failure_command(Comm,H,WT,P)
804 % Comm is the command the user gave
805 % H is the current goal
807 % P is the probability of this proof
809 interpret_debugging_failure_command(help,H,WT,P) :- !,
811 ' The
system has reached the depth bound
.',nl,
812 ' You can give the following commands
:',nl,
813 ' fail
. fail this subgoal
.',nl,
814 ' succeed
. make this subgoal succeed
.',nl,
815 ' proceed
. fail
and don
''t stop any more at failing subgoals
.',nl,
816 ' why
. determine why this subgoal was called
.',nl,
817 ' ok
. return to ailog prompt
.',nl,
818 ' help
. print this message
.']),
819 debugging_failure_goal(H,WT,P).
820 interpret_debugging_failure_command(fail,_,_,P) :- !,
821 retractall(failed(_)),
822 assert(failed(unnaturally)),
824 retract(pruned_prob(PP)),
826 asserta(pruned_prob(PP1)),
828 interpret_debugging_failure_command(succeed,_,_,_) :- !.
829 interpret_debugging_failure_command(proceed,_,_,P) :- !,
830 retractall(debugging_failure),
831 retractall(failed(_)),
832 assert(failed(unnaturally)),
834 retract(pruned_prob(PP)),
836 asserta(pruned_prob(PP1)),
838 interpret_debugging_failure_command(ok,_,_,_) :- !,
840 interpret_debugging_failure_command(end_of_file,_,_,_) :- !,
842 interpret_debugging_failure_command(why,H,WT,P) :- !,
843 \+ \+ (mynumbervars(WT,0,_),why_question(WT,_)),
844 debugging_failure_goal(H,WT,P).
845 interpret_debugging_failure_command(Comm,H,WT,P) :- !,
846 write_all([' Unknown command
: ',Comm,'. Type
"help." for help
.']),
847 debugging_failure_goal(H,WT,P).
850 % builtin(G,C) is true if goal G is defined in the system (as opposed to
851 % being defined in clauses). C is the condition that must hold to make sure
852 % there are no errors.
853 builtin((A =< B), ground((A =< B))).
854 builtin((A >= B), ground((A >= B))).
855 builtin((A =\= B), ground((A =\= B))).
856 builtin((A < B), ground((A<B))).
857 builtin((A > B), ground((A>B))).
858 builtin((_ is E),ground(E)).
859 builtin(number(E),ground(E)).
860 builtin(atomic(E),ground(E)).
862 % Error in a built-in
863 debugging_builtin_error(H,WT) :-
864 debug_error([' Error
in built
-in predicate
: ',H,'.'],WT).
866 % RUNTIME ERROR HANDLING
867 debug_error(Message,WT) :-
869 writel([' [fail
,succeed
,why
,ok
,help
]: ']),
870 flush_and_read(Comm),
871 interpret_error_command(Comm,Message,WT).
873 interpret_error_command(help,Message,WT) :- !,
874 % write_all(Message),
876 ' You can give the following commands
:',nl,
877 ' fail
. fail this subgoal
.',nl,
878 ' succeed
. make this subgoal succeed
.',nl,
879 ' why
. determine why this subgoal was called
.',nl,
880 ' ok
. return to ailog prompt
.',nl,
881 ' help
. print this message
.']),
882 debug_error(Message,WT).
883 interpret_error_command(fail,_,_) :- !,
885 interpret_error_command(succeed,_,_) :- !.
886 interpret_error_command(ok,_,_) :- !,
888 interpret_error_command(end_of_file,_,_) :- !,
890 interpret_error_command(why,H,WT) :- !,
891 \+ \+ (mynumbervars(WT,0,_),why_question(WT,_)),
893 interpret_error_command(Comm,H,WT) :- !,
894 write_all([' Unknown command
: ',Comm,'. Type
"help." for help
.']),
897 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
899 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
902 % G is the goal to ask
907 asked(G,Ans1),!,Ans=Ans1.
908 ask_user(G=V,_,yes) :-
910 asked(G=V1,yes),!,V=V1.
912 ask_user(T=V,WT,Ans) :-
914 writel(['What is the value of
',T,'?
[value
,unknown
,why
,help
]: ']),
915 flush_and_read(Reply),
916 (member(Reply,[unknown,why,help])
917 -> interpret_ask_answer(Reply,T=V,WT,Ans)
919 interpret_ask_answer(yes,T=V,WT,Ans)
921 ask_user(G,WT,Ans) :-
923 writel(['Is
',G,' true?
[yes
,no,unknown
,why
,help
]: ']),
925 interpret_ask_answer(Rep,G,WT,Ans).
927 ask_user(G,WT,fail) :-
928 write_all([' Error
: Askables with free variables
not implemented
.',nl,
929 ' The
system wanted to ask
',G,'.',nl,
930 ' Entering why interation
.']),
931 mynumbervars(WT,0,_),
933 write_all([' Askable subgoal
',G,' failing due to free variables
.']).
936 % interpret_ask_answer(Rep,G,WT,Ans).
937 interpret_ask_answer(help,G,WT,Rep) :- !,
938 write_all([' The
system is asking whether
',G,' is true
or not. Give one of
:',nl,
939 ' "yes." if ',G,' is known to be true
.',nl,
940 ' "no." if ',G,' is known to be false
.',nl,
941 ' "unknown." if ',G,' is unknown
(so applicable clauses can be used
).',nl,
942 ' "fail." to fail the subgoal
(but
not record an answer
).',nl,
943 ' "why." to see why the
system was asking this question
.',nl,
944 ' "prompt." to
return to the ailog prompt
.',nl,
945 ' "help." to
print this message
.']),
947 interpret_ask_answer(yes,G,_,yes) :- !,
948 assertz(asked(G,yes)).
949 interpret_ask_answer(no,G,_,no) :- !,
950 assertz(asked(G,no)).
951 interpret_ask_answer(unknown,G,_,unknown) :- !,
952 assertz(asked(G,unknown)).
953 interpret_ask_answer(fail,_,_,fail) :- !.
954 interpret_ask_answer(prompt,_,_,_) :- !,
956 interpret_ask_answer(end_of_file,_,_,_) :- !,
960 interpret_ask_answer(why,G,WT,Rep) :- !,
961 \+ \+ ( mynumbervars(WT,0,_),why_question(WT,Rep),Rep \== prompt),
963 interpret_ask_answer(Ans,G,WT,Rep) :-
965 write_all([' Unknown response
"',Ans,'". For help type
"help.".']),
969 % why_question(WT,Rep)
970 % WT is a list of wrule(Head,LeftTree,Current,RightBody)
971 % Rep is the reply. It is one of:
972 % down go back one step
973 % bottom return to the ask-the-user query
974 % prompt return to prompt
975 why_question([wrule(H,LT,C,RB)|WT],Rep) :-
976 write_all([' ',C,' is used
in the rule
']),
977 write_all([' ',H,' <-']),
978 print_tree_body(LT,1,Max),
979 write_all([' ** ',Max,': ',C]),
982 writel([' [Number
,why
,help
,ok
]: ']),
983 flush_and_read(Comm),
984 interpret_why_ans(Comm,Max,[wrule(H,LT,C,RB)|WT],Rep).
985 why_question([],down) :-
986 write_all([' This was the original query
.']).
988 % interpret_why_ans(Comm,[wrule(H,LT,C,RB)|WT],Rep).
989 interpret_why_ans(help,Max,[wrule(H,LT,C,RB)|WT],Rep) :- !,
991 ' You can taverse the proof
for a subgoal using following commands
:',nl,
992 ' how i
. show how element i
(i
<',Max,') of the body was proved
.',nl,
993 ' how
',Max,'. show the rule being considered
for ',C,'.',nl,
994 ' why
. show why
',H,' is being proved
.',nl,
995 ' prompt
. return to the ailog prompt
.',nl,
996 ' help
. print this message
.']),
997 why_question([wrule(H,LT,C,RB)|WT],Rep).
998 interpret_why_ans(up,_,WT,Rep) :- !,
999 interpret_why_ans(why,_,WT,Rep).
1000 interpret_why_ans(why,_,[WR|WT],Rep) :- !,
1001 why_question(WT,Rep1),
1003 -> why_question([WR|WT],Rep)
1005 interpret_why_ans((how N),Max,[wrule(H,LT,C,RB)|WT],Rep) :-
1007 interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep).
1008 interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep) :-
1014 (Rep1=up -> why_question([wrule(H,LT,C,RB)|WT],Rep) ;
1015 Rep1=top -> Rep=bottom ;
1017 -> write_all([' retry doesn
''t make sense here
.']),
1018 why_question([wrule(H,LT,C,RB)|WT],Rep) ;
1020 interpret_why_ans(Max,Max,_,down) :- !.
1021 interpret_why_ans(N,Max,WT,Rep) :-
1024 write_all(['You can
''t trace this
, as it hasn
''t been proved
.']),
1025 why_question(WT,Rep).
1026 interpret_why_ans(end_of_file,_,_,_) :- !,
1029 interpret_why_ans(prompt,_,_,_) :- !,
1031 interpret_why_ans(ok,_,_,bottom) :- !.
1033 interpret_why_ans(Comm,_,WT,Rep) :- !,
1034 write_all(['Unknown command
: ',Comm,'. Type
"help." for help
.']),
1035 why_question(WT,Rep).
1038 % print_body(B,N) is true if B is a body to be printed and N is the
1039 % count of atoms before B was called.
1040 print_body(true,N,N) :- !.
1041 print_body((A&B),N0,N2) :- !,
1042 print_body(A,N0,N1),
1043 print_body(B,N1,N2).
1044 print_body(H,N,N1) :-
1045 write_all([' ',N,': ',H]),
1050 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1051 %% NEGATION AS FAILURE
1052 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1054 % failtoprove(G,N,T,WT,A0,A1)
1055 % G is a ground goal,
1056 % N is a depth-bound
1057 % T is the tree returned
1058 % WT is the why tree
1059 % A0 is the assumables before and A1 is the set after
1060 % The complication here is due to the interaction with the depth-bound
1063 failtoprove(G,N,nafproof(PA1,ETs),WT,ass(A,PAs,Pr),ass(A,PA1,Pr1)) :-
1064 failed(HowFailedInit),
1065 retractall(failed(_)),
1066 assert(failed(naturally)),
1067 findall(et(Ass,T),solve(G,N,T,~WT,ass(A,PAs,Pr),Ass),ETs),
1068 (failed(naturally) ->
1069 extract_expls(ETs,EGs),
1070 duals(EGs,PAs,[PAs],Ds),
1074 member(et(ass(A,PAs,Pr),_),ETs) -> % found a proof with no assumptions
1075 retractall(failed(_)),
1076 assert(failed(HowFailedInit)),
1077 fail % fail naturally
1079 fail % fail unnaturally as depth-bound was hit
1082 /* interaction with depth-bound
1083 (failed(naturally) ->
1084 (solve(G,N,_,WT,[],_) ->
1085 retract(failed(unnaturally)), asserta(failed(naturally)),fail
1086 % note this just fails if failed(naturally) still true
1089 ; retract(failed(_)),
1090 assert(failed(naturally)),
1091 (solve(G,N,_,WT,[],_) ->
1092 retract(failed(naturally)), asserta(failed(unnaturally)),fail
1093 ; retract(failed(naturally)), asserta(failed(unnaturally))
1094 % note this just fails if failed(unnaturally) still true
1100 % AL is a list of probabilistic assumables
1103 prob([H|T],P0,P2) :-
1109 % The following code gives the interaction between negation and probabilities
1111 % A composite choice is a consistent set of probabilistic assumables.
1113 % duals(Es,R0,D0,D1) is true if Es is a list of terms of the form
1114 % ass(A,PAs,Pr) where R0 is a subset of PAs, and
1115 % D1-D0 is a list of ass(A1,R1,P1) such that
1116 % R1-R0 is a hitting set of negations of Es.
1119 duals([S|L],R0,D0,D2) :- !,
1121 hit_every_complement(NA,D0,[],D1),
1124 % hit_every_complement(S,R0,D0,D,D1) is true if S is a composite choice (with
1125 % tail R0), and D2 is D together with the hitting set of negations of
1128 hit_every_complement([],_,D0,D0) :- !.
1129 hit_every_complement([A|R],Ds,D0,D2) :-
1131 hit_every_element(NAs,Ds,D0,D1),
1132 hit_every_complement(R,Ds,D1,D2).
1134 % hit_every_element(As,A,D0,D1) is true if S is a composite choice (with
1135 % tail R0), and D2 is D together with the hitting set of negations of
1138 hit_every_element([],_,D,D).
1139 hit_every_element([E|T],Es,D0,D2) :-
1140 insert_into_each_exp(Es,E,D0,D1),
1141 hit_every_element(T,Es,D1,D2).
1143 % insert_into_each_exp(L,A,L0,L1) is true if inserting atomic choice A
1144 % into each explanation in L, and adding these to L0 produces L1. L,
1145 % L0 and L1 are all lists of explanations. Subsumed and inconsistent
1146 % explanations are removed.
1148 insert_into_each_exp([],_,L,L) :-!.
1149 insert_into_each_exp([E1|R],A,L0,L1) :-
1150 incompatible(A,E1),!,
1151 insert_into_each_exp(R,A,L0,L1).
1152 insert_into_each_exp([E1|R],A,L0,L2) :-
1153 insert_into_sorted_list(A,E1,E2),
1154 insert_exp(E2,L0,L1),
1155 insert_into_each_exp(R,A,L1,L2).
1157 % insert_exp(E,Es1,Es2) is true if inserting explanation E into list
1158 % Es1 of explanations produces list of explanations Es2.
1159 insert_exp(E,[],[E]) :- !.
1160 insert_exp(E0,[E|T],[E|T]) :-
1161 subset_sorted(E,E0),!. % includes the case where E0==E.
1162 insert_exp(E0,[E|T],R) :-
1163 subset_sorted(E0,E),!,
1165 insert_exp(E,[H|T],[H|R]) :-
1168 % mutually_incompatible(As1,As2) is true if A is inconsistent with all of As.
1169 mutually_incompatible(E1,E2) :-
1173 % incompatible(A,As) is true if A is inconsistent with all of As.
1174 incompatible(A,E) :-
1176 \+ consistent(E,NAs).
1179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1181 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1183 % normalize(L,Sum,LS) Sum is assumed to be a float.
1185 normalise([(A:P)|R],S,[(A:PN)|RN]) :-
1192 setof(AA,P1^member(AA:P1,L0),Alts),
1193 assertz(choice(A,P,Alts)),
1197 % insertUpdateProbs(PAs0,P0,G,P,PAs1,P1)
1198 % PAs0 is the initial probabilistic assumptions
1199 % P0 is the probability of the probablistic assumptions
1201 % P is the probability of G
1202 % PAs1 is the resulting probabilistic assumptions
1203 % P1 is the resulting probability
1204 insertUpdateProbs([],P0,G,P,[G],P1) :-
1206 insertUpdateProbs([G|R],P0,G,_,[G|R],P0) :- !.
1207 insertUpdateProbs([G0|R0],P0,G,P,[G,G0|R0],P1) :-
1210 insertUpdateProbs([G0|R0],P0,G,P,[G0|PAs1],P1) :-
1211 insertUpdateProbs(R0,P0,G,P,PAs1,P1).
1213 % latest_explanations(Obervations,ETs,Prob,Err)
1214 % ETs is a list of et(Explanation,ProofTree)
1215 latest_explanations(O,E,P,Err) :-
1216 explanations(O,E,P,Err),!.
1217 latest_explanations([],[et(ass([],[],1),null)],1,0.0).
1220 % Warning: this may not work properly with multiple answers + errors
1221 % We should really reset the pruned_prob for each proof...
1223 latest_explanations(_,ETs,Pr0,Err0),
1224 retractall(pruned_prob(_)),
1225 assert(pruned_prob(Err0)),
1227 retractall(failed(_)),
1228 assert(failed(naturally)),
1230 find_expls(G,ETs,DB,Expls),
1231 extract_expls(Expls,Sexpls),
1232 make_disjoint(Sexpls,DExpls),
1233 acc_probs(DExpls,0,Pr),
1235 report_expls(Expls,DExpls,G,Pr0,Pr,Err0,Err1).
1237 write_all(['No
(more
) answers
.']).
1241 retractall(debugging_failure),
1242 retractall(failed(_)),
1243 assert(failed(naturally)),
1244 latest_explanations(Obs,ETs,PrObs,Err0),
1245 retractall(pruned_prob(_)),
1246 assert(pruned_prob(Err0)),
1249 find_expls(G,ETs,DB,Expls),
1250 extract_expls(Expls,Sexpls),
1251 make_disjoint(Sexpls,DExpls),
1252 acc_probs(DExpls,0,Pnew),
1254 asserta(explanations([G|Obs],Expls,Pnew,Err1)),
1255 report_expls(Expls,DExpls,G,PrObs,Pnew,Err0,Err1).
1257 write_all(['No
(more
) answers
.']).
1259 % find_expls(G,ETs,DB,Expls)
1260 % +G is the goal to be solved
1261 % +ETs is the list of explanations of previous observations
1262 % +DB is the depth-bound
1263 % -Expls is the list of explanations of G and the previous observations
1264 find_expls(G,ETs,DB,Expls) :-
1266 E0^Tr^( member(et(E0,Tr),ETs),
1267 solve(G,DB,Res,[wrule(yes,true,G,true)],E0,Expl)),
1271 ; write_all(['Warning Explanations
not ground
: ',Expls])).
1273 % report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1)
1274 % +Ets is a list of et(Explanation,ProofTree)
1275 % +DExpls is a set of possible worlds (disjoint explanations)
1277 % +Pr0 is the probability of the previous observations
1278 % +Pr1 is the probability of the current observations
1279 % +Err0 is the error (pruned probability mass) before the query
1280 % +Err1 is the error (pruned probability mass) after the query Err1>Err0
1281 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-
1286 Min is Pr1/(Pr0+Err0),
1287 Max is (Pr1+Err1)/(Pr0+Err0),
1290 write_all(['Answer
: P
(',G,'|Obs
)=',Post,'.']),
1292 writel([' [ok
,more
,explanations
,worlds
,help
]: ']),
1293 flush_and_read(Comm),
1294 interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1296 % acc_probs(Expls,P0,P1) determines the probabilities of the assumables in Expls
1297 % +Expls is a list of explanations
1298 % +P0 is the previous probability
1299 % -P1 is the new probability
1301 acc_probs([A|R],P0,P2) :-
1306 % probs_expl(Expl,P0,P1) determines the probability of an expanation
1307 % +Expl is an explanation
1308 % +P0 is the previous probability
1309 % -P1 is the resulting probability (P1 = P0*prob(Expl))
1311 prob_expl([A|R],P0,P2) :-
1316 % interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1)
1317 % +Comm is the command given by the user
1318 % +Expls is the set of explanations
1319 % +DExpls is the set of worlds (disjoint explanations)
1320 % +G is the goal to be proved
1321 % +Pr0 is the probability of the previous observations
1322 % +Pr1 is the probability of the current observations
1323 interpret_prob_report(ok,_,_,_,_,_,_,_) :- !.
1324 interpret_prob_report(more,_,_,_,_,_,_,_) :- !,
1326 interpret_prob_report(end_of_file,_,_,_,_,_,_,_) :- !,
1328 interpret_prob_report(explanations,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1329 show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1330 interpret_prob_report(worlds,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1331 print_worlds(DExpls,0),
1332 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1333 interpret_prob_report(help,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1335 ' The
system has proven an instance of your query
.',nl,
1336 ' You can give the following commands
:',nl,
1337 ' more
. for more answers
',nl,
1338 ' ok
. for no more answers
',nl,
1339 ' explanations
. to explore how the goal is proved based
',
1340 ' sets of assumptions
.',nl,
1341 ' worlds
. to see the worlds where
',G,' is true
.']),
1342 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1343 interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-
1345 write_all(['Unknown command
; ',Comm,'. Type
"help." if you need help
.']),
1346 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1348 % show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1)
1349 show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-
1350 print_explanations(Expls,0),
1351 writel([' [ok
,more
,how i
,help
]: ']),
1352 flush_and_read(Comm),
1353 interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1355 % interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1)
1356 interpret_show_explanations_report(ok,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1357 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1358 interpret_show_explanations_report(more,_,_,_,_,_,_,_) :- !,
1360 interpret_show_explanations_report(how I,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-
1363 ith(Expls,et(_,Tree),I,0),
1364 traverse(Tree,_) % Report is ignored
1368 write_all(['Number out of range
: how
',I,'.'])
1369 ; write_all(['Argument to how must be an integer
: how
',I,'.'])
1372 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1373 interpret_show_explanations_report(help,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1375 'ok
. go back to answer dialogue
',nl,
1376 'more
. get another answer
.',nl,
1377 'how i
. ask how the ith explanation was proved
',nl,
1378 'help
. print this message
']),
1379 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1380 interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,
1382 'Unknown command
: ',Comm,'. Type
"help." for help
']),
1383 report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).
1385 % print_explanations(DExpls,Count).
1386 print_explanations([],_).
1387 print_explanations([et(W,_)|R],C) :-
1388 write_all([' ',C,': ', W]),
1390 print_explanations(R,C1).
1392 % print_worlds(DExpls,Count).
1394 print_worlds([W|R],C) :-
1396 write_all([' ',C,': ', W,' Prob
=',Pr]),
1400 % print_observations(Obs,N)
1401 print_observations([],0).
1402 print_observations([O|Os],N1) :-
1403 print_observations(Os,N),
1405 write_all([N1,': ',O]).
1408 % extract_expls(L1,L2) L1 is a list of et(ass(_,E,_),_) and L2 is the
1409 % corresponding list of explanations E.
1410 extract_expls([],[]).
1411 extract_expls([et(ass(_,E,_),_)|L],R1) :-
1415 % make_disjoint(L,SL) is true if L is a list of explanations and SL
1416 % is a lists of Expl such that SL are mutually exclusive and cover
1417 % the same worlds as the Expls in L.
1418 % This assumes that L is a minimal set: no member of L is a subset of another.
1420 make_disjoint([],[]).
1421 make_disjoint([R|L],L2) :-
1425 \+ mutually_incompatible(R,R1),!,
1426 (member(E,R1), \+ idmember(E,R) %%% was \+ member(E,R)
1427 -> true; write_all(['Error
in make_disjoint
: ',compatible(R,R1)]),fail),
1429 split([E|NE],R,L,L1),
1430 make_disjoint(L1,L2).
1431 make_disjoint([E|L1],[E|L2]) :-
1432 make_disjoint(L1,L2).
1434 % split(As,R,L0,L1) splits R on As, added to L0 produces L1
1436 split([A|As],E,L0,L2) :-
1437 insert_into_sorted_list(A,E,E1),
1438 insert_exp(E1,L0,L1),
1442 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1444 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1446 % traverse(T,Rep) true if
1447 % T is a tree being traversed
1448 % Rep is the reply it is one of {up,top,retry,prompt}
1449 % up means go up in the tree
1450 % top means go to the top of the tree (where traverse was called).
1451 % retry means find another proof tree
1452 % prompt means go to the top level prompt
1453 traverse((A&B),Rep) :-
1454 traverse(if(yes,(A&B)),Rep).
1455 traverse(if(H,true),up) :- !,
1456 write_all([' ',H,' is a fact
']).
1457 traverse(if(H,builtin),up) :- !,
1458 write_all([' ',H,' is built
-in.']).
1459 traverse(if(H,asked),up) :- !,
1460 write_all([' You told me
',H,' is true
.']).
1461 traverse(if(H,assumed),up) :- !,
1462 write_all([' ',H,' is assumed
.']).
1463 traverse(if(~G,nafproof(_,[])),Rep) :- !,
1464 write_all([' ',G,' finitely failed
. You can examine the search space
.']),
1466 whynotb(G,DB,Rep,ass([],[],1),_).
1467 traverse(if(~G,nafproof(Expl,ETs)),Rep) :- !,
1468 write_all([' ',~G,' succeeded assuming
',Expl]),
1469 write_all([' ',G,' succeeded with the following explanations
:']),
1470 print_explanations(ETs,0),
1471 writel([' [up
,top
,retry
,prompt
,how i
,help
,whynot
]: ']),
1472 flush_and_read(Comm),
1473 interpret_naf_how(Comm,ETs,Rep0),
1475 traverse(if(~G,nafproof(Expl,ETs)),Rep)
1478 traverse(null,top) :- !,
1479 write_all([' There was nothing to be proved
.']).
1480 traverse(if(H,B),Rep) :-
1481 write_all([' ',H,' <-']),
1482 print_tree_body(B,1,Max),
1483 writel([' How?
[Number
,up
,retry
,ok
,prompt
,help
]: ']),
1484 flush_and_read(Comm),
1485 interpretcommand(Comm,B,Max,if(H,B),Rep).
1487 % print_tree_body(B,N) is true if B is a body to be printed and N is the
1488 % count of atoms before B was called.
1489 print_tree_body(true,N,N).
1490 print_tree_body((A&B),N0,N2) :-
1491 print_tree_body(A,N0,N1),
1492 print_tree_body(B,N1,N2).
1493 print_tree_body(if(H,_),N,N1) :-
1494 write_all([' ',N,': ',H]),
1497 % interpretcommand(Comm,B,Max,Goal,Reply) interprets the command Comm on body B
1498 interpretcommand(help,_,Max,G,Rep) :- !,
1500 ' Give either
(end
each command with a period
):',nl,
1501 ' how i
. explain how subgoal i
(i
<',Max,') was proved
.',nl,
1502 ' up
. go up the proof tree one level
.',nl,
1503 ' retry
. find another proof
.',nl,
1504 ' ok
. stop traversing the proof tree
.',nl,
1505 ' prompt
. return to the ailog prompt
.',nl,
1506 ' help
. to
print this message
.']),
1508 interpretcommand((how N),B,Max,G,Rep) :-
1510 interpretcommand(N,B,Max,G,Rep).
1511 interpretcommand(N,B,Max,G,Rep) :-
1521 interpretcommand(N,_,Max,G,Rep) :-
1523 % (N < 1 ; N >= Max,Rep),
1525 write_all(['Number out of range
: ',N,'. Use number
in range
: [1,',M1,'].']),
1527 interpretcommand(up,_,_,_,up) :-!.
1528 interpretcommand(why,_,_,_,up) :-!.
1529 interpretcommand(ok,_,_,_,top) :-!.
1530 interpretcommand(prompt,_,_,_,_) :-!,
1532 interpretcommand(retry,_,_,_,retry) :-!.
1533 interpretcommand(end_of_file,_,_,_,prompt) :-!,
1535 interpretcommand(C,_,_,G,Rep) :-
1536 write_all(['Illegal Command
: ',C,' Type
"help." for help
.']),
1539 % nth(S,N0,N1,N,E) is true if E is the N-th element of structure S
1540 nth((A&B),N0,N2,N,E) :- !,
1543 nth(true,N0,N0,_,_) :- !.
1544 nth(A,N,N1,N,A) :- !,
1549 % interpret_naf_how(Comm,ETs,Report)
1550 % Report is either up, or repeat or whatever travese can report
1551 interpret_naf_how(ok,_,up).
1552 interpret_naf_how(more,_,_) :- !,
1554 interpret_naf_how(how I,Expls,Report) :-
1557 ith(Expls,et(_,Tree),I,0),
1558 traverse(Tree,Report)
1562 write_all(['Number out of range
: how
',I,'.'])
1563 ; write_all(['Argument to how must be an integer
: how
',I,'.'])
1567 interpret_naf_how(help,_,repeat) :- !,
1569 'ok
. go back to answer dialogue
',nl,
1570 'more
. get another answer
.',nl,
1571 'how i
. ask how the ith explanation was proved
',nl,
1572 'help
. print this message
']).
1573 interpret_naf_how(Comm,_,repeat) :- !,
1575 'Unknown command
: ',Comm,'. Type
"help." for help
']).
1578 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1579 %% WHY NOT QUESTIONS for FAILING QUERIES
1580 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1582 % determine why an answer to body Q was not found.
1583 % whynotb(+Q,+DB,-Rep,+Ass0,-Ass1) determine why body Q, with depth-bound DB
1584 % and Ass0 did not find an expected answer
1585 % Rep is the reply it is one of {up,top,retry,prompt}
1586 % up means go up in the tree
1587 % top means go to the top of the tree (where traverse was called).
1588 % retry means find another proof tree
1589 % prompt means go to the top level prompt
1591 whynotb((A & B),DB,Rep,Ass0,Ass2) :-
1592 retractall(failed(_)),
1593 assert(failed(naturally)),
1594 solve(A,DB,Res,[whynot],Ass0,Ass1),
1595 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1,Ass2).
1596 whynotb((A & _),DB,Rep,Ass0,Ass1) :- !,
1597 whynotb(A,DB,Rep,Ass0,Ass1).
1599 whynotb(call(A),DB,Rep,Ass0,Ass1) :- !,
1600 whynotb(A,DB,Rep,Ass0,Ass1).
1602 whynotb((~ A),DB,Rep,Ass0,Ass1) :-
1604 retractall(failed(_)),
1605 assert(failed(naturally)),
1606 findall(et(Ass,T),solve(A,DB,T,[whynot],Ass0,Ass),ETs),
1608 member(et(Ass0,T),ETs)
1609 -> % found a proof with no assumables
1610 write_all([' ',~A,' failed as
',A,' suceeded
. Here is how
:']),
1612 ; (ETs=[], failed(naturally)) ->
1613 write_all([' ',~A,' succeeds
, as
',A,' finitely fails
.']),
1614 whynotb(A,DB,Rep,Ass0,_),
1616 ; failed(unnaturally) ->
1617 write_all([' ',~A,' failed because of the depth
-bound
.']),
1618 whynotb(A,DB,Rep,Ass0,_)
1620 whynotb_expls(A,ETs,Rep)
1624 whynotb((~ A),_,up,Ass0,Ass0) :- !,
1625 write_all([' Error
: ',~A,' needs to be ground
when called
.']).
1627 whynotb(A,_,up,Ass0,Ass0) :-
1631 -> write_all([' ',A,' is built
-in and succeeds
.'])
1632 ; write_all([' ',A,' is built
-in and fails
.']))
1633 ; write_all([' ',A,' is built
-in and is insufficiently instanciated
.'])).
1635 whynotb((A \= B),_,up,Ass0,Ass0) :-
1638 -> write_all([' ',(A \= B),' succeeds as they can never unify
.'])
1639 ; write_all([' ',(A \= B),' fails as they are identical
.'])).
1640 whynotb((A \= B),_,up,Ass0,Ass0) :-
1641 write_all([' ',(A \= B),' cannot be resolved
. It is delayed
.']),
1644 -> write_all([' Resolving delayed
',(A \= B),'. It succeeded
.'])
1645 ; write_all([' Failure due to delayed constraint
, ',(A \= B),'.']),
1647 whynotb((A #= B),_,up,Ass0,Ass0) :-
1649 -> write_all([' ',(A #= B),' succeeds as they can never unify
.'])
1650 ; write_all([' ',(A #= B),' fails as they can unify
.'])).
1653 whynotb(Q,_,up,ass(A0,PAs,P),ass(A1,PAs,P)) :-
1657 write_all([' ',Q,' has already been assumed
. It succeeds
.']),
1662 write_all([' ',Q,' is consistently assumed
.']),
1665 write_all([' ',Q,' is inconsistent with other assumables
.']),
1669 whynotb(Q,_,up,ass(A0,PAs0,P0),ass(A0,PAs1,P1)) :-
1671 % (ground(Q) -> true
1672 % ; write_all([' Error
: assumable
',Q,' needs to be ground
when called
.'])),
1675 insertUpdateProbs(PAs0,P0,Q,P,PAs1,P1),
1676 prob_threshold(Bound),
1679 retract(pruned_prob(PP)),
1681 asserta(pruned_prob(PP1)),
1682 write_all([' ',Q,' fails as the probability
(',P1,') is too small
'])
1684 write_all([' ',Q,' suceeds as it can be assumed
'])
1687 write_all([' ',Q,' fails as it is inconsistent with other assumpions
'])
1691 whynotb(G=V,_,up,ass(A0,PAs,P),ass(A1,PAs,P)) :-
1696 write_all([' ',G=V,' is has already been assumed
.'])
1697 ; write_all([' arbitrary
',G,' has value
',V1,', so
',G=V,' fails
.'])
1701 write_all([' ',G=V,' is consistently assumed
.']),
1706 whynotb(Q,0,up,Ass0,Ass0) :- !,
1707 write_all([' ',Q,' fails because of the depth
-bound
.']).
1709 % whynotb(Q,DB,up,Ass0,Ass0) :-
1712 % write_all([' ',Q,' is a fact
. It doesn
''t fail
.']).
1714 whynotb(Q,DB,Rep,Ass0,Ass1) :-
1717 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
1718 whynotb(Q,_,up,Ass0,Ass0) :-
1719 write_all([' There is
no applicable rule
for ',Q,'.']).
1721 whynotrule(Q,B,DB,Rep,Ass0,Ass1) :-
1724 write_all([' ',Q,'.']);
1725 write_all([' ',Q,' <- ',B,'.'])
1727 writel([' Trace this rule?
[yes
,no,up
,help
]: ']),
1728 flush_and_read(Comm),
1729 whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1).
1731 whynotruleinterpret(yes,Q,B,DB,Rep,Ass0,Ass1) :- !,
1733 whynotb(B,DB1,Rep1,Ass0,Ass1),
1735 -> whynotrule(Q,B,DB,Rep,Ass0,Ass1)
1737 whynotruleinterpret(no,_,_,_,_,_,_) :- !,
1739 whynotruleinterpret(up,_,_,_,up,Ass0,Ass0) :- !.
1740 whynotruleinterpret(end_of_file,_,_,_,prompt,_,_) :- !,
1742 whynotruleinterpret(ok,_,_,_,prompt,_,_) :- !.
1743 whynotruleinterpret(help,Q,B,DB,Rep,Ass0,Ass1) :- !,
1745 ' Do you want to examine why this rule failed?
',nl,
1746 ' yes
. look at this rule
',nl,
1747 ' no. try another rule
',nl,
1748 ' up
. go back to the rule this rule was called from
',nl,
1749 ' ok
. go to top
-level prompt
']),
1750 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
1751 whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1) :-
1752 write_all([' Unknown command
: ',Comm,'. Type
"help." for help
.']),
1753 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
1756 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1,Ass2) :-
1757 write_all([' The proof
for ',A,' succeeded
.']),
1759 write_all([' assuming
',Ass1])
1762 writel([' Is this the appropriate answer?
[yes
,no,debug
,help
]: ']),
1763 flush_and_read(Comm),
1764 why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass1,Ass2).
1766 why_not_conj_interpret(debug,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
1769 -> report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1)
1771 why_not_conj_interpret(yes,_,_,B,DB,Rep,Ass0,Ass1) :- !,
1772 whynotb(B,DB,Rep,Ass0,Ass1).
1773 why_not_conj_interpret(no,_,_,_,_,_,_,_) :- !,
1774 fail. % find another proof for A
1776 why_not_conj_interpret(end_of_file,_,_,_,_,prompt,_,_) :- !,
1778 why_not_conj_interpret(ok,_,_,_,_,prompt,_,_) :- !,
1780 why_not_conj_interpret(help,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
1782 ' yes
. this instance should have made the body succeed
.',nl,
1783 ' no. this instance should lead to a failure of the body
.',nl,
1784 ' debug
. this instance is false
, debug it
.',nl,
1785 ' ok
. I
''ve had enough
. Go to the prompt
.',nl,
1786 ' help
. print this message
.']),
1787 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1788 why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1) :-
1789 write_all([' Unknown command
: ',Comm,'. Type
"help." for help
.']),
1790 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1792 whynotb_expls(A,ETs,Rep) :-
1793 write_all([' ',~A,' succeeds
, as
',A,' has the explanations
: ']),
1794 print_explanations(ETs,0),
1795 writel([' [up
,top
,retry
,prompt
,how i
,help
,whynot
]: ']),
1796 flush_and_read(Comm),
1797 interpret_naf_how(Comm,ETs,Rep0),
1799 whynotb_expls(A,ETs,Rep)
1803 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1805 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1807 flush_and_read(T) :-
1809 (read(T) -> true ; flush_and_read(T)). % reads until no error.
1812 current_input(OldFile),
1813 open(File,read,Input),
1818 write_all(['AILog theory
',File,' loaded
.']).
1821 file_or_command(C,file),
1822 flush_and_read(T2),!,
1825 read_all(end_of_file) :- !.
1826 read_all((H :- B)) :- !,
1827 write_all(['Error
: Illegal Implication
: ',H,' :- ',B,'. Use
<- or prload
.']).
1830 flush_and_read(T2),!,
1834 prolog_load(File) :-
1835 current_input(OldFile),
1836 open(File,read,Input),
1841 write_all(['AILog theory
',File,' consulted
.']).
1845 file_or_command(T,file),
1848 prread_all(end_of_file) :- !.
1850 prillegal(T,Mesg),!,
1857 % prillegal(R,Mesg) is true if R is illegal Prolog rule.
1858 % Mesg is the corresponding error message.
1859 prillegal((H <- B),['Error
. Illegal Implication
: ',H,' <- ',B,
1860 '. Use
:- in prload
.']) :- !.
1861 prillegal((:- B),['Error
. Commands
not allowed
. ":- ',B,'."']) :- !.
1862 prillegal((_ :- B),Mesg) :- !,
1864 prillbody((A,_),Mesg) :-
1866 prillbody((_,B),Mesg) :-
1868 prillbody((_;_),['Prolog rules assume disjunction
";". Define it before loading
.']) :-
1870 prillbody((A;_),Mesg) :-
1872 prillbody((_;B),Mesg) :-
1874 prillbody((_&_),['Error
. Illegal conjunction
in Prolog rules
: &']):- !.
1875 prillbody(!,['Error
. Cut
(!) not allowed
.']) :- !.
1876 prillbody((_ -> _ ; _),['Error
. "->" is
not implemented
.']) :- !.
1877 prillbody((_ -> _ ),['Error
. "->" is
not implemented
.']) :- !.
1879 % prtell(Cl) tells the prolog clause Cl
1880 prtell((H :- B)) :- !,
1884 assertz((H <- true)).
1886 % convert_body(PB,CB) converts Prolog body PB to ailog body CB
1887 convert_body((A,B),(A1&B1)) :- !,
1890 convert_body((A;B),(A1;B1)) :- !,
1893 convert_body((\+ A),(~ A1)) :- !,
1898 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1900 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1905 'AILog Version
',V,'. Copyright
',Y,', David Poole
.',nl,
1906 'AILog comes with absolutely
no warranty
.',nl,
1907 'All inputs end with a period
. Type
"help." for help
.']),
1911 catch(go,Exc,handle_exception(Exc)).
1914 writel(['ailog
: ']),
1917 write_all(['Returning to Prolog
. Type
"start." to start ailog
.'])
1918 ; T == end_of_file ->
1920 write_all(['Returning to Prolog
. Type
"start." to start ailog
.'])
1925 handle_exception(prompt) :- !, start1.
1926 handle_exception(quit) :- halt.
1927 handle_exception(Exc) :-
1928 write_all(['Error
: ',Exc]),
1931 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1933 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1935 % check searches through the knowledge base looking for a rule
1936 % containing an atom in the body which doesn't have a corresponding
1937 % definition
(i
.e
., a clause with it at the head
).
1940 body_elt_undefined
(B
,H
,B
).
1946 write_all
([H
,' should not be defined in a rule and as a probability.']),
1949 body_elt_undefined
(true
,_
,_
) :- !,fail
.
1950 body_elt_undefined
((A
&_
),H
,B
) :-
1951 body_elt_undefined
(A
,H
,B
).
1952 body_elt_undefined
((_
&A
),H
,B
) :- !,
1953 body_elt_undefined
(A
,H
,B
).
1954 body_elt_undefined
((~ A
),H
,B
) :- !,
1955 body_elt_undefined
(A
,H
,B
).
1956 body_elt_undefined
((A
;_
),H
,B
) :-
1957 body_elt_undefined
(A
,H
,B
).
1958 body_elt_undefined
((_
;A
),H
,B
) :- !,
1959 body_elt_undefined
(A
,H
,B
).
1960 body_elt_undefined
(call
(A
),H
,B
) :- !,
1961 body_elt_undefined
(A
,H
,B
).
1962 body_elt_undefined
(_ \
= _
,_
,_
) :- !,fail
.
1963 body_elt_undefined
(_
#= _,_,_) :- !,fail.
1964 body_elt_undefined
(A
,_
,_
) :-
1966 body_elt_undefined
(A
,_
,_
) :-
1968 body_elt_undefined
(A
,_
,_
) :-
1969 choice
(A
,_
,_
),!,fail
.
1970 body_elt_undefined
(X
=V
,_
,_
) :-
1972 body_elt_undefined
(A
,_
,_
) :-
1973 builtin
(A
,_
),!,fail
.
1974 body_elt_undefined
(A
,_
,_
) :-
1976 body_elt_undefined
(A
,H
,B
) :-
1977 write_all
(['Warning: no clauses for ',A
,' in rule ',(H
<- B
),'.']),!,fail
.
1979 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1981 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1983 % uncomment the
next line to make runtime checking the
default
1986 % stats_command
(Cmd
) means
"stats Cmd" was
given as a command
.
1987 stats_command
(runtime
) :- !,
1988 retractall
(checking_runtime
),
1989 asserta
(checking_runtime
),
1990 write_all
(['Runtime report turned on. Type "stats none." to turn it off.']).
1991 stats_command
(none
) :- !,
1992 retractall
(checking_runtime
).
1994 write_all
(['The stats commands implemented are:']),
1995 write_all
([' stats runtime. turn on report of runtime.']),
1996 write_all
([' stats none. turn off report of runtime.']).
1998 % reset_runtime means that we are storing the current valuse of
1999 % runtime
. This means that we are leaving out much of the ailog
2000 % overhead from the calcluation
.
2004 retractall
(lastruntime
(_
)),
2006 asserta
(lastruntime
(T
)),!.
2009 write_all
([' Problem with runtime checking.'])
2015 get_runtime
(T1
,Units
),
2017 write_all
([' Runtime since last report: ',RT
,' ',Units
,'.']),!.
2020 write_all
([' Problem with runtime reporting.'])
2023 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2025 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2026 % A nogood is a set of assumables that is inconsistent
2027 construct_nogoods
(DB
) :-
2029 retractall
(failed
(_
)),
2030 assert
(failed
(naturally
)),
2032 solve
(false
,DB
,PfTree
,[wrule
(yes
,true
,false
,true
)],ass
([],[],1),ass
(Ass
,_
,_
)),
2033 assert
(nogood
(Ass
,PfTree
)),
2034 assert_each_nogood
(Ass
,[]),
2036 construct_nogoods
(DB
) :-
2038 -> write_all
(['Nogoods recorded. Type "nogoods." to see them.'])
2039 ; write_all
(['Nogoods recorded, but depth-bound ',DB
,' reached. Type "nogoods." to see them.']).
2041 assert_each_nogood
([],[]).
2042 assert_each_nogood
([H
|NotDone
],Done
) :-
2043 append
(NotDone
,Done
,Rest
),
2044 assert
(anogood
(H
,Rest
)),
2045 assert_each_nogood
(NotDone
,[H
|Done
]).
2049 write_all
(['Nogood: ',NG
,'.']), fail
.
2059 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2061 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2063 % write_all
(L
) writes
each element of list L
, ends with new line
2065 \
+ \
+ (mynumbervars
(L
,0,_
),writel0
(L
)),
2067 % writel
(L
) writes
each element of list L
2069 \
+ \
+ (mynumbervars
(L
,0,_
),writel0
(L
)).
2071 % writel0
(L
) writes
each element of list L
2073 writel0
([nl
|T
]) :- !,
2080 % writeAllDelim
(L
,D
) writes the elements of L using delimiter D
2081 writeAllDelim
(L
,D
) :-
2082 \
+ \
+ (mynumbervars
(L
,0,_
),writeAllDelim0
(L
,D
)).
2084 writeAllDelim0
([],_
) :-!.
2085 writeAllDelim0
([E
],_
) :- !, mywrite
(E
).
2086 writeAllDelim0
([H
|T
],nl
) :- !, mywrite
(H
),nl
,writeAllDelim0
(T
,nl
).
2087 writeAllDelim0
([H
|T
],D
) :- mywrite
(H
),mywrite
(D
),writeAllDelim0
(T
,D
).
2089 % mywrite
(T
) writes term T
2091 write_term
(T
,[numbervars
(true
),portray
(true
)]).
2093 portray
(A
&B
) :- mywrite
(A
),mywrite
(' & '),mywrite
(B
).
2095 % insert_into_sorted_list
(E
,L
,R
) inserts E into sorted list L producing R
2096 insert_into_sorted_list
(A
,[],[A
]).
2097 insert_into_sorted_list
(A
,[A1
|R
],[A
|R
]) :- A
== A1
,!.
2098 insert_into_sorted_list
(A
,[A1
|R
],[A
,A1
|R
]) :- A @
< A1
, !.
2099 insert_into_sorted_list
(A
,[B
|R
],[B
|R1
]) :-
2100 insert_into_sorted_list
(A
,R
,R1
).
2102 % insertUpdateProbs
(E
,L
) inserts E into sorted list L
2103 insertUpdateProbs
(A
,[],[A
]).
2104 insertUpdateProbs
(A
,[A1
|R
],[A
|R
]) :- A
== A1
,!.
2105 insertUpdateProbs
(A
,[A1
|R
],[A
,A1
|R
]) :- A @
< A1
, !.
2106 insertUpdateProbs
(A
,[B
|R
],[B
|R1
]) :-
2107 insertUpdateProbs
(A
,R
,R1
).
2109 % consistent
(L1
,L2
) is true
if L1
& L2 are sorted lists with
no
2110 % elements
in common
.
2111 consistent
([],_
) :- !.
2112 consistent
(_
,[]) :- !.
2113 consistent
([A1
|R1
],[A2
|R2
]) :-
2115 consistent
(R1
,[A2
|R2
]).
2116 consistent
([A1
|R1
],[A2
|R2
]) :-
2118 consistent
([A1
|R1
],R2
).
2120 % remove
(E
,L
,L1
) removes E from list L producing L1
2122 remove
(E
,[A
|L
],[A
|R
]) :-
2126 % subset_sorted
(L1
,L2
) is true
if list L1 is a subset of L2
2127 % all lists are assumed to be ground
and sorted
.
2128 subset_sorted
([],_
) :- !.
2129 subset_sorted
([A
|L1
],[A
|L2
]) :- !,
2130 subset_sorted
(L1
,L2
).
2131 subset_sorted
([A1
|L1
],[A2
|L2
]) :-
2133 subset_sorted
([A1
|L1
],L2
).
2135 % setDiff
(S1
,S2
,S3
) S3
= S1
-S2
. All lists are sorted
.
2137 setDiff
([],_
,[]) :- !.
2138 setDiff
(S
,[],S
) :- !.
2139 setDiff
([A
|L1
],[A
|L2
],R
) :- !,
2141 setDiff
([A1
|L1
],[A2
|L2
],[A1
|R
]) :-
2143 setDiff
(L1
,[A2
|L2
],R
).
2144 setDiff
(L1
,[_
|L2
],R
) :-
2147 % mywhen
(C
,G
) replaces
"when". It does
not delay
, but instead gives an
2148 % error
. This is now redundant as SWI has
"when".
2152 write_all
(['Warning: ',C
,' failing. Delaying not implemented.']),
2155 % ith
(L
,E
,I
,I0
) is true
if E is the Ith element of list L
, starting to
2159 ith
([H
|_
],H
,I
,I
) :- !.
2160 ith
([_
|T
],E
,I
,I0
) :-
2167 idmember
(A
,[A1
|_
]) :- A
==A1
,!.
2168 idmember
(A
,[_
|L
]) :- idmember
(A
,L
).
2170 mynumbervars
(Term
, From
, To
) :-
2171 numbervars
(Term
, From
, To
, [attvar
(bind)]).
2175 issorted
([E1
,E2
|R
]) :-
2182 write_all
(['Warning: not sorted: ',L
]).
2184 % Run
"start" at initialization
2185 :- initialization
(start
).
repositories / ker2014-2.git / blob