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