--- /dev/null
+% -*- Mode: Prolog -*-\r
+% ailog2.pl logic engine for Artificial Intelligence http://artint.info\r
+% Copyright (C) 1997-2012, David Poole.\r
+% This is subject to the GNU Public License (GPL). See user manual for details.\r
+% Designed for standard Prolog, but only tested on SWI Prolog.\r
+% It is written in one file to make it easy to use:\r
+% Get swi-prolog, double click on this file and it should start!\r
+\r
+ailog_version('2.3.6.2',2013).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+% SYSTEM DEPENDENT CODE %\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+%% the keys to stastics don't seem to be standard. This should cover the cases:\r
+%% get_runtime(T,Units) gets accumulated runtime from the system\r
+get_runtime(T,U) :- catch((statistics(cputime,T),U=secs),_,\r
+ (statistics(runtime,[T,_]),U=ms)). % Sicstus/Quintus Prolog\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+% OPERATOR DEFINITIONS %\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% <- is the "if"\r
+:- op(1150, xfx, <- ).\r
+% <= is the base-level "if" (it is not used here, but can be used in\r
+% programs). \r
+:- op(1120, xfx, <= ).\r
+% "&" is the conjunction.\r
+:- op(950,xfy, &).\r
+% "~" is the negation\r
+:- op(900,fy,~).\r
+% "\=" is inequality\r
+:- op(700,xfx,\=).\r
+% "#=" is can't be equal\r
+:- op(700,xfx,#=).\r
+% ":" is used for probability declarations.\r
+:- op(800,xfx,:).\r
+\r
+:- op(1170, fx, tell).\r
+:- op(1170, fx, ask).\r
+:- op(1170, fx, whynot).\r
+:- op(1170, fx, how).\r
+:- op(1170, fx, how).\r
+:- op(1170, fx, help).\r
+:- op(1170,fx,load).\r
+:- op(1170,fx,prload).\r
+:- op(1170,fx,cd).\r
+:- op(1170,fx,bound).\r
+:- op(1170,fx,stats).\r
+:- op(1170,fx,listing).\r
+:- op(1170,fx,clear).\r
+:- op(1170,fx,askable).\r
+:- op(1170,fx,assumable).\r
+:- op(1170,fx,prob).\r
+:- op(1170,fx,observe).\r
+:- op(1170,fx,unobserve).\r
+:- op(1170,fx,predict).\r
+:- op(1170,fx,deterministic).\r
+:- op(1170,fx,prob_threshold).\r
+:- op(1170,fx,arbitrary).\r
+:- op(1170,fx,allow).\r
+\r
+:- dynamic (<-)/2.\r
+:- dynamic failed/1.\r
+:- dynamic depth_bound/1.\r
+:- dynamic askabl/1.\r
+:- dynamic assumabl/1.\r
+:- dynamic choice/3.\r
+:- dynamic alt/1.\r
+:- dynamic asked/2.\r
+:- dynamic debugging_failure/0.\r
+:- dynamic answer_found/0.\r
+:- dynamic checking_runtime/0.\r
+:- dynamic lastruntime/1.\r
+:- dynamic deter/1.\r
+:- dynamic explanations/4.\r
+:- dynamic nogood/2.\r
+:- dynamic anogood/2.\r
+:- dynamic (prob_threshold)/1.\r
+:- dynamic pruned_prob/1.\r
+:- dynamic arbit/2.\r
+:- dynamic builtin/2.\r
+\r
+depth_bound(30).\r
+prob_threshold(0.000001).\r
+pruned_prob(0.0).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% AILog Help\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+help_message(['\r
+AILog Version ',V,' Help','\r
+\r
+A clause is of the form','\r
+ Head <- Body','\r
+ Head','\r
+Head is an atom.','\r
+Body is an expression made up of','\r
+ Atom','\r
+ ~ B1 negation as finite failure','\r
+ B1 & B2 conjunction B1 and B2','\r
+where B1 and B2 are expressions.','\r
+\r
+***** Basic commands:','\r
+\r
+tell CLAUSE. add the clause to the knowledge base','\r
+askable Atom. makes Atom askable.','\r
+\r
+ask QUERY. ask if expression QUERY is a consequence of the KB','\r
+whynot QUERY. find out why an answer to QUERY was not returned.','\r
+\r
+allow G. allow goal G to use the Prolog definition.','\r
+bound N. set search depth-bound to N (default=30)','\r
+listing. list all clauses in the knowledge base.','\r
+listing H. list clauses in the knowledge base with head H.','\r
+askables. list all askables.','\r
+clear. clear the knowledge base','\r
+clear asked. clear all user responses','\r
+clear H. clear clauses with head H from knowledge base','\r
+check. check the knowledge base for undefined predicates','\r
+help. print this help message','\r
+help prob. prints help on probabilistic reasoning','\r
+help abduction. prints help on abductive reasoning','\r
+stats runtime. turn on runtime statistics','\r
+quit. quit ailog','\r
+prolog. exit to Prolog. Type "start." to start ailog again.','\r
+\r
+***** Input/Output','\r
+\r
+load ''Filename''. load the clauses in file Filename','\r
+prload ''Filename''. load the clauses in Filename, using Prolog''s syntax.','\r
+cd ''directory''. changes directory (folder) for loads']) :-\r
+ ailog_version(V,_).\r
+\r
+help_message(prob,[\r
+'AILog Version ',V,' Probabilistic Reasoning Help','\r
+\r
+This help is for probabilistic reasoning in Ailog. This is not useful\r
+if you are a beginner interested in deductive reasoning.','\r
+\r
+AILog implements a version of the independent choice logic that allows\r
+for probabilities on atoms. These atoms should not be the head of clauses.','\r
+\r
+prob a:p. makes atom a probabilistic with probability p.','\r
+prob a1:p1,a2:p2,...,ak:pk. makes atoms ai probabilistic with probability pi.','\r
+ a''s are exclusive and covering; the p''s must sum to 1.','\r
+\r
+probs. list all prob assertions.','\r
+\r
+observe QUERY. observe that QUERY is true','\r
+predict QUERY. ask the posterior probability that QUERY is true','\r
+observations. list all observations made','\r
+unobserve. undo whylast observation','\r
+unobserve all. undo all observations','\r
+explanations. describe the explanations of the observations','\r
+worlds. describe the worlds of the observations','\r
+\r
+prob_threshold V. set the probability threshold to V in range [0,1]','\r
+prob_threshold. get the current probability threshold']) :-\r
+ ailog_version(V,_).\r
+\r
+help_message(abduction,[\r
+'AILog Version ',V,' Abductive Reasoning Help','\r
+\r
+This help is for abductive reasoning in AILog. This is not useful if\r
+you are a beginner interested in deductive reasoning.','\r
+\r
+Abduction allows the system to make assumptions to prove a goal, as\r
+long as the assumptions are consistent.',' The atoms that can be\r
+assumed are called assumables.',' You use "false" at the head of a\r
+clause to make constraints.',' After adding assumables or more\r
+clauses, you need to create nogoods to make sure that inconsistent\r
+sets of assumables are found.',' Abduction in AILog does not work\r
+satisfactorily with negation as failure.','\r
+\r
+assumable Atoms. makes (comma-separated) Atoms assumable.','\r
+assumables. list all assumables.','\r
+\r
+create_nogoods construct nogoods.','\r
+nogoods list nogoods.'\r
+]) :-\r
+ ailog_version(V,_).\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% AILog Commands\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+interpret(C) :-\r
+ file_or_command(C,command),!.\r
+\r
+interpret(help) :- !,\r
+ help_message(Help),\r
+ write_all(Help).\r
+interpret(help What) :-\r
+ help_message(What,Help),!,\r
+ write_all(Help).\r
+interpret(help What) :- !,\r
+ write_all(['No help on "',What,'". Type "help." for more information.']).\r
+\r
+interpret((tell _ :- _)) :- !,\r
+ write_all(['Illegal rule: ":-" is not a legal implication. Use "<-".']).\r
+interpret((tell C)) :- !,\r
+ tell_clause(C).\r
+\r
+interpret((ask Q)) :- !,\r
+ retractall(debugging_failure),\r
+ retractall(answer_found),\r
+ depth_bound(DB),\r
+ askq(Q,DB).\r
+\r
+interpret((whynot Q)) :- !,\r
+ depth_bound(DB),\r
+ (explanations(_,ETs,_,_)\r
+ ->\r
+ member(et(E,_),ETs),\r
+ whynotb(Q,DB,_,E,_)\r
+ ;\r
+ whynotb(Q,DB,_,ass([],[],1),_)\r
+ ).\r
+\r
+interpret(clear) :- !,\r
+ retractall((_ <- _)),\r
+ retractall(assumabl(_)),\r
+ retractall(alt(_)),\r
+ retractall(choice(_,_,_)), \r
+ retractall(askabl(_)),\r
+ retractall(asked(_,_)),\r
+ retractall(nogood(_,_)),\r
+ retractall(anogood(_,_)),\r
+ retractall(explanations(_,_,_,_)),\r
+ retractall(pruned_prob(_)),\r
+ retractall(arbit(_,_)),\r
+ assert(pruned_prob(0.0)).\r
+\r
+interpret((clear asked)) :- !,\r
+ retractall(asked(_,_)),\r
+ write_all(['User responses cleared.']).\r
+\r
+interpret((clear H)) :- !,\r
+ retractall((H <- _)),\r
+ retractall(assumabl(H)),\r
+ ( alt(A) , member(H:_, A)\r
+ ->\r
+ retract(alt(A)),\r
+ forall(member(G:_, A), retract(choice(G,_,_)))\r
+ ; true),\r
+ retractall(askabl(H)),\r
+ retractall(asked(H,_)),\r
+ (H=(X,V) -> retractall(arbit(X,V));true).\r
+\r
+interpret((stats Cmd)) :- !,\r
+ stats_command(Cmd).\r
+\r
+interpret((prload File)) :- !,\r
+ prolog_load(File).\r
+\r
+interpret((load File)) :- !,\r
+ ci_load(File).\r
+\r
+interpret((cd Dir)) :- !,\r
+ working_directory(_,Dir).\r
+\r
+interpret((cd)) :- !,\r
+ working_directory(_,'~').\r
+\r
+interpret((bound)) :- !,\r
+ depth_bound(N),\r
+ write_all(['Current depth bound is ',N]).\r
+\r
+interpret((bound N)) :- !,\r
+ (integer(N) ->\r
+ retract(depth_bound(_)),\r
+ asserta(depth_bound(N))\r
+ ; write_all(['Depth bound must be an integer'])).\r
+\r
+interpret(quit) :-\r
+ throw(quit).\r
+\r
+interpret(check) :- !,\r
+ check.\r
+\r
+interpret((observe G)) :- !,\r
+ observe(G).\r
+\r
+interpret((predict G)) :- !,\r
+ predict(G).\r
+\r
+interpret(askables) :- \r
+ askabl(G),\r
+ write_all(['askable ',G,'.']),\r
+ fail.\r
+interpret(askables) :- !.\r
+\r
+interpret(assumables) :- \r
+ assumabl(G),\r
+ write_all(['assumable ',G,'.']),\r
+ fail.\r
+interpret(assumables) :- !.\r
+\r
+interpret(arbitraries) :- \r
+ arbit(X,V),\r
+ write_all(['arbitrary ',X=V,'.']),\r
+ fail.\r
+interpret(arbitraries) :- !.\r
+\r
+interpret(probs) :-\r
+ alt(L),\r
+ (L=[A:P1,~A:_]\r
+ ->\r
+ write_all(['prob ',A,':',P1,'.'])\r
+ ;\r
+ write('prob '),\r
+ writeAllDelim(L,', '),\r
+ write('.'),\r
+ nl\r
+ ),\r
+ fail.\r
+interpret(probs) :- !.\r
+\r
+interpret((listing)) :- !,\r
+ interpret((listing _)),\r
+ interpret(askables),\r
+ interpret(assumables),\r
+ interpret(probs),\r
+ interpret(arbitraries).\r
+\r
+interpret((listing H)) :-\r
+ (H <- B),\r
+ (B == true \r
+ -> write_all([H,'.'])\r
+ ; write_all([H,' <- ',B,'.'])\r
+ ),\r
+ fail.\r
+interpret((listing _)) :- !.\r
+\r
+interpret(unobserve all) :- !,\r
+ retractall(explanations(_,_,_,_)),\r
+ retractall(pruned_prob(_)),\r
+ assert(pruned_prob(0.0)).\r
+\r
+interpret(unobserve) :- !,\r
+ (retract(explanations(_,_,_,_))\r
+ ->\r
+ (\r
+ explanations(_,_,_,Err)\r
+ ->\r
+ retractall(pruned_prob(_)),\r
+ assert(pruned_prob(Err))\r
+ ;\r
+ retractall(pruned_prob(_)),\r
+ assert(pruned_prob(0.0))\r
+ \r
+ )\r
+ ;\r
+ write_all(['No observations to undo.'])\r
+ ).\r
+\r
+interpret(observations) :- !,\r
+ (explanations(Obs,_,_,_) ->\r
+ print_observations(Obs,_)\r
+ ; write_all(['There are no observations.'])).\r
+\r
+interpret(explanations) :- !,\r
+ (explanations(_,ETs,_,_) ->\r
+ print_explanations(ETs,0)\r
+ ; write_all(['There are no observations.'])).\r
+\r
+interpret(worlds) :- !,\r
+ (explanations(Obs,Expls,Pr,Err) ->\r
+ extract_expls(Expls,Sexpls),\r
+ make_disjoint(Sexpls,Worlds),\r
+ print_worlds(Worlds,0),\r
+ (Err=:=0.0\r
+ ->\r
+ write_all(['P(',Obs,') = ',Pr])\r
+ ;\r
+ Max is Pr+Err,\r
+ write_all(['P(',Obs,') = [',Pr,',',Max,']'])\r
+ )\r
+ ; write_all(['There are no observations.'])).\r
+\r
+interpret(prob_threshold V) :-\r
+ (number(V), V>=0.0, V=<1.0)\r
+ ->\r
+ retract(prob_threshold(_)),\r
+ assert(prob_threshold(V))\r
+ ;\r
+ write_all(['Argument to prob_threshold must be in range [0,1].']).\r
+interpret(prob_threshold) :-\r
+ prob_threshold(V),\r
+ write_all(['Probability threshold is ',V]).\r
+\r
+\r
+interpret(nogoods) :- !,\r
+ list_nogoods.\r
+ \r
+interpret((A <- B)) :- !,\r
+ write_all(['Illegal command, ',(A <- B),'. You have to "tell" a clause.']).\r
+\r
+interpret(C) :-\r
+ write_all(['Unknown Command, ',C,'. Type "help." for help.']).\r
+\r
+% listifyProbs(St,L0,L1,S0,S1)\r
+% St is a probability structure \r
+% L1-L0 is thhe list corresponding to the structure\r
+% S1-S0 is the sum of the probabilities\r
+listifyProbs((X,Y),L0,L2,S0,S2) :- !,\r
+ listifyProbs(X,L0,L1,S0,S1),\r
+ listifyProbs(Y,L1,L2,S1,S2).\r
+listifyProbs((A:P),L0,[A:P|L0],S0,S1) :-\r
+% atomic(A), % we want it to mean its a ailog atom\r
+% number(P),\r
+ P >= 0,\r
+ S1 is S0+P.\r
+\r
+% file_or_command(C,W) C is a command that can be in a file or on the\r
+% command line, W is either command or file \r
+file_or_command((askable G),_) :- !,\r
+ assertz(askabl(G)).\r
+\r
+file_or_command((assumable G),_) :- !,\r
+ make_assumable(G).\r
+\r
+file_or_command((allow G),_) :- !,\r
+ assertz(builtin(G,true)).\r
+\r
+\r
+file_or_command((prob A:P),W) :- !,\r
+ (number(P), P>=0, P=<1 ->\r
+ P1 is 1-P,\r
+ assertz(alt([A:P,~A:P1])),\r
+ assertz(choice(A,P,[~A])),\r
+ assertz(choice(~A,P1,[A]))\r
+ ;\r
+ legal_arithmetic_expression(P) ->\r
+ assertz(alt([A:P,~A:(1-P)])),\r
+ assertz(choice(A,P,[~A])),\r
+ assertz(choice(~A,(1-P),[A]))\r
+\r
+ ;\r
+ (W=file \r
+ ->\r
+ write_all(['Error: ',(prob A:P)])\r
+ ; true),\r
+ write_all(['Probability must be a number or expression in range [0,1]'])\r
+ ).\r
+\r
+file_or_command((prob APs),W) :- !, \r
+ ( (listifyProbs(APs,[],L,0,Sum) )%, Sum > 0.9999999999999, Sum< 1.0000000000001)\r
+ ->\r
+ normalise(L,Sum*1.0,LN),\r
+ assertz(alt(LN)),\r
+ make_choices(LN)\r
+ ;\r
+ (W=file \r
+ ->\r
+ write_all(['Error: ',(prob APs)])\r
+ ; true),\r
+ write_all(['Error: command should be: prob a1:p1,a2:p2,...,ak:pk.']),\r
+ write_all([' the pi''s must be nonnegative and sum to 1.0'])\r
+ ).\r
+\r
+file_or_command((arbitrary A),W) :- !,\r
+ A=(X=V)\r
+ ->\r
+ assertz(arbit(X,V))\r
+ ;\r
+ (W=file \r
+ ->\r
+ write_all(['Error: ',(arbitrary A)])\r
+ ; true),\r
+ write_all(['Error: command should be: arbitrary X=V.']).\r
+ \r
+ \r
+file_or_command((deterministic G),_) :- !,\r
+ assertz(deter(G)).\r
+\r
+file_or_command(create_nogoods,_) :- !,\r
+ depth_bound(DB),\r
+ construct_nogoods(DB).\r
+\r
+\r
+legal_arithmetic_expression(N) :- var(N),!.\r
+legal_arithmetic_expression(N) :- number(N),!.\r
+legal_arithmetic_expression(E1+E2) :- !,\r
+ legal_arithmetic_expression(E1),\r
+ legal_arithmetic_expression(E2).\r
+legal_arithmetic_expression(E1-E2) :- !,\r
+ legal_arithmetic_expression(E1),\r
+ legal_arithmetic_expression(E2).\r
+legal_arithmetic_expression(E1*E2) :- !,\r
+ legal_arithmetic_expression(E1),\r
+ legal_arithmetic_expression(E2).\r
+legal_arithmetic_expression(E1/E2) :- !,\r
+ legal_arithmetic_expression(E1),\r
+ legal_arithmetic_expression(E2).\r
+\r
+% make_assumable makes an atom or a comma-separated atoms assumable.\r
+make_assumable((A,B)) :- !,\r
+ make_assumable(A),\r
+ make_assumable(B).\r
+\r
+make_assumable(G) :-\r
+ assertz(assumabl(G)).\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% ASKING\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+askq(Q,_) :-\r
+ illegal_body(Q,Why),!,\r
+ write_all(['Illegal query: '|Why]).\r
+askq(Q,DB) :-\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ reset_runtime,\r
+ solve(Q,DB,Res,[wrule(yes,true,Q,true)],ass([],[],1),Ass),\r
+ (answer_found -> true ; assert(answer_found)),\r
+ mynumbervars((Q,Res,Ass),0,_),\r
+ report(Q,Res,Ass).\r
+askq(Q,_) :- \r
+ failed(naturally),!,\r
+ (answer_found\r
+ -> write_all(['No more answers.'])\r
+ ; write_all(['No. ',Q,' doesn''t follow from the knowledge base.'])),\r
+ report_runtime.\r
+askq(Q,DB) :- !,\r
+ ask_failing(Q,DB).\r
+\r
+ask_failing(Q,DB) :-\r
+ write_all(['Query failed due to depth-bound ',DB,'.']),\r
+ report_runtime,\r
+ writel([' [New-depth-bound,where,ok,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_failing_question(Comm,Q,DB).\r
+\r
+% interpret_failing_question(Comm,Q,DB).\r
+interpret_failing_question(help,Q,DB) :- !,\r
+ write_all([\r
+ ' Give one of the following commands:',nl,\r
+ ' an integer > ',DB,' to use this depth bound.',nl,\r
+ ' (use "bound N." to set it permanently).',nl,\r
+ ' where. to explore the proof tree where the depth-bound was reached.',nl,\r
+ ' ok. to return to the ailog prompt.',nl,\r
+ ' help. to print this message.']),\r
+ ask_failing(Q,DB).\r
+interpret_failing_question(end_of_file,_,_) :- !.\r
+interpret_failing_question(ok,_,_) :- !.\r
+interpret_failing_question(where,Q,DB) :-\r
+ assert(debugging_failure),\r
+ askq(Q,DB).\r
+interpret_failing_question(Comm,Q,_) :-\r
+ integer(Comm),!,\r
+ askq(Q,Comm).\r
+interpret_failing_question(Comm,Q,DB) :-\r
+ write_all([' Unknown command, ',Comm,' type "help." for help.']),\r
+ ask_failing(Q,DB).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% TELLING\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+tell_clause((~ H <- B)) :- !,\r
+ write_all(['Illegal rule: ~',H,' <- ',B,'.',nl,\r
+ 'You cannot have negation in the head of a clause.']).\r
+tell_clause((H1 & H2 <- B)) :- !,\r
+ write_all(['Illegal rule: ',H1 & H2,' <- ',B,'.',nl,\r
+ 'You cannot have a conjunction in the head of a clause.']).\r
+tell_clause((H1 , H2 <- B)) :- !,\r
+ write_all(['Illegal rule: ',H1 ,',', H2,' <- ',B,'.',nl,\r
+ 'You cannot have a "," in the head of a clause.']).\r
+tell_clause((H <- B)) :-\r
+ !,\r
+ ( builtin(H,_) ->\r
+ write_all([H,' is built-in. It cannot be redefined.'])\r
+ ; illegal_body(B,Why) ->\r
+ write_all(['Illegal rule: ',H,'<-',B,'. '|Why])\r
+ ; assertz((H <- B))).\r
+tell_clause((H :- B)) :-\r
+ !,\r
+ write_all(['Illegal rule: ',H,':-',B,'. ":-" is not a legal implication. Use "<-".']).\r
+tell_clause((A, B)) :-\r
+ !,\r
+ write_all(['Error: ',(A,B),' is not a valid clause.']).\r
+tell_clause((A & B)) :-\r
+ !,\r
+ write_all(['Error: ',(A&B),' is not a valid clause.']).\r
+tell_clause((~A)) :-\r
+ !,\r
+ write_all(['Error: ',~A,' is not a valid clause.']).\r
+tell_clause(H) :-\r
+ builtin(H,_),!,\r
+ write_all([H,' is built-in. It cannot be redefined.']).\r
+tell_clause(H) :-\r
+ !,\r
+ assertz((H <- true)).\r
+\r
+illegal_body(X,['Variables cannot be atoms. Use call(',X,').']) :- var(X).\r
+illegal_body((_,_),[' "," is not a legal conjunction. Use "&".']).\r
+illegal_body((\+ _),[' "\\+" is not a legal negation. Use "~".']).\r
+illegal_body(!,[' "!" is not supported.']).\r
+illegal_body([_|_],[' Lists cannot be atoms.']).\r
+\r
+illegal_body((A&_),Why) :-\r
+ illegal_body(A,Why).\r
+illegal_body((_&A),Why) :-\r
+ illegal_body(A,Why).\r
+illegal_body((A;_),Why) :-\r
+ illegal_body(A,Why).\r
+illegal_body((_;A),Why) :-\r
+ illegal_body(A,Why).\r
+illegal_body((~A),Why) :-\r
+ illegal_body(A,Why).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% META-INTERPRETER\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% solve(Goal,DepthBnd,PfTree,WhyTree,Ass0,Ass1) \r
+% Goal is the goal to be proved\r
+% DepthBnd is the depth bound\r
+% PfTree is the proof tree returned\r
+% Whytree is a list of wrule(Head,LeftTree,Current,RightBody)\r
+% Ass0 is the assumables coming in. \r
+% This is structure of the form ass(As,PAs,P)\r
+% Ass1 is the assumables coming out\r
+solve(true,_,true,_,Ass,Ass) :- !.\r
+solve((A&B),N,(AT&BT),[wrule(H,LT,_,RB)|WT],A0,A2) :- !,\r
+ solve(A,N,AT,[wrule(H,LT,A,(B&RB))|WT],A0,A1),\r
+ solve(B,N,BT,[wrule(H,(LT&AT),B,RB)|WT],A1,A2).\r
+\r
+% The following is tempting, but doesn't work if A makes assumptions...\r
+% solve((A -> B ; C),N,(AT -> BT;CT),[wrule(H,LT,_,RB)|WT],A0,A2) :-\r
+% solve(A,N,AT,[wrule(H,LT,A,(B&RB))|WT],A0,A1) % why rules is wrong\r
+% ->\r
+% solve(B,N,BT,[wrule(H,(LT&AT),B,RB)|WT],A1,A2)\r
+% ;\r
+% solve(C,N,CT,[wrule(H,LT,C,RB)|WT],A0,A2).\r
+ \r
+solve(A \= B,_,if(A \= B,builtin),_,A0,A0) :- !,\r
+ dif(A,B).\r
+solve(A #= B,_,if(A #= B,builtin),_,A0,A0) :- !,\r
+ \+(A=B).\r
+solve(call(G),_,_,WT,A0,A0) :- \r
+ var(G),!,\r
+ debug_error([' Error: argument to call must be bound when evaluated.'],\r
+ WT).\r
+solve(call(G),N,T,WT,A0,A1) :- !,\r
+ solve(G,N,T,WT,A0,A1).\r
+solve((~ G),N,if(~G,T),WT,A0,A1) :- !,\r
+ (ground(G) ->\r
+ failtoprove(G,N,T,WT,A0,A1)\r
+ ;\r
+ debug_error([' Error: ',~G,' needs to be ground when called.'],\r
+ WT)).\r
+\r
+\r
+solve(G,_,if(G,assumed),_,ass(A0,PAs,P),ass(A0,PAs,P)) :-\r
+ assumabl(G),\r
+% (ground(G) -> true\r
+% ; debug_error([' Error: assumable ',G,' needs to be ground when called.'],\r
+% WT)),\r
+ idmember(G,A0),!.\r
+solve(G,_,if(G,assumed),_,ass(A0,PAs,P),ass(A1,PAs,P)) :-\r
+ assumabl(G),\r
+% (ground(G) -> true\r
+% ; debug_error([' Error: assumable ',G,' needs to be ground when called.'],\r
+% WT)),\r
+% \+ idmember(G,A0),\r
+ good(G,A0),\r
+ insert_into_sorted_list(G,A0,A1).\r
+solve(G,_,if(G,assumed),_,ass(A0,PAs0,P0),ass(A0,PAs1,P1)) :-\r
+ choice(G,P,A),\r
+% (ground(G) -> true\r
+% ; debug_error([' Error: assumable ',G,' needs to be ground when called.'],\r
+% WT)),\r
+ consistent(PAs0,A),\r
+ insertUpdateProbs(PAs0,P0,G,P,PAs1,P1),\r
+ prob_threshold(Bound),\r
+ ((P1 < Bound)\r
+ ->\r
+ retract(pruned_prob(PP)),\r
+ PP1 is PP+P1,\r
+ asserta(pruned_prob(PP1)),\r
+ fail\r
+ ;\r
+ true\r
+ ).\r
+\r
+solve(G=V,_,if(G=V,assumed),_,ass(A0,PAs,P),ass(A1,PAs,P)) :-\r
+ arbit(G,V),\r
+ (member((G=V1),A0)\r
+ ->\r
+ V=V1, A1=A0\r
+ ;\r
+ nonvar(V) -> % this seems to be necessary to get it to work.\r
+ % The arbitrary choice has not been made, but this call\r
+ % isn't making the choice.\r
+ A1=[G=V|A0];\r
+ A1=[G=V|A0]\r
+% fail\r
+% gensym(ind,V),\r
+% A1=[G=V|A0]\r
+ ).\r
+ \r
+solve(G,_,if(G,asked),WT,A0,A0) :-\r
+ askabl(G),\r
+ ask_user(G,WT,Ans),\r
+ Ans \== unknown,!, % fail if Ans=unknown, otherwise don't try clauses\r
+ Ans=yes.\r
+solve(H,_,if(H,builtin),WT,A0,A0) :-\r
+ builtin(H,C),!,\r
+ (C -> catch(H,_,debugging_builtin_error(H,WT))\r
+ ; write_all(['Error: "',H,'" can''t be called in this form, as ',C,' isn''t true.']), \r
+ debugging_builtin_error(H,WT)\r
+ ).\r
+solve(H,N0,if(H,BT),WT,A0,A1) :-\r
+ N0 > 0,\r
+ deter(H),\r
+ N1 is N0-1,\r
+ (H <- B),\r
+ solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1), !.\r
+solve(H,N0,if(H,BT),WT,A0,A1) :-\r
+ N0 > 0,\r
+ N1 is N0-1,\r
+ (H <- B),\r
+ solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1).\r
+solve(H,0,if(H,asked),WT,ass(A0,PAs0,P0),ass(A0,PAs0,P0)) :-\r
+ debugging_failure,!,\r
+ debugging_failure_goal(H,WT,P0).\r
+solve(_,0,_,_,ass(_,_,P),_) :-\r
+ retractall(failed(_)),\r
+ assert(failed(unnaturally)),\r
+ P>0,\r
+ retract(pruned_prob(PP)),\r
+ PP1 is PP+P,\r
+ asserta(pruned_prob(PP1)),\r
+ fail.\r
+\r
+% report(Query,Res,Ass) report an answer after an ask\r
+report(Q,Res,ass([],[],1)) :- !,\r
+ write_all(['Answer: ',Q,'.']),\r
+ report_runtime,\r
+ writel([' [ok,more,how,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_report(Comm,Q,Res,ass([],[],1)).\r
+report(Q,Res,Ass) :-\r
+ write_all(['Answer: ',Q,'.']),\r
+ ( Ass=ass(A0,[],1) ->\r
+ write_all(['Assuming: ',A0,'.'])\r
+ ; write_all(['Assuming: ',Ass,'.'])),\r
+ report_runtime,\r
+ writel([' [more,ok,how,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_report(Comm,Q,Res,Ass).\r
+\r
+% interpret_report(Comm,Q,Res,Ass) interprets the answer given by the user\r
+% to an answer given after and ask \r
+interpret_report(ok,_,_,_) :- !.\r
+interpret_report(more,_,_,_) :- !,\r
+ reset_runtime,fail.\r
+interpret_report(end_of_file,_,_,_) :- !,\r
+ write_all(['^D']).\r
+interpret_report(how,Q,Res,Ass) :- !,\r
+ traverse(Res,Rep),\r
+ ( (Rep = top; Rep=up)\r
+ -> report(Q,Res,Ass)\r
+ ; Rep= retry\r
+ -> reset_runtime,fail\r
+ ; Rep=prompt\r
+ -> true\r
+ ; write_all(['This shouldn''t occur. Traverse reported ',Rep])\r
+ ).\r
+interpret_report(help,Q,Res,Ass) :- !,\r
+ write_all([\r
+ ' The system has proven an instance of your query.',nl,\r
+ ' You can give the following commands:',nl,\r
+ ' more. for more answers',nl,\r
+ ' ok. for no more answers',nl,\r
+ ' how. to enter a dialog to determine how the goal was proved.']),\r
+ report(Q,Res,Ass).\r
+interpret_report(Comm,Q,Res,Ass) :-\r
+ Comm \== more,\r
+ write_all(['Unknown command; ',Comm,'. Type "help." if you need help.']),\r
+ report(Q,Res,Ass).\r
+\r
+% Depth-bound reached\r
+% debugging_failure_goal(H,WT,P)\r
+% H is the current goal\r
+% WT is the why-tree\r
+% P is the probability of this proof\r
+debugging_failure_goal(H,WT,P) :-\r
+ write_all([' Depth-bound reached. Current subgoal: ',H,'.']),\r
+ writel([' [fail,succeed,proceed,why,ok,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_debugging_failure_command(Comm,H,WT,P).\r
+\r
+\r
+% interpret_debugging_failure_command(Comm,H,WT,P)\r
+% Comm is the command the user gave\r
+% H is the current goal\r
+% WT is the why-tree\r
+% P is the probability of this proof\r
+\r
+interpret_debugging_failure_command(help,H,WT,P) :- !,\r
+ write_all([\r
+ ' The system has reached the depth bound.',nl,\r
+ ' You can give the following commands:',nl,\r
+ ' fail. fail this subgoal.',nl,\r
+ ' succeed. make this subgoal succeed.',nl,\r
+ ' proceed. fail and don''t stop any more at failing subgoals.',nl,\r
+ ' why. determine why this subgoal was called.',nl,\r
+ ' ok. return to ailog prompt.',nl,\r
+ ' help. print this message.']),\r
+ debugging_failure_goal(H,WT,P).\r
+interpret_debugging_failure_command(fail,_,_,P) :- !,\r
+ retractall(failed(_)),\r
+ assert(failed(unnaturally)),\r
+ P>0,\r
+ retract(pruned_prob(PP)),\r
+ PP1 is PP+P,\r
+ asserta(pruned_prob(PP1)),\r
+ fail.\r
+interpret_debugging_failure_command(succeed,_,_,_) :- !.\r
+interpret_debugging_failure_command(proceed,_,_,P) :- !,\r
+ retractall(debugging_failure),\r
+ retractall(failed(_)),\r
+ assert(failed(unnaturally)),\r
+ P>0,\r
+ retract(pruned_prob(PP)),\r
+ PP1 is PP+P,\r
+ asserta(pruned_prob(PP1)),\r
+ fail.\r
+interpret_debugging_failure_command(ok,_,_,_) :- !,\r
+ throw(prompt).\r
+interpret_debugging_failure_command(end_of_file,_,_,_) :- !,\r
+ throw(prompt).\r
+interpret_debugging_failure_command(why,H,WT,P) :- !,\r
+ \+ \+ (mynumbervars(WT,0,_),why_question(WT,_)),\r
+ debugging_failure_goal(H,WT,P).\r
+interpret_debugging_failure_command(Comm,H,WT,P) :- !,\r
+ write_all([' Unknown command: ',Comm,'. Type "help." for help.']),\r
+ debugging_failure_goal(H,WT,P).\r
+\r
+\r
+% builtin(G,C) is true if goal G is defined in the system (as opposed to \r
+% being defined in clauses). C is the condition that must hold to make sure\r
+% there are no errors.\r
+builtin((A =< B), ground((A =< B))).\r
+builtin((A >= B), ground((A >= B))).\r
+builtin((A =\= B), ground((A =\= B))).\r
+builtin((A < B), ground((A<B))).\r
+builtin((A > B), ground((A>B))).\r
+builtin((_ is E),ground(E)).\r
+builtin(number(E),ground(E)).\r
+builtin(atomic(E),ground(E)).\r
+\r
+% Error in a built-in\r
+debugging_builtin_error(H,WT) :-\r
+ debug_error([' Error in built-in predicate: ',H,'.'],WT).\r
+\r
+% RUNTIME ERROR HANDLING\r
+debug_error(Message,WT) :-\r
+ write_all(Message),\r
+ writel([' [fail,succeed,why,ok,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_error_command(Comm,Message,WT).\r
+\r
+interpret_error_command(help,Message,WT) :- !,\r
+% write_all(Message),\r
+ write_all([\r
+ ' You can give the following commands:',nl,\r
+ ' fail. fail this subgoal.',nl,\r
+ ' succeed. make this subgoal succeed.',nl,\r
+ ' why. determine why this subgoal was called.',nl,\r
+ ' ok. return to ailog prompt.',nl,\r
+ ' help. print this message.']),\r
+ debug_error(Message,WT).\r
+interpret_error_command(fail,_,_) :- !,\r
+ fail.\r
+interpret_error_command(succeed,_,_) :- !.\r
+interpret_error_command(ok,_,_) :- !,\r
+ throw(prompt).\r
+interpret_error_command(end_of_file,_,_) :- !,\r
+ throw(prompt).\r
+interpret_error_command(why,H,WT) :- !,\r
+ \+ \+ (mynumbervars(WT,0,_),why_question(WT,_)),\r
+ debug_error(H,WT).\r
+interpret_error_command(Comm,H,WT) :- !,\r
+ write_all([' Unknown command: ',Comm,'. Type "help." for help.']),\r
+ debug_error(H,WT).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% ASK THE USER\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% ask_user(G,WT,Ans)\r
+% G is the goal to ask\r
+% WT is the why-tree\r
+% Ans is the reply\r
+ask_user(G,_,Ans) :-\r
+ ground(G),\r
+ asked(G,Ans1),!,Ans=Ans1.\r
+ask_user(G=V,_,yes) :-\r
+ ground(G),\r
+ asked(G=V1,yes),!,V=V1.\r
+\r
+ask_user(T=V,WT,Ans) :-\r
+ ground(T),var(V),!,\r
+ writel(['What is the value of ',T,'? [value,unknown,why,help]: ']),\r
+ flush_and_read(Reply),\r
+ (member(Reply,[unknown,why,help])\r
+ -> interpret_ask_answer(Reply,T=V,WT,Ans)\r
+ ; V=Reply,\r
+ interpret_ask_answer(yes,T=V,WT,Ans)\r
+ ).\r
+ask_user(G,WT,Ans) :-\r
+ ground(G),!,\r
+ writel(['Is ',G,' true? [yes,no,unknown,why,help]: ']),\r
+ flush_and_read(Rep),\r
+ interpret_ask_answer(Rep,G,WT,Ans).\r
+ \r
+ask_user(G,WT,fail) :-\r
+ write_all([' Error: Askables with free variables not implemented.',nl,\r
+ ' The system wanted to ask ',G,'.',nl,\r
+ ' Entering why interation.']),\r
+ mynumbervars(WT,0,_),\r
+ why_question(WT,_),\r
+ write_all([' Askable subgoal ',G,' failing due to free variables.']).\r
+\r
+\r
+% interpret_ask_answer(Rep,G,WT,Ans).\r
+interpret_ask_answer(help,G,WT,Rep) :- !,\r
+ write_all([' The system is asking whether ',G,' is true or not. Give one of:',nl,\r
+ ' "yes." if ',G,' is known to be true.',nl,\r
+ ' "no." if ',G,' is known to be false.',nl,\r
+ ' "unknown." if ',G,' is unknown (so applicable clauses can be used).',nl,\r
+ ' "fail." to fail the subgoal (but not record an answer).',nl,\r
+ ' "why." to see why the system was asking this question.',nl,\r
+ ' "prompt." to return to the ailog prompt.',nl,\r
+ ' "help." to print this message.']),\r
+ ask_user(G,WT,Rep).\r
+interpret_ask_answer(yes,G,_,yes) :- !,\r
+ assertz(asked(G,yes)).\r
+interpret_ask_answer(no,G,_,no) :- !,\r
+ assertz(asked(G,no)).\r
+interpret_ask_answer(unknown,G,_,unknown) :- !,\r
+ assertz(asked(G,unknown)).\r
+interpret_ask_answer(fail,_,_,fail) :- !.\r
+interpret_ask_answer(prompt,_,_,_) :- !,\r
+ throw(prompt).\r
+interpret_ask_answer(end_of_file,_,_,_) :- !,\r
+ write_all(['^D']),\r
+ throw(prompt).\r
+\r
+interpret_ask_answer(why,G,WT,Rep) :- !,\r
+ \+ \+ ( mynumbervars(WT,0,_),why_question(WT,Rep),Rep \== prompt),\r
+ ask_user(G,WT,Rep).\r
+interpret_ask_answer(Ans,G,WT,Rep) :-\r
+ Ans \== fail,\r
+ write_all([' Unknown response "',Ans,'". For help type "help.".']),\r
+ ask_user(G,WT,Rep).\r
+\r
+\r
+% why_question(WT,Rep)\r
+% WT is a list of wrule(Head,LeftTree,Current,RightBody)\r
+% Rep is the reply. It is one of:\r
+% down go back one step\r
+% bottom return to the ask-the-user query\r
+% prompt return to prompt\r
+why_question([wrule(H,LT,C,RB)|WT],Rep) :-\r
+ write_all([' ',C,' is used in the rule ']),\r
+ write_all([' ',H,' <-']),\r
+ print_tree_body(LT,1,Max),\r
+ write_all([' ** ',Max,': ',C]),\r
+ M1 is Max+1,\r
+ print_body(RB,M1,_),\r
+ writel([' [Number,why,help,ok]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_why_ans(Comm,Max,[wrule(H,LT,C,RB)|WT],Rep).\r
+why_question([],down) :-\r
+ write_all([' This was the original query.']).\r
+\r
+% interpret_why_ans(Comm,[wrule(H,LT,C,RB)|WT],Rep).\r
+interpret_why_ans(help,Max,[wrule(H,LT,C,RB)|WT],Rep) :- !,\r
+ write_all([\r
+' You can taverse the proof for a subgoal using following commands:',nl,\r
+' how i. show how element i (i<',Max,') of the body was proved.',nl,\r
+' how ',Max,'. show the rule being considered for ',C,'.',nl,\r
+' why. show why ',H,' is being proved.',nl,\r
+' prompt. return to the ailog prompt.',nl,\r
+' help. print this message.']),\r
+ why_question([wrule(H,LT,C,RB)|WT],Rep).\r
+interpret_why_ans(up,_,WT,Rep) :- !,\r
+ interpret_why_ans(why,_,WT,Rep).\r
+interpret_why_ans(why,_,[WR|WT],Rep) :- !,\r
+ why_question(WT,Rep1),\r
+ (Rep1 = down\r
+ -> why_question([WR|WT],Rep)\r
+ ; Rep=Rep1).\r
+interpret_why_ans((how N),Max,[wrule(H,LT,C,RB)|WT],Rep) :-\r
+ integer(N),!,\r
+ interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep).\r
+interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep) :-\r
+ integer(N),\r
+ N > 0,\r
+ N < Max, !,\r
+ nth(LT,1,_,N,E),\r
+ traverse(E,Rep1),\r
+ (Rep1=up -> why_question([wrule(H,LT,C,RB)|WT],Rep) ;\r
+ Rep1=top -> Rep=bottom ;\r
+ Rep1=retry\r
+ -> write_all([' retry doesn''t make sense here.']),\r
+ why_question([wrule(H,LT,C,RB)|WT],Rep) ;\r
+ Rep=Rep1).\r
+interpret_why_ans(Max,Max,_,down) :- !.\r
+interpret_why_ans(N,Max,WT,Rep) :-\r
+ integer(N),\r
+ N > Max, !,\r
+ write_all(['You can''t trace this, as it hasn''t been proved.']),\r
+ why_question(WT,Rep).\r
+interpret_why_ans(end_of_file,_,_,_) :- !,\r
+ write_all(['^D']),\r
+ throw(prompt).\r
+interpret_why_ans(prompt,_,_,_) :- !,\r
+ throw(prompt).\r
+interpret_why_ans(ok,_,_,bottom) :- !.\r
+\r
+interpret_why_ans(Comm,_,WT,Rep) :- !,\r
+ write_all(['Unknown command: ',Comm,'. Type "help." for help.']),\r
+ why_question(WT,Rep).\r
+\r
+\r
+% print_body(B,N) is true if B is a body to be printed and N is the \r
+% count of atoms before B was called.\r
+print_body(true,N,N) :- !.\r
+print_body((A&B),N0,N2) :- !,\r
+ print_body(A,N0,N1),\r
+ print_body(B,N1,N2).\r
+print_body(H,N,N1) :-\r
+ write_all([' ',N,': ',H]),\r
+ N1 is N+1.\r
+\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% NEGATION AS FAILURE\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% failtoprove(G,N,T,WT,A0,A1) \r
+% G is a ground goal, \r
+% N is a depth-bound\r
+% T is the tree returned\r
+% WT is the why tree\r
+% A0 is the assumables before and A1 is the set after\r
+% The complication here is due to the interaction with the depth-bound\r
+% and assumables\r
+\r
+failtoprove(G,N,nafproof(PA1,ETs),WT,ass(A,PAs,Pr),ass(A,PA1,Pr1)) :-\r
+ failed(HowFailedInit),\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ findall(et(Ass,T),solve(G,N,T,~WT,ass(A,PAs,Pr),Ass),ETs),\r
+ (failed(naturally) ->\r
+ extract_expls(ETs,EGs),\r
+ duals(EGs,PAs,[PAs],Ds),\r
+ member(PA1,Ds),\r
+ prob(PA1,1,Pr1)\r
+ ;\r
+ member(et(ass(A,PAs,Pr),_),ETs) -> % found a proof with no assumptions \r
+ retractall(failed(_)),\r
+ assert(failed(HowFailedInit)),\r
+ fail % fail naturally\r
+ ;\r
+ fail % fail unnaturally as depth-bound was hit\r
+ ).\r
+\r
+/* interaction with depth-bound\r
+ (failed(naturally) ->\r
+ (solve(G,N,_,WT,[],_) ->\r
+ retract(failed(unnaturally)), asserta(failed(naturally)),fail\r
+ % note this just fails if failed(naturally) still true\r
+ ; failed(naturally)\r
+ )\r
+ ; retract(failed(_)),\r
+ assert(failed(naturally)),\r
+ (solve(G,N,_,WT,[],_) ->\r
+ retract(failed(naturally)), asserta(failed(unnaturally)),fail\r
+ ; retract(failed(naturally)), asserta(failed(unnaturally))\r
+ % note this just fails if failed(unnaturally) still true\r
+ )).\r
+*/\r
+\r
+\r
+% prob(AL,P0,P1) \r
+% AL is a list of probabilistic assumables\r
+% P1 = P0*P(AL)\r
+prob([],P,P).\r
+prob([H|T],P0,P2) :-\r
+ choice(H,P,_),\r
+ P1 is P0*P,\r
+ prob(T,P1,P2).\r
+\r
+\r
+% The following code gives the interaction between negation and probabilities\r
+\r
+% A composite choice is a consistent set of probabilistic assumables.\r
+\r
+% duals(Es,R0,D0,D1) is true if Es is a list of terms of the form\r
+% ass(A,PAs,Pr) where R0 is a subset of PAs, and \r
+% D1-D0 is a list of ass(A1,R1,P1) such that\r
+% R1-R0 is a hitting set of negations of Es.\r
+\r
+duals([],_,D,D).\r
+duals([S|L],R0,D0,D2) :- !,\r
+ setDiff(S,R0,NA),\r
+ hit_every_complement(NA,D0,[],D1),\r
+ duals(L,R0,D1,D2).\r
+\r
+% hit_every_complement(S,R0,D0,D,D1) is true if S is a composite choice (with\r
+% tail R0), and D2 is D together with the hitting set of negations of\r
+% D0.\r
+\r
+hit_every_complement([],_,D0,D0) :- !.\r
+hit_every_complement([A|R],Ds,D0,D2) :-\r
+ choice(A,_,NAs),\r
+ hit_every_element(NAs,Ds,D0,D1),\r
+ hit_every_complement(R,Ds,D1,D2).\r
+\r
+% hit_every_element(As,A,D0,D1) is true if S is a composite choice (with\r
+% tail R0), and D2 is D together with the hitting set of negations of\r
+% D0.\r
+\r
+hit_every_element([],_,D,D).\r
+hit_every_element([E|T],Es,D0,D2) :-\r
+ insert_into_each_exp(Es,E,D0,D1),\r
+ hit_every_element(T,Es,D1,D2).\r
+\r
+% insert_into_each_exp(L,A,L0,L1) is true if inserting atomic choice A\r
+% into each explanation in L, and adding these to L0 produces L1. L,\r
+% L0 and L1 are all lists of explanations. Subsumed and inconsistent\r
+% explanations are removed. \r
+\r
+insert_into_each_exp([],_,L,L) :-!.\r
+insert_into_each_exp([E1|R],A,L0,L1) :-\r
+ incompatible(A,E1),!,\r
+ insert_into_each_exp(R,A,L0,L1).\r
+insert_into_each_exp([E1|R],A,L0,L2) :-\r
+ insert_into_sorted_list(A,E1,E2),\r
+ insert_exp(E2,L0,L1),\r
+ insert_into_each_exp(R,A,L1,L2).\r
+\r
+% insert_exp(E,Es1,Es2) is true if inserting explanation E into list\r
+% Es1 of explanations produces list of explanations Es2.\r
+insert_exp(E,[],[E]) :- !.\r
+insert_exp(E0,[E|T],[E|T]) :- \r
+ subset_sorted(E,E0),!. % includes the case where E0==E.\r
+insert_exp(E0,[E|T],R) :-\r
+ subset_sorted(E0,E),!,\r
+ insert_exp(E0,T,R).\r
+insert_exp(E,[H|T],[H|R]) :-\r
+ insert_exp(E,T,R).\r
+\r
+% mutually_incompatible(As1,As2) is true if A is inconsistent with all of As.\r
+mutually_incompatible(E1,E2) :-\r
+ member(A,E1),\r
+ incompatible(A,E2).\r
+\r
+% incompatible(A,As) is true if A is inconsistent with all of As.\r
+incompatible(A,E) :-\r
+ choice(A,_,NAs),\r
+ \+ consistent(E,NAs).\r
+ \r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% Probabilities\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% normalize(L,Sum,LS) Sum is assumed to be a float.\r
+normalise([],_,[]).\r
+normalise([(A:P)|R],S,[(A:PN)|RN]) :-\r
+ PN is P/S,\r
+ normalise(R,S,RN).\r
+ \r
+% make_choices(L)\r
+make_choices(L) :-\r
+ remove(A:P,L,L0),\r
+ setof(AA,P1^member(AA:P1,L0),Alts),\r
+ assertz(choice(A,P,Alts)),\r
+ fail.\r
+make_choices(_).\r
+\r
+% insertUpdateProbs(PAs0,P0,G,P,PAs1,P1)\r
+% PAs0 is the initial probabilistic assumptions\r
+% P0 is the probability of the probablistic assumptions\r
+% G is the choice\r
+% P is the probability of G\r
+% PAs1 is the resulting probabilistic assumptions\r
+% P1 is the resulting probability\r
+insertUpdateProbs([],P0,G,P,[G],P1) :-\r
+ P1 is P0*P.\r
+insertUpdateProbs([G|R],P0,G,_,[G|R],P0) :- !.\r
+insertUpdateProbs([G0|R0],P0,G,P,[G,G0|R0],P1) :-\r
+ G @< G0, !,\r
+ P1 is P0*P.\r
+insertUpdateProbs([G0|R0],P0,G,P,[G0|PAs1],P1) :-\r
+ insertUpdateProbs(R0,P0,G,P,PAs1,P1).\r
+\r
+% latest_explanations(Obervations,ETs,Prob,Err)\r
+% ETs is a list of et(Explanation,ProofTree)\r
+latest_explanations(O,E,P,Err) :-\r
+ explanations(O,E,P,Err),!.\r
+latest_explanations([],[et(ass([],[],1),null)],1,0.0).\r
+\r
+% predict(G)\r
+% Warning: this may not work properly with multiple answers + errors\r
+% We should really reset the pruned_prob for each proof...\r
+predict(G) :-\r
+ latest_explanations(_,ETs,Pr0,Err0),\r
+ retractall(pruned_prob(_)),\r
+ assert(pruned_prob(Err0)),\r
+ depth_bound(DB),\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ reset_runtime,\r
+ find_expls(G,ETs,DB,Expls),\r
+ extract_expls(Expls,Sexpls),\r
+ make_disjoint(Sexpls,DExpls),\r
+ acc_probs(DExpls,0,Pr),\r
+ pruned_prob(Err1),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr,Err0,Err1).\r
+predict(_) :-\r
+ write_all(['No (more) answers.']).\r
+\r
+% observe(G)\r
+observe(G) :-\r
+ retractall(debugging_failure),\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ latest_explanations(Obs,ETs,PrObs,Err0),\r
+ retractall(pruned_prob(_)),\r
+ assert(pruned_prob(Err0)),\r
+ depth_bound(DB),\r
+ reset_runtime,\r
+ find_expls(G,ETs,DB,Expls),\r
+ extract_expls(Expls,Sexpls),\r
+ make_disjoint(Sexpls,DExpls),\r
+ acc_probs(DExpls,0,Pnew),\r
+ pruned_prob(Err1),\r
+ asserta(explanations([G|Obs],Expls,Pnew,Err1)),\r
+ report_expls(Expls,DExpls,G,PrObs,Pnew,Err0,Err1).\r
+observe(_) :-\r
+ write_all(['No (more) answers.']).\r
+\r
+% find_expls(G,ETs,DB,Expls)\r
+% +G is the goal to be solved\r
+% +ETs is the list of explanations of previous observations\r
+% +DB is the depth-bound\r
+% -Expls is the list of explanations of G and the previous observations\r
+find_expls(G,ETs,DB,Expls) :-\r
+ bagof(et(Expl,Res),\r
+ E0^Tr^( member(et(E0,Tr),ETs),\r
+ solve(G,DB,Res,[wrule(yes,true,G,true)],E0,Expl)), \r
+ Expls),\r
+ (ground(Expls) ->\r
+ true\r
+ ; write_all(['Warning Explanations not ground: ',Expls])).\r
+\r
+% report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1)\r
+% +Ets is a list of et(Explanation,ProofTree)\r
+% +DExpls is a set of possible worlds (disjoint explanations)\r
+% +G is the goal\r
+% +Pr0 is the probability of the previous observations\r
+% +Pr1 is the probability of the current observations\r
+% +Err0 is the error (pruned probability mass) before the query\r
+% +Err1 is the error (pruned probability mass) after the query Err1>Err0\r
+report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-\r
+ (Err1=:=0.0\r
+ ->\r
+ Post is Pr1/Pr0\r
+ ;\r
+ Min is Pr1/(Pr0+Err0),\r
+ Max is (Pr1+Err1)/(Pr0+Err0),\r
+ Post=[Min,Max]\r
+ ),\r
+ write_all(['Answer: P(',G,'|Obs)=',Post,'.']),\r
+ report_runtime,\r
+ writel([' [ok,more,explanations,worlds,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+\r
+% acc_probs(Expls,P0,P1) determines the probabilities of the assumables in Expls\r
+% +Expls is a list of explanations\r
+% +P0 is the previous probability\r
+% -P1 is the new probability\r
+acc_probs([],P,P).\r
+acc_probs([A|R],P0,P2) :-\r
+ prob_expl(A,1,P),\r
+ P1 is P+P0,\r
+ acc_probs(R,P1,P2).\r
+\r
+% probs_expl(Expl,P0,P1) determines the probability of an expanation\r
+% +Expl is an explanation\r
+% +P0 is the previous probability\r
+% -P1 is the resulting probability (P1 = P0*prob(Expl))\r
+prob_expl([],P,P).\r
+prob_expl([A|R],P0,P2) :-\r
+ choice(A,P,_),\r
+ P1 is P*P0,\r
+ prob_expl(R,P1,P2).\r
+\r
+% interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1)\r
+% +Comm is the command given by the user\r
+% +Expls is the set of explanations\r
+% +DExpls is the set of worlds (disjoint explanations)\r
+% +G is the goal to be proved\r
+% +Pr0 is the probability of the previous observations\r
+% +Pr1 is the probability of the current observations\r
+interpret_prob_report(ok,_,_,_,_,_,_,_) :- !.\r
+interpret_prob_report(more,_,_,_,_,_,_,_) :- !,\r
+ reset_runtime,fail.\r
+interpret_prob_report(end_of_file,_,_,_,_,_,_,_) :- !,\r
+ write_all(['^D']).\r
+interpret_prob_report(explanations,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_prob_report(worlds,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ print_worlds(DExpls,0),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_prob_report(help,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ write_all([\r
+ ' The system has proven an instance of your query.',nl,\r
+ ' You can give the following commands:',nl,\r
+ ' more. for more answers',nl,\r
+ ' ok. for no more answers',nl,\r
+ ' explanations. to explore how the goal is proved based ',\r
+ ' sets of assumptions.',nl,\r
+ ' worlds. to see the worlds where ',G,' is true.']),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_prob_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-\r
+ Comm \== more,\r
+ write_all(['Unknown command; ',Comm,'. Type "help." if you need help.']),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+\r
+% show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1)\r
+show_explanations(Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-\r
+ print_explanations(Expls,0),\r
+ writel([' [ok,more,how i,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+\r
+% interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1)\r
+interpret_show_explanations_report(ok,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_show_explanations_report(more,_,_,_,_,_,_,_) :- !,\r
+ reset_runtime,fail.\r
+interpret_show_explanations_report(how I,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :-\r
+ catch(\r
+ (\r
+ ith(Expls,et(_,Tree),I,0),\r
+ traverse(Tree,_) % Report is ignored\r
+ ),\r
+ Ex,\r
+ (Ex= outofrange ->\r
+ write_all(['Number out of range: how ',I,'.'])\r
+ ; write_all(['Argument to how must be an integer: how ',I,'.']) \r
+ )\r
+ ),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_show_explanations_report(help,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ write_all([\r
+ 'ok. go back to answer dialogue',nl,\r
+ 'more. get another answer.',nl,\r
+ 'how i. ask how the ith explanation was proved',nl,\r
+ 'help. print this message']),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+interpret_show_explanations_report(Comm,Expls,DExpls,G,Pr0,Pr1,Err0,Err1) :- !,\r
+ write_all([\r
+ 'Unknown command: ',Comm,'. Type "help." for help']),\r
+ report_expls(Expls,DExpls,G,Pr0,Pr1,Err0,Err1).\r
+\r
+% print_explanations(DExpls,Count).\r
+print_explanations([],_).\r
+print_explanations([et(W,_)|R],C) :-\r
+ write_all([' ',C,': ', W]),\r
+ C1 is C+1,\r
+ print_explanations(R,C1).\r
+\r
+% print_worlds(DExpls,Count).\r
+print_worlds([],_).\r
+print_worlds([W|R],C) :-\r
+ prob_expl(W,1,Pr),\r
+ write_all([' ',C,': ', W,' Prob=',Pr]),\r
+ C1 is C+1,\r
+ print_worlds(R,C1).\r
+\r
+% print_observations(Obs,N)\r
+print_observations([],0).\r
+print_observations([O|Os],N1) :-\r
+ print_observations(Os,N),\r
+ N1 is N+1,\r
+ write_all([N1,': ',O]).\r
+\r
+\r
+% extract_expls(L1,L2) L1 is a list of et(ass(_,E,_),_) and L2 is the\r
+% corresponding list of explanations E. \r
+extract_expls([],[]).\r
+extract_expls([et(ass(_,E,_),_)|L],R1) :-\r
+ extract_expls(L,R),\r
+ insert_exp(E,R,R1).\r
+\r
+% make_disjoint(L,SL) is true if L is a list of explanations and SL\r
+% is a lists of Expl such that SL are mutually exclusive and cover\r
+% the same worlds as the Expls in L.\r
+% This assumes that L is a minimal set: no member of L is a subset of another.\r
+\r
+make_disjoint([],[]).\r
+make_disjoint([R|L],L2) :-\r
+ % check_sorted(R),\r
+ member(R1,L),\r
+ % check_sorted(R1),\r
+ \+ mutually_incompatible(R,R1),!,\r
+ (member(E,R1), \+ idmember(E,R) %%% was \+ member(E,R)\r
+ -> true; write_all(['Error in make_disjoint: ',compatible(R,R1)]),fail),\r
+ choice(E,_,NE),\r
+ split([E|NE],R,L,L1),\r
+ make_disjoint(L1,L2).\r
+make_disjoint([E|L1],[E|L2]) :-\r
+ make_disjoint(L1,L2).\r
+\r
+% split(As,R,L0,L1) splits R on As, added to L0 produces L1\r
+split([],_,L,L).\r
+split([A|As],E,L0,L2) :-\r
+ insert_into_sorted_list(A,E,E1),\r
+ insert_exp(E1,L0,L1),\r
+ split(As,E,L1,L2).\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% HOW QUESTIONS\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% traverse(T,Rep) true if \r
+% T is a tree being traversed\r
+% Rep is the reply it is one of {up,top,retry,prompt}\r
+% up means go up in the tree \r
+% top means go to the top of the tree (where traverse was called).\r
+% retry means find another proof tree\r
+% prompt means go to the top level prompt\r
+traverse((A&B),Rep) :-\r
+ traverse(if(yes,(A&B)),Rep).\r
+traverse(if(H,true),up) :- !,\r
+ write_all([' ',H,' is a fact']).\r
+traverse(if(H,builtin),up) :- !,\r
+ write_all([' ',H,' is built-in.']).\r
+traverse(if(H,asked),up) :- !,\r
+ write_all([' You told me ',H,' is true.']).\r
+traverse(if(H,assumed),up) :- !,\r
+ write_all([' ',H,' is assumed.']).\r
+traverse(if(~G,nafproof(_,[])),Rep) :- !,\r
+ write_all([' ',G,' finitely failed. You can examine the search space.']),\r
+ depth_bound(DB),\r
+ whynotb(G,DB,Rep,ass([],[],1),_).\r
+traverse(if(~G,nafproof(Expl,ETs)),Rep) :- !,\r
+ write_all([' ',~G,' succeeded assuming ',Expl]),\r
+ write_all([' ',G,' succeeded with the following explanations:']),\r
+ print_explanations(ETs,0),\r
+ writel([' [up,top,retry,prompt,how i,help,whynot]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_naf_how(Comm,ETs,Rep0),\r
+ (Rep0=repeat ->\r
+ traverse(if(~G,nafproof(Expl,ETs)),Rep)\r
+ ; Rep=Rep0\r
+ ).\r
+traverse(null,top) :- !,\r
+ write_all([' There was nothing to be proved.']).\r
+traverse(if(H,B),Rep) :-\r
+ write_all([' ',H,' <-']),\r
+ print_tree_body(B,1,Max),\r
+ writel([' How? [Number,up,retry,ok,prompt,help]: ']),\r
+ flush_and_read(Comm),\r
+ interpretcommand(Comm,B,Max,if(H,B),Rep).\r
+\r
+% print_tree_body(B,N) is true if B is a body to be printed and N is the \r
+% count of atoms before B was called.\r
+print_tree_body(true,N,N).\r
+print_tree_body((A&B),N0,N2) :-\r
+ print_tree_body(A,N0,N1),\r
+ print_tree_body(B,N1,N2).\r
+print_tree_body(if(H,_),N,N1) :-\r
+ write_all([' ',N,': ',H]),\r
+ N1 is N+1.\r
+\r
+% interpretcommand(Comm,B,Max,Goal,Reply) interprets the command Comm on body B\r
+interpretcommand(help,_,Max,G,Rep) :- !,\r
+ write_all([\r
+ ' Give either (end each command with a period):',nl,\r
+ ' how i. explain how subgoal i (i<',Max,') was proved.',nl,\r
+ ' up. go up the proof tree one level.',nl,\r
+ ' retry. find another proof.',nl,\r
+ ' ok. stop traversing the proof tree.',nl,\r
+ ' prompt. return to the ailog prompt.',nl,\r
+ ' help. to print this message.']),\r
+ traverse(G,Rep).\r
+interpretcommand((how N),B,Max,G,Rep) :-\r
+ integer(N),\r
+ interpretcommand(N,B,Max,G,Rep).\r
+interpretcommand(N,B,Max,G,Rep) :-\r
+ integer(N),\r
+ N > 0,\r
+ N < Max,!,\r
+ nth(B,1,_,N,E),\r
+ traverse(E,Rep1),\r
+ ( Rep1= up\r
+ -> traverse(G,Rep)\r
+ ; Rep=Rep1\r
+ ).\r
+interpretcommand(N,_,Max,G,Rep) :-\r
+ integer(N),!,\r
+ % (N < 1 ; N >= Max,Rep),\r
+ M1 is Max-1,\r
+ write_all(['Number out of range: ',N,'. Use number in range: [1,',M1,'].']),\r
+ traverse(G,Rep).\r
+interpretcommand(up,_,_,_,up) :-!.\r
+interpretcommand(why,_,_,_,up) :-!.\r
+interpretcommand(ok,_,_,_,top) :-!.\r
+interpretcommand(prompt,_,_,_,_) :-!,\r
+ throw(prompt).\r
+interpretcommand(retry,_,_,_,retry) :-!.\r
+interpretcommand(end_of_file,_,_,_,prompt) :-!,\r
+ write_all(['^D']).\r
+interpretcommand(C,_,_,G,Rep) :-\r
+ write_all(['Illegal Command: ',C,' Type "help." for help.']),\r
+ traverse(G,Rep).\r
+\r
+% nth(S,N0,N1,N,E) is true if E is the N-th element of structure S\r
+nth((A&B),N0,N2,N,E) :- !,\r
+ nth(A,N0,N1,N,E),\r
+ nth(B,N1,N2,N,E).\r
+nth(true,N0,N0,_,_) :- !.\r
+nth(A,N,N1,N,A) :- !,\r
+ N1 is N+1.\r
+nth(_,N0,N1,_,_) :-\r
+ N1 is N0+1.\r
+\r
+% interpret_naf_how(Comm,ETs,Report)\r
+% Report is either up, or repeat or whatever travese can report\r
+interpret_naf_how(ok,_,up).\r
+interpret_naf_how(more,_,_) :- !,\r
+ reset_runtime,fail.\r
+interpret_naf_how(how I,Expls,Report) :-\r
+ catch(\r
+ (\r
+ ith(Expls,et(_,Tree),I,0),\r
+ traverse(Tree,Report)\r
+ ),\r
+ Ex,\r
+ ((Ex= outofrange ->\r
+ write_all(['Number out of range: how ',I,'.'])\r
+ ; write_all(['Argument to how must be an integer: how ',I,'.']) \r
+ ),\r
+ Report=repeat)\r
+ ).\r
+interpret_naf_how(help,_,repeat) :- !,\r
+ write_all([\r
+ 'ok. go back to answer dialogue',nl,\r
+ 'more. get another answer.',nl,\r
+ 'how i. ask how the ith explanation was proved',nl,\r
+ 'help. print this message']).\r
+interpret_naf_how(Comm,_,repeat) :- !,\r
+ write_all([\r
+ 'Unknown command: ',Comm,'. Type "help." for help']).\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% WHY NOT QUESTIONS for FAILING QUERIES\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% determine why an answer to body Q was not found.\r
+% whynotb(+Q,+DB,-Rep,+Ass0,-Ass1) determine why body Q, with depth-bound DB\r
+% and Ass0 did not find an expected answer\r
+% Rep is the reply it is one of {up,top,retry,prompt}\r
+% up means go up in the tree \r
+% top means go to the top of the tree (where traverse was called).\r
+% retry means find another proof tree\r
+% prompt means go to the top level prompt\r
+\r
+whynotb((A & B),DB,Rep,Ass0,Ass2) :- \r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ solve(A,DB,Res,[whynot],Ass0,Ass1),\r
+ report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1,Ass2).\r
+whynotb((A & _),DB,Rep,Ass0,Ass1) :- !,\r
+ whynotb(A,DB,Rep,Ass0,Ass1).\r
+\r
+whynotb(call(A),DB,Rep,Ass0,Ass1) :- !,\r
+ whynotb(A,DB,Rep,Ass0,Ass1).\r
+\r
+whynotb((~ A),DB,Rep,Ass0,Ass1) :-\r
+ ground(A), !,\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ findall(et(Ass,T),solve(A,DB,T,[whynot],Ass0,Ass),ETs),\r
+ (\r
+ member(et(Ass0,T),ETs)\r
+ -> % found a proof with no assumables\r
+ write_all([' ',~A,' failed as ',A,' suceeded. Here is how:']),\r
+ traverse(T,Rep)\r
+ ; (ETs=[], failed(naturally)) ->\r
+ write_all([' ',~A,' succeeds, as ',A,' finitely fails.']),\r
+ whynotb(A,DB,Rep,Ass0,_),\r
+ Ass1=Ass0\r
+ ; failed(unnaturally) ->\r
+ write_all([' ',~A,' failed because of the depth-bound.']),\r
+ whynotb(A,DB,Rep,Ass0,_)\r
+ ;\r
+ whynotb_expls(A,ETs,Rep)\r
+ ).\r
+\r
+\r
+whynotb((~ A),_,up,Ass0,Ass0) :- !,\r
+ write_all([' Error: ',~A,' needs to be ground when called.']).\r
+\r
+whynotb(A,_,up,Ass0,Ass0) :-\r
+ builtin(A,C),!,\r
+ (call(C)\r
+ -> (call(A)\r
+ -> write_all([' ',A,' is built-in and succeeds.'])\r
+ ; write_all([' ',A,' is built-in and fails.']))\r
+ ; write_all([' ',A,' is built-in and is insufficiently instanciated.'])).\r
+\r
+whynotb((A \= B),_,up,Ass0,Ass0) :-\r
+ ?=(A,B),!,\r
+ (A \== B\r
+ -> write_all([' ',(A \= B),' succeeds as they can never unify.'])\r
+ ; write_all([' ',(A \= B),' fails as they are identical.'])).\r
+whynotb((A \= B),_,up,Ass0,Ass0) :-\r
+ write_all([' ',(A \= B),' cannot be resolved. It is delayed.']),\r
+ when(?=(A,B),\r
+ (A \== B\r
+ -> write_all([' Resolving delayed ',(A \= B),'. It succeeded.'])\r
+ ; write_all([' Failure due to delayed constraint, ',(A \= B),'.']),\r
+ fail)).\r
+whynotb((A #= B),_,up,Ass0,Ass0) :-\r
+ (\+(A = B)\r
+ -> write_all([' ',(A #= B),' succeeds as they can never unify.'])\r
+ ; write_all([' ',(A #= B),' fails as they can unify.'])).\r
+\r
+\r
+whynotb(Q,_,up,ass(A0,PAs,P),ass(A1,PAs,P)) :-\r
+ assumabl(Q),!,\r
+ (idmember(Q,A0)\r
+ ->\r
+ write_all([' ',Q,' has already been assumed. It succeeds.']),\r
+ A1=A0\r
+ ;\r
+ good(Q,A0)\r
+ ->\r
+ write_all([' ',Q,' is consistently assumed.']),\r
+ A1=[Q|A0]\r
+ ;\r
+ write_all([' ',Q,' is inconsistent with other assumables.']),\r
+ A1=A0\r
+ ).\r
+\r
+whynotb(Q,_,up,ass(A0,PAs0,P0),ass(A0,PAs1,P1)) :-\r
+ choice(Q,P,A),!,\r
+% (ground(Q) -> true\r
+% ; write_all([' Error: assumable ',Q,' needs to be ground when called.'])),\r
+ (consistent(PAs0,A)\r
+ ->\r
+ insertUpdateProbs(PAs0,P0,Q,P,PAs1,P1),\r
+ prob_threshold(Bound),\r
+ ((P1 < Bound)\r
+ ->\r
+ retract(pruned_prob(PP)),\r
+ PP1 is PP+P1,\r
+ asserta(pruned_prob(PP1)),\r
+ write_all([' ',Q,' fails as the probability (',P1,') is too small'])\r
+ ;\r
+ write_all([' ',Q,' suceeds as it can be assumed'])\r
+ )\r
+ ;\r
+ write_all([' ',Q,' fails as it is inconsistent with other assumpions'])\r
+ \r
+ ).\r
+\r
+whynotb(G=V,_,up,ass(A0,PAs,P),ass(A1,PAs,P)) :-\r
+ arbit(G,V),!,\r
+ (member((G=V1),A0)\r
+ ->\r
+ (V=V1 ->\r
+ write_all([' ',G=V,' is has already been assumed.'])\r
+ ; write_all([' arbitrary ',G,' has value ',V1,', so ',G=V,' fails.'])\r
+ ),\r
+ A1=A0\r
+ ;\r
+ write_all([' ',G=V,' is consistently assumed.']),\r
+ A1=[G=V|A0]\r
+ ).\r
+\r
+\r
+whynotb(Q,0,up,Ass0,Ass0) :- !,\r
+ write_all([' ',Q,' fails because of the depth-bound.']).\r
+\r
+% whynotb(Q,DB,up,Ass0,Ass0) :-\r
+% DB > 0,\r
+% (Q <- true),!,\r
+% write_all([' ',Q,' is a fact. It doesn''t fail.']).\r
+\r
+whynotb(Q,DB,Rep,Ass0,Ass1) :-\r
+ DB > 0,\r
+ (Q <- B),\r
+ whynotrule(Q,B,DB,Rep,Ass0,Ass1).\r
+whynotb(Q,_,up,Ass0,Ass0) :-\r
+ write_all([' There is no applicable rule for ',Q,'.']).\r
+\r
+whynotrule(Q,B,DB,Rep,Ass0,Ass1) :-\r
+ (B=true\r
+ ->\r
+ write_all([' ',Q,'.']);\r
+ write_all([' ',Q,' <- ',B,'.'])\r
+ ),\r
+ writel([' Trace this rule? [yes,no,up,help]: ']),\r
+ flush_and_read(Comm),\r
+ whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1).\r
+\r
+whynotruleinterpret(yes,Q,B,DB,Rep,Ass0,Ass1) :- !,\r
+ DB1 is DB-1,\r
+ whynotb(B,DB1,Rep1,Ass0,Ass1),\r
+ (Rep1 = up\r
+ -> whynotrule(Q,B,DB,Rep,Ass0,Ass1)\r
+ ; Rep=Rep1).\r
+whynotruleinterpret(no,_,_,_,_,_,_) :- !,\r
+ fail.\r
+whynotruleinterpret(up,_,_,_,up,Ass0,Ass0) :- !.\r
+whynotruleinterpret(end_of_file,_,_,_,prompt,_,_) :- !,\r
+ write_all(['^D']).\r
+whynotruleinterpret(ok,_,_,_,prompt,_,_) :- !.\r
+whynotruleinterpret(help,Q,B,DB,Rep,Ass0,Ass1) :- !,\r
+ write_all([\r
+ ' Do you want to examine why this rule failed?',nl,\r
+ ' yes. look at this rule',nl,\r
+ ' no. try another rule',nl,\r
+ ' up. go back to the rule this rule was called from',nl,\r
+ ' ok. go to top-level prompt']),\r
+ whynotrule(Q,B,DB,Rep,Ass0,Ass1).\r
+whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1) :-\r
+ write_all([' Unknown command: ',Comm,'. Type "help." for help.']),\r
+ whynotrule(Q,B,DB,Rep,Ass0,Ass1).\r
+\r
+\r
+report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1,Ass2) :-\r
+ write_all([' The proof for ',A,' succeeded.']),\r
+ (Ass0 \== Ass1 ->\r
+ write_all([' assuming ',Ass1])\r
+ ; true\r
+ ),\r
+ writel([' Is this the appropriate answer? [yes,no,debug,help]: ']),\r
+ flush_and_read(Comm),\r
+ why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass1,Ass2).\r
+\r
+why_not_conj_interpret(debug,A,Res,B,DB,Rep,Ass0,Ass1) :- !,\r
+ traverse(Res,Rep1),\r
+ (Rep1 = up\r
+ -> report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1)\r
+ ; Rep=Rep1).\r
+why_not_conj_interpret(yes,_,_,B,DB,Rep,Ass0,Ass1) :- !,\r
+ whynotb(B,DB,Rep,Ass0,Ass1).\r
+why_not_conj_interpret(no,_,_,_,_,_,_,_) :- !,\r
+ fail. % find another proof for A\r
+\r
+why_not_conj_interpret(end_of_file,_,_,_,_,prompt,_,_) :- !,\r
+ write_all(['^D']).\r
+why_not_conj_interpret(ok,_,_,_,_,prompt,_,_) :- !,\r
+ write_all(['^D']).\r
+why_not_conj_interpret(help,A,Res,B,DB,Rep,Ass0,Ass1) :- !,\r
+ write_all([\r
+ ' yes. this instance should have made the body succeed.',nl,\r
+ ' no. this instance should lead to a failure of the body.',nl,\r
+ ' debug. this instance is false, debug it.',nl,\r
+ ' ok. I''ve had enough. Go to the prompt.',nl,\r
+ ' help. print this message.']),\r
+ report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).\r
+why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1) :-\r
+ write_all([' Unknown command: ',Comm,'. Type "help." for help.']),\r
+ report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).\r
+\r
+whynotb_expls(A,ETs,Rep) :-\r
+ write_all([' ',~A,' succeeds, as ',A,' has the explanations: ']),\r
+ print_explanations(ETs,0),\r
+ writel([' [up,top,retry,prompt,how i,help,whynot]: ']),\r
+ flush_and_read(Comm),\r
+ interpret_naf_how(Comm,ETs,Rep0),\r
+ (Rep0=repeat ->\r
+ whynotb_expls(A,ETs,Rep)\r
+ ; Rep=Rep0\r
+ ).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% FILE INTERACTION\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+flush_and_read(T) :-\r
+ flush_output,\r
+ (read(T) -> true ; flush_and_read(T)). % reads until no error.\r
+\r
+ci_load(File) :-\r
+ current_input(OldFile),\r
+ open(File,read,Input),\r
+ set_input(Input),\r
+ flush_and_read(T),\r
+ read_all(T),\r
+ set_input(OldFile),\r
+ write_all(['AILog theory ',File,' loaded.']).\r
+\r
+read_all(C) :-\r
+ file_or_command(C,file),\r
+ flush_and_read(T2),!,\r
+ read_all(T2).\r
+\r
+read_all(end_of_file) :- !.\r
+read_all((H :- B)) :- !,\r
+ write_all(['Error: Illegal Implication: ',H,' :- ',B,'. Use <- or prload.']).\r
+read_all(T) :-\r
+ tell_clause(T),\r
+ flush_and_read(T2),!,\r
+ read_all(T2).\r
+read_all(_).\r
+\r
+prolog_load(File) :-\r
+ current_input(OldFile),\r
+ open(File,read,Input),\r
+ set_input(Input),\r
+ flush_and_read(T),\r
+ prread_all(T),\r
+ set_input(OldFile),\r
+ write_all(['AILog theory ',File,' consulted.']).\r
+\r
+\r
+prread_all(T) :-\r
+ file_or_command(T,file),\r
+ flush_and_read(T2),\r
+ prread_all(T2).\r
+prread_all(end_of_file) :- !.\r
+prread_all(T) :- \r
+ prillegal(T,Mesg),!,\r
+ write_all(Mesg).\r
+prread_all(T) :-\r
+ prtell(T),\r
+ flush_and_read(T2),\r
+ prread_all(T2).\r
+\r
+% prillegal(R,Mesg) is true if R is illegal Prolog rule. \r
+% Mesg is the corresponding error message.\r
+prillegal((H <- B),['Error. Illegal Implication: ',H,' <- ',B,\r
+ '. Use :- in prload.']) :- !.\r
+prillegal((:- B),['Error. Commands not allowed. ":- ',B,'."']) :- !.\r
+prillegal((_ :- B),Mesg) :- !,\r
+ prillbody(B,Mesg).\r
+prillbody((A,_),Mesg) :-\r
+ prillbody(A,Mesg).\r
+prillbody((_,B),Mesg) :-\r
+ prillbody(B,Mesg).\r
+prillbody((_;_),['Prolog rules assume disjunction ";". Define it before loading.']) :-\r
+ \+ ((_;_) <- _).\r
+prillbody((A;_),Mesg) :-\r
+ prillbody(A,Mesg).\r
+prillbody((_;B),Mesg) :-\r
+ prillbody(B,Mesg).\r
+prillbody((_&_),['Error. Illegal conjunction in Prolog rules: &']):- !.\r
+prillbody(!,['Error. Cut (!) not allowed.']) :- !.\r
+prillbody((_ -> _ ; _),['Error. "->" is not implemented.']) :- !.\r
+prillbody((_ -> _ ),['Error. "->" is not implemented.']) :- !.\r
+\r
+% prtell(Cl) tells the prolog clause Cl\r
+prtell((H :- B)) :- !,\r
+ convert_body(B,B1),\r
+ assertz((H <- B1)).\r
+prtell(H) :-\r
+ assertz((H <- true)).\r
+\r
+% convert_body(PB,CB) converts Prolog body PB to ailog body CB\r
+convert_body((A,B),(A1&B1)) :- !,\r
+ convert_body(A,A1),\r
+ convert_body(B,B1).\r
+convert_body((A;B),(A1;B1)) :- !,\r
+ convert_body(A,A1),\r
+ convert_body(B,B1).\r
+convert_body((\+ A),(~ A1)) :- !,\r
+ convert_body(A,A1).\r
+convert_body(A,A).\r
+\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% MAIN LOOP\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+start :-\r
+ ailog_version(V,Y),\r
+ write_all([nl,\r
+ 'AILog Version ',V,'. Copyright ',Y,', David Poole.',nl,\r
+ 'AILog comes with absolutely no warranty.',nl,\r
+ 'All inputs end with a period. Type "help." for help.']),\r
+ start1.\r
+\r
+start1 :-\r
+ catch(go,Exc,handle_exception(Exc)). \r
+\r
+go :-\r
+ writel(['ailog: ']), \r
+ flush_and_read(T),\r
+ (T == prolog ->\r
+ write_all(['Returning to Prolog. Type "start." to start ailog.'])\r
+ ; T == end_of_file ->\r
+ write_all(['^D']),\r
+ write_all(['Returning to Prolog. Type "start." to start ailog.'])\r
+ ; interpret(T),\r
+ !,\r
+ go).\r
+\r
+handle_exception(prompt) :- !, start1.\r
+handle_exception(quit) :- halt.\r
+handle_exception(Exc) :-\r
+ write_all(['Error: ',Exc]),\r
+ start1.\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% CHECKING the KB\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% check searches through the knowledge base looking for a rule\r
+% containing an atom in the body which doesn't have a corresponding\r
+% definition (i.e., a clause with it at the head).\r
+check :-\r
+ (H <- B),\r
+ body_elt_undefined(B,H,B).\r
+check.\r
+\r
+check :-\r
+ (H <- _),\r
+ choice(H,_,_),\r
+ write_all([H,' should not be defined in a rule and as a probability.']),\r
+ fail.\r
+\r
+body_elt_undefined(true,_,_) :- !,fail.\r
+body_elt_undefined((A&_),H,B) :-\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined((_&A),H,B) :- !,\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined((~ A),H,B) :- !,\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined((A;_),H,B) :-\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined((_;A),H,B) :- !,\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined(call(A),H,B) :- !,\r
+ body_elt_undefined(A,H,B).\r
+body_elt_undefined(_ \= _,_,_) :- !,fail.\r
+body_elt_undefined(_ #= _,_,_) :- !,fail.\r
+body_elt_undefined(A,_,_) :-\r
+ askabl(A),!,fail.\r
+body_elt_undefined(A,_,_) :-\r
+ assumabl(A),!,fail.\r
+body_elt_undefined(A,_,_) :-\r
+ choice(A,_,_),!,fail.\r
+body_elt_undefined(X=V,_,_) :-\r
+ arbit(X,V),!,fail.\r
+body_elt_undefined(A,_,_) :-\r
+ builtin(A,_),!,fail.\r
+body_elt_undefined(A,_,_) :-\r
+ (A <- _),!,fail.\r
+body_elt_undefined(A,H,B) :-\r
+ write_all(['Warning: no clauses for ',A,' in rule ',(H <- B),'.']),!,fail.\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% STATS\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% uncomment the next line to make runtime checking the default\r
+%checking_runtime.\r
+\r
+% stats_command(Cmd) means "stats Cmd" was given as a command.\r
+stats_command(runtime) :- !,\r
+ retractall(checking_runtime),\r
+ asserta(checking_runtime),\r
+ write_all(['Runtime report turned on. Type "stats none." to turn it off.']).\r
+stats_command(none) :- !,\r
+ retractall(checking_runtime).\r
+stats_command(_) :-\r
+ write_all(['The stats commands implemented are:']),\r
+ write_all([' stats runtime. turn on report of runtime.']),\r
+ write_all([' stats none. turn off report of runtime.']).\r
+\r
+% reset_runtime means that we are storing the current valuse of\r
+% runtime. This means that we are leaving out much of the ailog\r
+% overhead from the calcluation.\r
+\r
+reset_runtime :-\r
+ checking_runtime,\r
+ retractall(lastruntime(_)),\r
+ get_runtime(T,_),\r
+ asserta(lastruntime(T)),!.\r
+reset_runtime :-\r
+ checking_runtime ->\r
+ write_all([' Problem with runtime checking.'])\r
+ ; true.\r
+\r
+report_runtime :-\r
+ checking_runtime,\r
+ lastruntime(T),\r
+ get_runtime(T1,Units),\r
+ RT is T1 - T,\r
+ write_all([' Runtime since last report: ',RT,' ',Units,'.']),!.\r
+report_runtime :-\r
+ checking_runtime ->\r
+ write_all([' Problem with runtime reporting.'])\r
+ ; true.\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% NOGOOD Handling\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+% A nogood is a set of assumables that is inconsistent\r
+construct_nogoods(DB) :-\r
+ depth_bound(DB),\r
+ retractall(failed(_)),\r
+ assert(failed(naturally)),\r
+ reset_runtime,\r
+ solve(false,DB,PfTree,[wrule(yes,true,false,true)],ass([],[],1),ass(Ass,_,_)),\r
+ assert(nogood(Ass,PfTree)),\r
+ assert_each_nogood(Ass,[]),\r
+ fail.\r
+construct_nogoods(DB) :-\r
+ failed(naturally)\r
+ -> write_all(['Nogoods recorded. Type "nogoods." to see them.'])\r
+ ; write_all(['Nogoods recorded, but depth-bound ',DB,' reached. Type "nogoods." to see them.']).\r
+\r
+assert_each_nogood([],[]).\r
+assert_each_nogood([H|NotDone],Done) :-\r
+ append(NotDone,Done,Rest),\r
+ assert(anogood(H,Rest)),\r
+ assert_each_nogood(NotDone,[H|Done]).\r
+\r
+list_nogoods :-\r
+ nogood(NG,_),\r
+ write_all(['Nogood: ',NG,'.']), fail.\r
+list_nogoods.\r
+\r
+good(A,E) :-\r
+ \+ bad(A,E).\r
+bad(A,E) :-\r
+ ground((A,E)),\r
+ anogood(A,N),\r
+ subset(N,E).\r
+\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+%% HELPERS\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\r
+% write_all(L) writes each element of list L, ends with new line\r
+write_all(L) :-\r
+ \+ \+ (mynumbervars(L,0,_),writel0(L)),\r
+ nl.\r
+% writel(L) writes each element of list L\r
+writel(L) :-\r
+ \+ \+ (mynumbervars(L,0,_),writel0(L)).\r
+\r
+% writel0(L) writes each element of list L\r
+writel0([]) :- !.\r
+writel0([nl|T]) :- !,\r
+ nl,\r
+ writel0(T).\r
+writel0([H|T]) :-\r
+ mywrite(H),\r
+ writel0(T).\r
+\r
+% writeAllDelim(L,D) writes the elements of L using delimiter D\r
+writeAllDelim(L,D) :-\r
+ \+ \+ (mynumbervars(L,0,_),writeAllDelim0(L,D)).\r
+\r
+writeAllDelim0([],_) :-!.\r
+writeAllDelim0([E],_) :- !, mywrite(E).\r
+writeAllDelim0([H|T],nl) :- !, mywrite(H),nl,writeAllDelim0(T,nl).\r
+writeAllDelim0([H|T],D) :- mywrite(H),mywrite(D),writeAllDelim0(T,D).\r
+\r
+% mywrite(T) writes term T\r
+mywrite(T) :-\r
+ write_term(T,[numbervars(true),portray(true)]).\r
+\r
+portray(A&B) :- mywrite(A),mywrite(' & '),mywrite(B).\r
+\r
+% insert_into_sorted_list(E,L,R) inserts E into sorted list L producing R\r
+insert_into_sorted_list(A,[],[A]).\r
+insert_into_sorted_list(A,[A1|R],[A|R]) :- A == A1,!.\r
+insert_into_sorted_list(A,[A1|R],[A,A1|R]) :- A @< A1, !.\r
+insert_into_sorted_list(A,[B|R],[B|R1]) :-\r
+ insert_into_sorted_list(A,R,R1).\r
+\r
+% insertUpdateProbs(E,L) inserts E into sorted list L\r
+insertUpdateProbs(A,[],[A]).\r
+insertUpdateProbs(A,[A1|R],[A|R]) :- A == A1,!.\r
+insertUpdateProbs(A,[A1|R],[A,A1|R]) :- A @< A1, !.\r
+insertUpdateProbs(A,[B|R],[B|R1]) :-\r
+ insertUpdateProbs(A,R,R1).\r
+\r
+% consistent(L1,L2) is true if L1 & L2 are sorted lists with no\r
+% elements in common. \r
+consistent([],_) :- !.\r
+consistent(_,[]) :- !.\r
+consistent([A1|R1],[A2|R2]) :-\r
+ A1 @< A2, !,\r
+ consistent(R1,[A2|R2]).\r
+consistent([A1|R1],[A2|R2]) :-\r
+ A1 @> A2, !,\r
+ consistent([A1|R1],R2).\r
+\r
+% remove(E,L,L1) removes E from list L producing L1\r
+remove(E,[E|L],L).\r
+remove(E,[A|L],[A|R]) :-\r
+ remove(E,L,R).\r
+\r
+\r
+% subset_sorted(L1,L2) is true if list L1 is a subset of L2\r
+% all lists are assumed to be ground and sorted.\r
+subset_sorted([],_) :- !.\r
+subset_sorted([A|L1],[A|L2]) :- !,\r
+ subset_sorted(L1,L2).\r
+subset_sorted([A1|L1],[A2|L2]) :-\r
+ A2 @< A1,\r
+ subset_sorted([A1|L1],L2).\r
+\r
+% setDiff(S1,S2,S3) S3 = S1-S2. All lists are sorted.\r
+\r
+setDiff([],_,[]) :- !.\r
+setDiff(S,[],S) :- !.\r
+setDiff([A|L1],[A|L2],R) :- !,\r
+ setDiff(L1,L2,R).\r
+setDiff([A1|L1],[A2|L2],[A1|R]) :-\r
+ A1 @< A2, !,\r
+ setDiff(L1,[A2|L2],R).\r
+setDiff(L1,[_|L2],R) :-\r
+ setDiff(L1,L2,R).\r
+\r
+% mywhen(C,G) replaces "when". It does not delay, but instead gives an\r
+% error. This is now redundant as SWI has "when".\r
+mywhen(C,G) :-\r
+ C -> G \r
+ ;\r
+ write_all(['Warning: ',C,' failing. Delaying not implemented.']),\r
+ fail.\r
+\r
+% ith(L,E,I,I0) is true if E is the Ith element of list L, starting to\r
+% count from I0\r
+ith([],_,_,_) :-\r
+ throw(outofrange).\r
+ith([H|_],H,I,I) :- !.\r
+ith([_|T],E,I,I0) :-\r
+ I>I0, !,\r
+ I1 is I0+1,\r
+ ith(T,E,I,I1).\r
+ith(_,_,_,_) :-\r
+ throw(outofrange).\r
+\r
+idmember(A,[A1|_]) :- A==A1,!.\r
+idmember(A,[_|L]) :- idmember(A,L).\r
+\r
+mynumbervars(Term, From, To) :-\r
+ numbervars(Term, From, To, [attvar(bind)]).\r
+\r
+issorted([]).\r
+issorted([_]).\r
+issorted([E1,E2|R]) :-\r
+ E1 @< E2,\r
+ issorted([E2|R]).\r
+\r
+check_sorted(L) :-\r
+ issorted(L),!.\r
+check_sorted(L) :-\r
+ write_all(['Warning: not sorted: ',L]).\r
+\r
+% Run "start" at initialization\r
+:- initialization(start).
\ No newline at end of file
repositories / ker2014-2.git / commitdiff