1:- module(icl, [on_icl_read/1,
    2          explain/1, explain/2, explain/3,
    3          op(1060, xfy, '&'),
    4          op(900,fy, ~),
    5          op(700,xfx, \=),
    6           op(1150, xfx, <- ),
    7           op(0, fx, (table) ) ]).    8% this is both a latex file and a Sicstus Prolog file.
    9% just compile it in Prolog or Latex it.
   10% the only difference is that the Latex version comments out the following
   11% line:  (i.e., the latex vesion starts with "%/*" and the prolog has "/*")
   12/*
   13\documentclass[11pt,fleqn]{article}
   14
   15%\usepackage[LY1]{fontenc}           % for Y&Y tex
   16%\usepackage[mtbold,LY1]{mathtime}   % for Y&Y tex
   17
   18\usepackage{times,latexsym,makeidx}
   19\pagestyle{myheadings}
   20\markright{ICL interpreter --- Version 0.2.1}
   21\makeindex
   22
   23\newcommand{\btt}{\ttfamily\bfseries}
   24
   25\title{Independent Choice Logic Interpreter\\Version 0.2.1
   26\\PROLOG CODE\thanks{Copyright \copyright 1998 David Poole. All rights
   27reserved.}}
   28\author{David Poole\\
   29Department of Computer Science,\\
   30University of British Columbia,\\
   312366 Main Mall,\\
   32Vancouver, B.C. Canada V6T 1Z4\\
   33Phone: (604) 822-6254\\
   34Fax: (604) 822-5485\\
   35Email: {\ttfamily poole@cs.ubc.ca}\\
   36URL: {\ttfamily http://www.cs.ubc.ca/spider/poole}}
   37\begin{document}
   38\maketitle
   39\begin{abstract}
   40This paper gives the code for a simple independent choice logic
   41\cite{Poole97b,Poole98a} interpreter. This is based on a naive Prolog
   42search (rather than some best first, or iterative deepening search).
   43
   44It includes negation as failure,
   45controllables (although is a very limited form --- they are
   46not chosen, but the user can control them), and debugging facilities
   47(including tracing, traversing proof trees, and automatic detection
   48of non-disjoint rules).
   49
   50This is experimental code. It is written to let us explore with
   51ideas. I make no warranty as to its suitability for anything. Use at
   52your own risk.
   53\end{abstract}
   54\newpage
   55\section{Syntax} \label{vocabulary}
   56The following commands can be used in a file or
   57as a user command to the prolog prompt. Note that all commands end with a period.
   58\begin{description}
   59\item[{\btt rule$(R)$.}]
   60The facts are
   61given in the form of {\ttfamily rule($R$)}, where $R$ is either a rule of
   62the form {\ttfamily H :- B} or is just an atom (similar to the use of
   63$clause$ in many Prolog systems). $B$ is a body made up of {\ttfamily
   64true}, atoms, conjunctions (using ``\verb|&|''), disjunctions (using
   65``\verb|;|'') and negations (using ``\verb|~|''). This code assumes
   66that rules are disjoint. 
   67\item[{\ttfamily $H$ <- $B$.}] is the same as {\ttfamily rule((H :-
   68B))}. Rules with empty 
   69bodies (facts) must be written as {\ttfamily H <- true.} or as
   70{\ttfamily rule(H).} 
   71\item[{\btt random$([h_1:p_1,\cdots,h_n:p_n])$.}]declares
   72the $h_i$ to be pairwise disjoint hypotheses, with $P(h_i)=p_i$. 
   73\item[{\btt random$(X,h,[x_1:p_1,\cdots,x_n:p_n])$.}]
   74where $h$ is an atom that contains variable $X$, and the $x_1$ are
   75different terms, declares the atoms $h$ with $X$ replaced by each
   76$x_i$ to be pairwise disjoint hypotheses with $P(h[x_i])=p_i$.
   77\item[{\btt controllable$([h_1,\cdots,h_n])$.}]declares
   78the $h_i$ to be pairwise disjoint controllable variables (i.e., the
   79agent can choose one of the $h_i$.)
   80\end{description}
   81
   82The following commands can be used as
   83user commands to the prolog prompt:
   84\begin{description}
   85\item[{\btt explain$(G,C)$.}] asks to find all explanations of $G$
   86given controllables $C$.
   87\item[{\btt thconsult$(\hbox{\em filename})$.}] loads a file called
   88{\em filename}. This does not erase any definitions in the database.
   89\item[{\btt tracing(F).}] sets tracing to have status $F$ which is
   90one of {\ttfamily \{yes,no,duals\}}. {\ttfamily duals} traces only the
   91duals (i.e., the explanations of the negation of an atom).
   92\item[{\btt debug(F).}] sets debugging to have status $F$ which is
   93one of {\ttfamily \{yes,no\}}. This lets you choose which rules get
   94selected, so you can pinpoint missing cluases (i.e., when an answer
   95wasn't returned).
   96\item[{\btt help.}] gives a list of commands.
   97\item[{\btt how$(G,C,N)$.}]
   98is used to explain the $N$th explanation of $G$ given $C$. Called
   99after {\ttfamily explain$(G,C)$.}
  100\item[{\btt diff$(G,C,N,M)$.}] 
  101prints the differences in the proof tree for the $N$th and $M$th
  102explanation of $G$ given $C$. Called after {\ttfamily explain$(G,C)$}.
  103\item[{\btt check$(G)$.}] 
  104checks for disjoint rules in the explanations of $G$.
  105 Called after {\ttfamily explain$(G,C)$.}.
  106\item[{\btt check\_disj$(G_1,G_2)$.}] 
  107checks for cases in which $G_1$ and $G_2$ are both true.
  108 Called after {\ttfamily explain$(G_1,C)$} and {\ttfamily explain$(G_2,C)$}.
  109\item[{\btt recap$(G).$}] 
  110recaps the explanations of $G$, with posterior probabilities of each
  111 explanation (i.e., given $G$). 
  112 Called after {\ttfamily explain$(G,C)$}.
  113\item[{\btt recap.}] 
  114gives the prior probabilities of every goal explained.
  115\item[{\btt check\_undef.}] checks for undefined atoms --- those atoms
  116in the body of rules for which there is no corresponding definition.
  117\item[{\btt clear.}] clears the knowledge base. This should be done before reloading clauses.
  118\end{description}
  119
  120\section{Code}
  121\subsection{Operators}
  122The ``if'' operator is written as ``{\ttfamily <-}''.  In bodies,
  123conjunction is represented as ``{\ttfamily \&}'', disjunction as ``{\ttfamily
  124;}'', negation as failure as ``\verb|~|'', and inequality as
  125``\verb|\=|.
  126\begin{verbatim} */
  127:- op(1060, xfy, '&').  128:- op(900,fy, ~).  129:- op(700,xfx, \=).  130:- op(1150, xfx, <- ).  131/* \end{verbatim}
  132The following declare the predicates that are used to store the
  133object-level knowledge base.
  134\begin{verbatim} */
  135:- dynamic rul/2.  136:- dynamic control/1.  137:- dynamic hypothesis/2.  138:- dynamic nogood/2.  139:- dynamic example_query/1.  140
  141/* \end{verbatim}
  142   
  143\subsection{Clearing the knowledge base}
  144\index{clear}
  145\begin{verbatim} */
  146clear :-
  147   retractall(rul(_,_)),
  148   retractall(control(_)),
  149   retractall(hypothesis(_,_)),
  150   retractall(nogood(_,_)),
  151   retractall(done(_,_,_,_,_)).
  152/* \end{verbatim}
  153
  154\subsection{Declaring Rules}
  155
  156$rule(R)$ where $R$ is the form of a Prolog rule. This asserts the
  157rule produced. 
  158
  159{\ttfamily h <- b} is the same as $rule(h,b)$.
  160
  161\index{rule}
  162\begin{verbatim} */
  163(H <- B) :- rule((H :- B)).
  164
  165rule(H) :- expand_rule_term(H,HH), H \=@=HH, !, rule(HH).
  166rule((H :- B)) :- !,
  167   assert_if_new(rul(H,B)).
  168rule(H) :-
  169   assert_if_new(rul(H,true)).
  170
  171expand_rule_term(H,HH):- expand_term(H,HH), !.
  172/* \end{verbatim}
  173
  174$lemma(G)$ is here to make the program upwardly compatible with the
  175version that includes lemmata. The declaration is ignored here.
  176
  177\index{rule}
  178\begin{verbatim} */
  179lemma(_).
  180/* \end{verbatim}
  181
  182\subsection{Declaring Hypotheses}
  183
  184\[\hbox{\ttfamily random}([h_1:p_1,\cdots,h_n:p_n]).\]
  185declares the $h_i$ to be pairwise disjoint hypotheses, with $P(h_i)=p_i$.
  186It should be the case that 
  187\[\sum_{i=1}^n p_i = 1\]
  188
  189This asserts $hypothesis(h_i,p_i)$ for each $i$ and asserts
  190$ngood(h_i,h_j)$ for each $i \neq j$.
  191
  192\index{random}
  193\begin{verbatim} */
  194:- op(  500, xfx,  : ).  195:- dynamic hypothesis/2.  196random(L) :-
  197   probsum(L,T),
  198   randomt(L,T).
  199probsum([],0).
  200probsum([_:P|R],P1) :-
  201   probsum(R,P0),
  202   P1 is P0+P.
  203randomt([],_).
  204randomt([H:P|R],T) :-
  205   NP is P/T,
  206   assertz(hypothesis(H,NP)),
  207   make_hyp_disjoint(H,R),
  208   randomt(R,T).
  209
  210time_arg(P, N):- 
  211  functor(P, F,_),
  212  assertz(is_time_arg(F,N)).
  213 
  214/* \end{verbatim}
  215\index{make\_disjoint}
  216\begin{verbatim} */
  217make_hyp_disjoint(_,[]).
  218make_hyp_disjoint(H,[H2 : _ | R]) :-
  219   asserta(nogood(H,H2)),
  220   asserta(nogood(H2,H)),
  221   make_hyp_disjoint(H,R).
  222/* \end{verbatim}
  223
  224\[\hbox{\ttfamily random}(X,h,[x_1:p_1,\cdots,x_n:p_n]).\]
  225where $X$ is a variable and $h$ is an atom that contains $X$ free, and the $x_1$ are different terms, is an abbreviation for
  226\[\hbox{\ttfamily random}([h[X \leftarrow x_1]:p_1,\cdots,h[X \leftarrow x_n]:p_n]).\]
  227Where $h[X \leftarrow x_1]$ is the atom $h$ with $X$ replaced by $x_i$.
  228\index{random}
  229\begin{verbatim} */
  230random(X,H,L) :-
  231   repvar(X,X1,H,H1),
  232   asserta((nogood(H,H1) :- dif(X,X1))),
  233   probsum(L,T),
  234   random_each(X,H,L,T).
  235random_each(_,_,[],_).
  236random_each(X,H,[X:P|_],T) :-
  237   NP is P/T,
  238   asserta(hypothesis(H,NP)),
  239   fail.
  240random_each(X,H,[_|R],T) :-
  241   random_each(X,H,R,T).
  242/* \end{verbatim}
  243
  244
  245
  246\[\hbox{\ttfamily controllable}([h_1,\cdots,h_n]).\]
  247declares the $h_i$ to be pairwise disjoint controllable hypotheses.
  248
  249This asserts $control(h_i)$ for each $i$ and asserts
  250$ngood(h_i,h_j)$ for each $i \neq j$.
  251
  252\index{disjoint}
  253\begin{verbatim} */
  254:- op(  500, xfx,  : ).  255controllable([]).
  256controllable([H|R]) :-
  257   asserta(control(H)),
  258   make_cont_disjoint(H,R),
  259   controllable(R).
  260/* \end{verbatim}
  261\index{make\_cont\_disjoint}
  262\begin{verbatim} */
  263make_cont_disjoint(_,[]).
  264make_cont_disjoint(H,[H2 | R]) :-
  265   asserta(nogood(H,H2)),
  266   asserta(nogood(H2,H)),
  267   make_cont_disjoint(H,R).
  268/* \end{verbatim}
  269
  270\section{The Internals of the Interpreter}
  271\subsection{Meta-interpreter}
  272The meta-interpreter is implemented using the relation:
  273\[prove(G,C0,C1,R0,R1,P0,P1,T)\]
  274where
  275\begin{description}
  276\item $G$ is the goal to be proved.
  277\item $R1-R0$ is a difference list of random assumptions to prove $G$.
  278\item $C1-C0$ is a difference list of controllable assumptions to prove $G$.
  279\item $P0$ is the probability of $R0$, $P1$ is the probability of $R1$.
  280\item $T$ is the returned proof tree.
  281\end{description}
  282The first rules defining $prove$ are the special purpose rules
  283for commands that are defined in the system.
  284\index{prove}
  285\begin{verbatim} */
  286prove(ans(A),C,C,R,R,P,P,ans(A)) :- !,
  287   ans(A,C,R, _R , P, _T).
  288prove(report_cp,C,C,R,R,P,P,_) :- !,
  289   report_cp(C,R,P).
  290prove(report_evidence,C,C,R,R,P,P,_) :- !,
  291   report_evidence(C,R,P).
  292/* \end{verbatim}
  293
  294The remaining rules are the real definition
  295\begin{verbatim} */
  296prove(true,C,C,R,R,P,P,true) :- !.
  297prove((A & B),C0,C2,R0,R2,P0,P2,(AT & BT)) :- !,
  298   prove(A,C0,C1,R0,R1,P0,P1,AT),
  299   prove(B,C1,C2,R1,R2,P1,P2,BT).
  300prove((A ; _),C0,C2,R0,R2,P0,P2,AT) :-
  301   prove(A,C0,C2,R0,R2,P0,P2,AT).
  302prove((_ ; B),C0,C2,R0,R2,P0,P2,BT) :-
  303   prove(B,C0,C2,R0,R2,P0,P2,BT).
  304prove((~ G),C0,C0,R0,R2,P0,P3,if(G,not)) :-
  305   findall(R2,prove(G,C0,_,R0,R2,P0,_,_), ExpG),
  306   duals(ExpG,R0,[exp(R0,P0)],ADs),
  307   make_disjoint(ADs,MDs),
  308   ( (tracn(yes); tracn(duals)) -> 
  309        writeln(['   Proved ~ ',G ,', assuming ',R0,'.']) ,
  310        writeln(['     explanations of ',G,': ',ExpG]),
  311        writeln(['     duals: ',ADs]),
  312        writeln(['     disjointed duals: ',MDs])
  313     ; true),!,
  314   member(exp(R2,P3),MDs).
  315prove(H,_,_,R,_,P,_,_) :-
  316   tracn(yes),
  317   writeln(['Proving: ',H,' assuming: ',R,' prob=',P]),
  318   fail.
  319prove(H,C,C,R,R,P,P,if(H,assumed)) :-
  320   hypothesis(H,_),
  321   member(H,R),
  322   ( tracn(yes) 
  323     -> writeln(['   Already assumed: ',H ,'.']) 
  324    ; true).
  325prove(H,C,C,R,[H|R],P0,P1,if(H,assumed)) :-
  326   hypothesis(H,PH),
  327   \+ member(H,R),
  328   PH > 0,
  329   good(H,R),
  330   P1 is P0*PH,
  331   ( tracn(yes) -> writeln(['   Assuming: ',H ,'.']) ; true).
  332prove(H,C,C,R,R,P,P,if(H,given)) :- 
  333   control(H),member(H,C),!,
  334   ( tracn(yes) -> writeln(['   Given: ',H,'.']) ; true).
  335prove(H,C,C,R,R,P,P,if(H,builtin)) :- 
  336   builtin(H), call(H).
  337prove(A \= B,C,C,R,R,P,P,if(A \= B,builtin)) :- 
  338   dif(A,B).
  339prove(G,C0,C1,R0,R1,P0,P1,if(G,BT)) :-
  340   rul(G,B),
  341   ( tracn(yes) -> 
  342     writeln(['   Using rule: ',G ,' <- ',B,'.']) 
  343   ; true),
  344   ( debgn(yes) -> deb(G,B) ; true),
  345   tprove(G,B,C0,C1,R0,R1,P0,P1,BT),
  346   ( tracn(yes) -> 
  347     writeln(['   Proved: ',G ,' assuming ',R1,'.']) 
  348     ; true).
  349prove(H,_,_,R,_,P,_,_) :-
  350   tracn(yes),
  351   writeln(['Failed: ',H,' assuming: ',R,' prob=',P]), 
  352   fail.
  353tprove(_,B,C0,C1,R0,R1,P0,P1,BT) :-
  354   prove(B,C0,C1,R0,R1,P0,P1,BT).
  355tprove(G,_,_,_,R,_,P,_,_) :-
  356   tracn(yes),
  357   writeln([' Retrying: ',G,' assuming: ',R,' prob=',P]),
  358   fail.
  359/* \end{verbatim}
  360
  361We allow many built in relations to be evaluated directly by Prolog.
  362\index{builtin}
  363\begin{verbatim} */
  364:- dynamic builtin/1.  365%:- multifile builtin/1.
  366builtin((_ is _)).
  367builtin((_ < _)).
  368builtin((_ > _)).
  369builtin((_ =< _)).
  370builtin((_ >= _)).
  371builtin((_ = _)).
  372builtin((user_help)).
  373
  374
  375/* \end{verbatim}
  376
  377\begin{verbatim} */
  378deb(G,B) :-
  379   writeln([' Use rule: ',G ,' <- ',B,'? [y, n or off]']),
  380   read(A),
  381  ( A = y -> true ;
  382    A = n -> fail ;
  383    A = off -> debug(off) ;
  384    true -> writeln(['y= use this rule, n= use another rule, off=debugging off']) ,
  385       deb(G,B)
  386   ).
  387
  388/* \end{verbatim}
  389\subsection{Negation}
  390\[duals(Es,R0,D0,D1)\]
  391is true if $Es$ is a list of composite choices (all of whose tail is
  392$R0$), and $D1-D2$ is a list of $exp(R1,P1)$ such that $R1-R0$ is a
  393hitting set of negations of $Es$.
  394\index{dual}
  395\begin{verbatim} */
  396duals([],_,D,D).
  397duals([S|L],R0,D0,D2) :-
  398   split_each(S,R0,D0,[],D1),
  399   duals(L,R0,D1,D2).
  400/* \end{verbatim}
  401
  402\[split\_each(S,R0,D0,D,D1)\]
  403is true if $S$ is a composite choice (with tail $R0$), and
  404$D2$ is $D$ together with the hitting set of negations of $D0$.
  405\index{split\_each}
  406\begin{verbatim} */
  407split_each(R0,R0,_,D0,D0) :- !.
  408split_each([A|R],R0,D0,PDs,D2) :-
  409   negs(A,NA),
  410   add_to_each(A,NA,D0,PDs,D1),
  411   split_each(R,R0,D0,D1,D2).
  412/* \end{verbatim}
  413
  414\[add\_to\_each(S,R0,D0,D,D1)\]
  415is true if $S$ is a composite choice (with tail $R0$), and
  416$D2$ is $D$ together with the hitting set of negations of $D0$.
  417\index{add\_to\_each}
  418\begin{verbatim} */
  419add_to_each(_,_,[],D,D).
  420add_to_each(A,NA,[exp(E,_)|T],D0,D1) :-
  421   member(A,E),!,
  422   add_to_each(A,NA,T,D0,D1).
  423add_to_each(A,NA,[exp(E,PE)|T],D0,D2) :-
  424   bad(A,E),!,
  425   insert_exp(exp(E,PE),D0,D1),
  426   add_to_each(A,NA,T,D1,D2).
  427add_to_each(A,NA,[B|T],D0,D2) :-
  428   ins_negs(NA,B,D0,D1),
  429   add_to_each(A,NA,T,D1,D2).
  430/* \end{verbatim}
  431
  432\[ins\_negs(NA,B,D0,D1)\]
  433is true if adding the elements of $NA$ to composite choice $B$, and
  434adding these to $D0$ produces $D1$.
  435\index{ins\_negs}
  436\begin{verbatim} */
  437ins_negs([],_,D0,D0).
  438ins_negs([N|NA],exp(E,PE),D,D2) :-
  439   hypothesis(N,PN),
  440   P is PN * PE,
  441   insert_exp(exp([N|E],P),D,D1),
  442   ins_negs(NA,exp(E,PE),D1,D2).
  443/* \end{verbatim}
  444
  445\[insert\_exp(E,L0,L1)\]
  446is true if inserting composite choice $E$ into list $L0$ 
  447produces list $L1$. Subsumed elements are removed.
  448\index{insert\_exp}
  449\begin{verbatim} */
  450insert_exp(exp(_,0.0),L,L) :-!.
  451insert_exp(E,[],[E]) :- !.
  452insert_exp(exp(E,_),D,D) :-
  453   member(exp(E1,_),D),
  454   subset(E1,E),!.
  455insert_exp(exp(E,P),[exp(E1,_)|D0],D1) :-
  456   subset(E,E1),!,
  457   insert_exp(exp(E,P),D0,D1).
  458insert_exp(exp(E,P),[E1|D0],[E1|D1]) :-
  459   insert_exp(exp(E,P),D0,D1).
  460/* \end{verbatim}
  461
  462\subsection{Making Composite Choices Disjoint}
  463
  464\[make\_disjoint(L,SL)\]
  465is true if $L$ and $SL$ are lists of the form $exp(R,P)$, such that
  466$L1$ is a subset of $L$ containing minimal elements with minimal
  467$R$-values.
  468\index{ins\_neg}
  469\begin{verbatim} */
  470make_disjoint([],[]).
  471make_disjoint([exp(R,P)|L],L2) :-
  472   member(exp(R1,_),L),
  473   \+ incompatible(R,R1),!,
  474   member(E,R1), \+ member(E,R),!,
  475   negs(E,NE),
  476   split(exp(R,P),NE,E,L,L1),
  477   make_disjoint(L1,L2).
  478make_disjoint([E|L1],[E|L2]) :-
  479   make_disjoint(L1,L2).
  480split(exp(R,P),[],E,L,L1) :-
  481   hypothesis(E,PE),
  482   P1 is P*PE,
  483   insert_exp1(exp([E|R],P1),L,L1).
  484split(exp(R,P),[E1|LE],E,L,L2) :-
  485   hypothesis(E1,PE),
  486   P1 is P*PE,
  487   split(exp(R,P),LE,E,L,L1),
  488   insert_exp1(exp([E1|R],P1),L1,L2).
  489negs(E,NE) :-
  490   findall(N,nogood(E,N),NE).
  491insert_exp1(exp(_,0.0),L,L) :-!.
  492insert_exp1(exp(E,_),D,D) :-
  493   member(exp(E1,_),D),
  494   subset(E1,E),!.
  495insert_exp1(exp(E,P),D,[exp(E,P)|D]).
  496/* \end{verbatim}
  497
  498\subsection{Nogoods}
  499We assume three relations for handling $nogoods$:
  500\[good(A,L)\]
  501fails if $[A|L]$ has a subset that has been declared nogood. We can
  502assume that no subset of $L$ is nogood (this allows us to more
  503efficiently index nogoods).
  504\[allgood(L)\]
  505fails if $L$ has a subset that has been declared nogood.
  506\index{good}
  507\begin{verbatim} */
  508allgood([]).
  509allgood([H|T]) :-
  510   good(H,T),
  511   allgood(T).
  512
  513good(A,T) :-
  514   \+ ( makeground((A,T)), bad(A,T)).
  515bad(A,[B|_]) :-
  516   nogood(A,B).
  517bad(A,[_|R]) :-
  518   bad(A,R).
  519/* \end{verbatim}
  520
  521
  522\subsection{Explaining}
  523To find an explanation for a subgoal $G$ given controllables $C$ and
  524building on random assumables $R$, we do
  525an $explain(G,C,R)$. Both $R$ and $C$ are optional.
  526\index{explain}
  527\begin{verbatim} */
  528:- dynamic done/4.  529explain(G) :-
  530   explain(G,[],[]).
  531explain(G,C) :-
  532   explain(G,C,[]).
  533explain(G,C,R) :-
  534   statistics(runtime,_),
  535   ex(G,C,R).
  536:- dynamic false/6.  537/* \end{verbatim}
  538
  539$ex(G,C,R)$ tries to prove $G$ with controllables $C$ and random
  540assumptions $R$. It repeatedly proves $G$, calling $ans$ for each
  541successful proof.
  542\index{ex}
  543\index{ans}
  544\begin{verbatim} */
  545:- dynamic done/5.  546ex(G,C,R0) :- 
  547   prove(G,C,_,R0,R,1,P,T), 
  548   ans(G,C,R0,R,P,T), fail.
  549ex(G,C,R) :-
  550   done(G,C,R,_,Pr),
  551   append(C,R,CR),
  552   nl,
  553   writeln(['Prob( ',G,' | ',CR,' ) = ',Pr]),
  554   statistics(runtime,[_,Time]),
  555   writeln(['Runtime: ',Time,' msec.']).
  556ex(G,C,R) :-
  557   \+ done(G,C,R,_,_),
  558   append(C,R,CR),
  559   nl,
  560   writeln(['Prob( ',G,' | ',CR,' ) = ',0.0]),
  561   statistics(runtime,[_,Time]),
  562   writeln(['Runtime: ',Time,' msec.']).
  563
  564ans(G,C,R0,R,P,T) :-
  565   allgood(R),
  566   ( retract(done(G,C,R0,Done,DC))
  567     -> true
  568     ; Done=[], DC=0),
  569   DC1 is DC+P,
  570   asserta(done(G,C,R0,[expl(R,P,T)|Done],DC1)),
  571   nl,
  572   length(Done,L),
  573   append(C,R0,Given),
  574   writeln(['***** Explanation ',L,' of ',G,' given ',Given,':']),
  575   writeln([R]),
  576   writeln(['Prior = ',P]).
  577/* \end{verbatim}
  578
  579$recap$ is used to give a list of all conditional probabilities computed.
  580\index{ans}
  581\begin{verbatim} */
  582recap :-
  583   done(G,C,R,_,Pr),
  584   append(C,R,CR),
  585   writeln(['Prob( ',G,' | ',CR,' ) = ',Pr]),
  586   fail.
  587recap.
  588recap(G) :-
  589   recap(G,_,_).
  590recap(G,C) :-
  591   recap(G,C,_).
  592recap(G,C,R) :-
  593   done(G,C,R,Expls,Pr),
  594   append(C,R,CR),
  595   writeln(['Prob( ',G,' | ',CR,' ) = ',Pr]),
  596   writeln(['Explanations:']),
  597   recap_each(_,Expls,Pr).
  598recap_each(0,[],_).
  599recap_each(N,[expl(R,P,_)|L],Pr) :-
  600   recap_each(N0,L,Pr),
  601   N is N0+1,
  602   PP is P/Pr,
  603   writeln([N0,': ',R,' Post Prob=',PP]).
  604   
  605/* \end{verbatim}
  606
  607\section{Debugging}
  608\subsection{Help}
  609\begin{verbatim} */
  610:- (h <- user_help).  611user_help :- writeln([
  612'rule(R).','
  613  asserts either a rule of the form H :- B or an atom.','
  614H <- B. ','
  615   is the same as rule((H :- B)). ','
  616   Rules with empty bodies (facts) must be written as H <- true. or as rule(H).','
  617random([h1:p1,...,hn:pn]).','
  618   declares the hi to be pairwise disjoint hypotheses, with P(hi)=pi. ','
  619random(X,h,[x1:p1,...,xn:pn]).','
  620   declares h[X/xi] to be pairwise disjoint hypotheses with P(h[X/xi])=pi.','
  621controllable([h1,...,hn]).','
  622   declares the hi to be pairwise disjoint controllable variables.','
  623explain(G,C). ','
  624   finds explanations of G given list of controlling values C.','
  625how(G,C,R,N).','
  626   is used to explain the Nth explanation of G given controllables C,','
  627   and randoms R.',' 
  628diff(G,C,N,M) ','
  629   prints difference in the proof tree for the Nth and Mth explanation','
  630   of G given C.','
  631check(G,C).','
  632   checks for disjoint rules in the explanations of G given C.','
  633recap(G). ','
  634   recaps the explanations of G, with posterior probabilities (given G).','
  635recap. ','
  636   gives the prior probabilities of everything explained.','
  637thconsult(filename). ','
  638   loads a file called filename. ','
  639tracing(F). ','
  640    sets tracing to have status F which is one of {yes,no,duals}.','
  641debug(F). ','
  642    sets debugging to have status F which is one of {yes,no}.','
  643check_undef.','
  644    checks for undefined atoms in the body of rules.','
  645clear.','
  646    clears the knowedge base. Do this before reloading.','
  647    Reconsulting a program will not remove old clauses and declarations.','
  648help.','
  649    print this message.']).
  650/* \end{verbatim}
  651
  652\subsection{Tracing}
  653Tracing is used to trace the details of the search tree. It is ugly
  654except for very small programs.
  655\index{tracing}
  656\begin{verbatim} */
  657:- dynamic tracn/1.  658tracing(V) :-
  659   member(V,[yes,no,duals]),!,
  660   retractall(tracn(_)),
  661   asserta(tracn(V)).
  662tracing(V) :-
  663   member(V,[on,y]),!,
  664   retractall(tracn(_)),
  665   asserta(tracn(yes)).
  666tracing(V) :-
  667   member(V,[off,n]),!,
  668   retractall(tracn(_)),
  669   asserta(tracn(no)).
  670tracing(_) :-
  671   writeln(['Argument to tracing should be in {yes,no,duals}.']),
  672   !,
  673   fail.
  674tracn(no).
  675% user_help :- unix(shell('more help')).
  676
  677/* \end{verbatim}
  678\subsection{Debugging}
  679Debugging is useful for determining why a program failed.
  680\begin{verbatim} */
  681:- dynamic debgn/1.  682debgn(no).
  683
  684debug(V) :-
  685   member(V,[yes,on,y]),!,
  686   retractall(debgn(_)),
  687   assert(debgn(yes)).
  688debug(V) :-
  689   member(V,[no,off,n]),!,
  690   retractall(debgn(_)),
  691   assert(debgn(no)).
  692debug(_) :-
  693   writeln(['Argument to debug should be in {yes,no}.']), !, fail.
  694/* \end{verbatim}
  695
  696\subsection{How was a goal proved?}
  697The programs in this section are used to explore how proofs were generated.
  698\[how(G,C,R,N)\]
  699is used to explain the $N$th explanation of $G$ given controllables
  700$C$, and randoms $R$. $R$ and $C$ are optional.
  701
  702\index{how}
  703\begin{verbatim} */
  704how(G,N) :-
  705   how(G,[],[],N).
  706how(G,C,N) :-
  707   how(G,C,[],N).
  708how(G,C,R,N) :-
  709   tree(G,C,R,N,T),
  710   traverse(T).
  711/* \end{verbatim}
  712
  713\[tree(G,C,R,N,NT)\]
  714is true if $NT$ is the proof tree for the $N$th explanation of $G$ given $C\wedge R$.
  715
  716\index{tree}
  717\begin{verbatim} */
  718tree(G,C,R,N,NT) :-
  719   done(G,C,R,Done,_),
  720   nthT(Done,N,NT).
  721
  722nthT([expl(_,_,T) |R],N,T) :-
  723   length(R,N),!.
  724nthT([_|R],N,T) :-
  725   nthT(R,N,T).
  726/* \end{verbatim}
  727
  728\[traverse(T)\] 
  729is true if T is a tree being traversed.
  730\index{traverse}
  731\begin{verbatim} */
  732traverse(if(H,true)) :-
  733    writeln([H,' is a fact']).
  734traverse(if(H,builtin)) :-
  735    writeln([H,' is built-in.']).
  736traverse(if(H,assumed)) :-
  737    writeln([H,' is assumed.']).
  738traverse(if(H,given)) :-
  739    writeln([H,' is a given controllable.']).
  740traverse(if(H,not)) :-
  741    writeln([~ H,' is a negation - I cannot trace it. Sorry.']).
  742traverse(if(H,B)) :-
  743    B \== true,
  744    B \== builtin,
  745    B \== assumed,
  746    B \== given,
  747    writeln([H,' :-']),
  748    printbody(B,1,Max),
  749    read(Comm),
  750    interpretcommand(Comm,B,Max,if(H,B)).
  751/* \end{verbatim}
  752
  753\[printbody(B,N)\]
  754is true if B is a body to be printed and N is the 
  755count of atoms before B was called (this assumes that ``{\ttfamily \&}'' is 
  756left-associative).
  757
  758\index{printbody}
  759\begin{verbatim} */
  760printbody((A&B),N,N2) :-
  761   printbody(A,N,N),
  762   N1 is N+1,
  763   printbody(B,N1,N2).
  764printbody(if(H,not),N,N) :-!,
  765   writeln(['   ',N,': ~ ',H]).
  766printbody(if(H,_),N,N) :-
  767   writeln(['   ',N,': ',H]).
  768printbody(true,N,N):-!,
  769   writeln(['   ',N,': true ']).
  770printbody(builtin,N,N):-!,
  771   writeln(['   ',N,': built in ']).
  772printbody(assumed,N,N):-!,
  773   writeln(['   ',N,': assumed ']).
  774printbody(given,N,N):-!,
  775   writeln(['   ',N,': given ']).
  776/* \end{verbatim}
  777
  778\[interpretcommand(Comm,B)\]
  779interprets the command $Comm$ on body $B$.
  780\index{interpretcommand}
  781\begin{verbatim} */
  782interpretcommand(N,B,Max,G) :-
  783   integer(N),
  784   N > 0,
  785   N =< Max,
  786   nth(B,N,E),
  787   traverse(E),
  788   traverse(G).
  789interpretcommand(up,_,_,_).
  790interpretcommand(N,_,Max,G) :-
  791   integer(N),
  792   (N < 1 ; N > Max),
  793   writeln(['Number out of range: ',N]),
  794   traverse(G).
  795interpretcommand(help,_,_,G) :-
  796   writeln(['Give either a number, up or exit. End command with a Period.']),
  797   traverse(G).
  798interpretcommand(C,_,_,G) :-
  799   \+ integer(C),
  800   C \== up,
  801   C \== help,
  802   C \== exit,
  803   C \== end_of_file,
  804   writeln(['Illegal Command: ',C,'   Type "help." for help.']),
  805   traverse(G).
  806
  807% nth(S,N,E) is true if E is the N-th element of conjunction S
  808nth(A,1,A) :-
  809   \+ (A = (_&_)).
  810nth((A&_),1,A).
  811nth((_&B),N,E) :-
  812   N>1,
  813   N1 is N-1,
  814   nth(B,N1,E).
  815/* \end{verbatim}
  816
  817\subsection{Diff}
  818\[diff(G,C,N,M)\] \index{diff}
  819prints the differences in the proof tree for the $N$th and $M$th
  820explanation of $G$ given $C$. 
  821
  822\begin{verbatim} */
  823diff(G,C,N,M) :-
  824   tree(G,C,N,NT),
  825   tree(G,C,M,MT),
  826   diffT(NT,MT).
  827/* \end{verbatim}
  828
  829\[diffT(T1,T2)\] 
  830prints the differences in the proof trees $T1$ and $T2$.
  831\begin{verbatim} */
  832diffT(T,T) :-
  833   writeln(['Trees are identical']).
  834
  835diffT(if(H,B1),if(H,B2)) :-
  836   immdiff(B1,B2),!,
  837   writeln([H,' :-']),
  838   printbody(B1,1,N1),
  839   writeln([H,' :-']),
  840   printbody(B2,N1,_).
  841diffT(if(H,B1),if(H,B2)) :-
  842   diffT(B1,B2).
  843diffT((X&Y),(X&Z)) :- !,
  844   diffT(Y,Z).
  845diffT((X&_),(Y&_)) :-
  846   diffT(X,Y).
  847
  848immdiff((A&_),(B&_)) :-
  849   immdiff(A,B).
  850immdiff((_&A),(_&B)) :-
  851   immdiff(A,B).
  852immdiff((_&_),if(_,_)).
  853immdiff(if(_,_),(_&_)).
  854immdiff(if(A,_),if(B,_)) :-
  855   \+ A = B.
  856immdiff(if(_,_),B) :-
  857   atomic(B).
  858immdiff(A,if(_,_)) :-
  859   atomic(A).
  860/* \end{verbatim}
  861
  862\subsection{Check}
  863\[check(G,C,R)\]\index{check} 
  864checks the explanations of $G$ given controllables $C$ and randoms $R$ 
  865for rules which violate the disjoint
  866assumptions assumption. The two rules which are not disjoint are returned.
  867
  868\begin{verbatim} */
  869check :- 
  870   check(_,_,_).
  871check(G) :-
  872   check(G,_,_).
  873check(G,C) :-
  874   check(G,C,_).
  875check(G,C,R) :-
  876   done(G,C,R,Done,_),
  877   check_done(Done).
  878
  879check_done([expl(R1,_,T1)|D]) :-
  880   memberR(expl(R2,_,T2),D,DR),
  881   \+ incompatible(R1,R2),
  882   length(D,LD),
  883   length(DR,L2),
  884   icl_union(R1,R2,R),
  885   writeln(['Non-disjoint rules ',LD,' & ',L2,' assuming ',R]),
  886   diffT(T1,T2).
  887check_done([_|D]) :-
  888   check_done(D).
  889/* \end{verbatim}
  890
  891\subsection{Check Disjoint Explanations}
  892\[check\_disj(G0,G1)\] \index{check\_disj}
  893checks whether explanations of $G0$ and $G1$ are disjoint. This is useful when $G0$ and $G1$ should be incompatible.
  894\begin{verbatim} */
  895check_disj(G0,G1):-
  896   check_disj(G0,G1,_,_).
  897check_disj(G0,G1,C,R):-
  898   done(G0,C,R,D0,_),
  899   done(G1,C,R,D1,_),
  900   memberR(expl(R0,_,_),D0,LD0),
  901   memberR(expl(R1,_,_),D1,LD1),
  902   \+ incompatible(R0,R1),
  903   length(LD0,L0),
  904   length(LD1,L1),
  905   append(C,R,CR),
  906   writeln(['Explanation ',L0,' of ',G0,' and ',L1,' of ',G1,
  907       ', given ',CR,' are compatible assuming:']),
  908   icl_union(R0,R1,R),
  909   writeln([R]).
  910incompatible(R1,R2) :-
  911   member(A1,R1),
  912   member(A2,R2),
  913   nogood(A1,A2).
  914/* \end{verbatim}
  915
  916\subsection{Checking for undefined atoms}
  917$check_undef$ searches through the knowledge base looking for a rule
  918containing an atom in the body which doesn't have a corresponding
  919definition (i.e., a clause with it at the head, or an atomic choice).
  920\begin{verbatim} */
  921check_undef :-
  922   forall(rul(H,B),
  923   forall(body_elt_undefined(B,H,B), true)), !.
  924
  925
  926body_elt_undefined(true,_,_) :- !,fail.
  927body_elt_undefined((A&_),H,B) :-
  928   body_elt_undefined(A,H,B).
  929body_elt_undefined((_&A),H,B) :- !,
  930   body_elt_undefined(A,H,B).
  931body_elt_undefined((~ A),H,B) :- !,
  932   body_elt_undefined(A,H,B).
  933body_elt_undefined((A;_),H,B) :-
  934   body_elt_undefined(A,H,B).
  935body_elt_undefined((_;A),H,B) :- !,
  936   body_elt_undefined(A,H,B).
  937body_elt_undefined(call(A),H,B) :- !,
  938   body_elt_undefined(A,H,B).
  939body_elt_undefined(_ \= _,_,_) :- !,fail.
  940%body_elt_undefined(A,_,_) :-
  941%   askabl(A),!,fail.
  942%body_elt_undefined(A,_,_) :-
  943%   assumabl(A),!,fail.
  944body_elt_undefined(A,_,_) :-
  945   builtin(A),!,fail.
  946body_elt_undefined(A,_,_) :-
  947   hypothesis(A,_),!,fail.
  948body_elt_undefined(A,_,_) :-
  949   control(A),!,fail.
  950body_elt_undefined(A,_,_) :-
  951   rul(A,_),!,fail.
  952body_elt_undefined(A,H,B) :-
  953   writeln(['Warning: no clauses for ',A,' in rule ',(H <- B),'.']),!,fail.
  954/* \end{verbatim}
  955
  956\section{Miscellaneous}
  957\subsection{File Handling}
  958To consult a probabilistic Horn abduction file, you should do a,
  959\begin{verse}
  960{\bf thconsult}\em (filename).
  961\end{verse}
  962The following is the definition of {\em thconsult}. Basically we just
  963keep reading the file and executing the commands in it until we stop.
  964This does not clear any previous database. If you reconsult a file you
  965will get multiple instances of clauses and this will undoubtedly screw you up.
  966\index{thconsult}
  967\begin{verbatim} */
  968thconsult(File) :-
  969   current_input(OldFile),
  970   open(File,read,Input),
  971   set_input(Input),
  972   read(T),
  973   read_all(T),
  974   set_input(OldFile),
  975   writeln(['ICL theory ',File,' consulted.']),!.
  976/* \end{verbatim}
  977\index{read\_all}
  978\begin{verbatim} */
  979read_all(end_of_file) :- !.
  980read_all(T) :-
  981   (on_icl_read(T);format('Warning: ~w failed~n',[T])),
  982   read(T2),
  983   read_all(T2).
  984
  985:- module_transparent(on_icl_read/1).  986on_icl_read(T):- notrace(T == end_of_file), !, listing(example_query/1).
  987on_icl_read(:- T):- must(T),!.
  988on_icl_read(example_query(X)):- !,assertz(example_query(X)).
  989on_icl_read(random(X)):- !, random(X). 
  990on_icl_read(T):- \+ predicate_property(icl:T, imported_from(_)), !, must(icl:T).
  991on_icl_read(T):- must(T).
  992
  993/* \end{verbatim}
  994
  995\subsection{Utility Functions}
  996\subsubsection{List Predicates}
  997$append(X,Y,Z)$ is the normal append function
  998\index{append} 
  999\begin{verbatim} */
 1000/*DMILES for SWI
 1001append([],L,L).
 1002
 1003append([H|X],Y,[H|Z]) :-
 1004   append(X,Y,Z).
 1005*/
 1006/* \end{verbatim}
 1007\index{icl_union} 
 1008\begin{verbatim} */
 1009icl_union([],L,L).
 1010
 1011icl_union([H|X],Y,Z) :-
 1012   member(H,Y),!,
 1013   icl_union(X,Y,Z).
 1014icl_union([H|X],Y,[H|Z]) :-
 1015   icl_union(X,Y,Z).
 1016/* \end{verbatim}
 1017
 1018\index{member}
 1019\begin{verbatim} */
 1020/*DMILES for SWI
 1021
 1022member(A,[A|_]).
 1023member(A,[_|R]) :-
 1024   member(A,R).
 1025*/
 1026/* \end{verbatim}
 1027\index{member}
 1028\begin{verbatim} */
 1029memberR(A,[A|R],R).
 1030memberR(A,[_|T],R) :-
 1031   memberR(A,T,R).
 1032/* \end{verbatim}
 1033\index{subset}
 1034\begin{verbatim} */
 1035subset([],_).
 1036subset([H|T],L) :-
 1037   member(H,L),
 1038   subset(T,L).
 1039/* \end{verbatim}
 1040\subsubsection{Term Management}
 1041
 1042\index{makeground}
 1043\begin{verbatim} */
 1044makeground(T) :-
 1045   numbervars(T,0,_).
 1046/* \end{verbatim}
 1047
 1048$repvar(X,X1,T,T1)$ replaces each occurrence of $X$ in $T$ by $X1$ forming $T1$.
 1049\index{copy}
 1050\begin{verbatim} */
 1051repvar(X,X1,Y,X1) :- X==Y, !.
 1052repvar(_,_,Y,Y) :- var(Y), !.
 1053repvar(_,_,Y,Y) :- ground(Y), !.
 1054repvar(X,X1,[H|T],[H1|T1]) :- !,
 1055   repvar(X,X1,H,H1),
 1056   repvar(X,X1,T,T1).
 1057repvar(X,X1,T,T1) :-
 1058   T =.. L,
 1059   repvar(X,X1,L,L1),
 1060   T1 =.. L1.
 1061/* \end{verbatim}
 1062
 1063\subsubsection{Output}
 1064\index{writeln}
 1065\begin{verbatim} */
 1066writeln([]) :- nl.
 1067writeln([H|T]) :-
 1068   write(H),
 1069   writeln(T).
 1070/* \end{verbatim}
 1071\bibliographystyle{plain}
 1072%\bibliography{/ai/poole/bib/reason.string,/ai/poole/bib/poole_local_reason,/ai/poole/bib/reason}
 1073%\bibliography{../../../book/bib/string,../../../book/bib/poole,../../../book/bib/reason}
 1074
 1075\begin{thebibliography}{1}
 1076
 1077\bibitem{Poole97b}
 1078D.~Poole.
 1079\newblock The independent choice logic for modelling multiple agents under
 1080  uncertainty.
 1081\newblock {\em Artificial Intelligence}, 94:7--56, 1997.
 1082\newblock special issue on economic principles of multi-agent systems.
 1083
 1084\bibitem{Poole98a}
 1085D.~Poole.
 1086\newblock Abducing through negation as failure: stable models in the
 1087  {Independent Choice Logic}.
 1088\newblock {\em Journal of Logic Programming}, to appear, 1998.
 1089
 1090\end{thebibliography}
 1091
 1092\printindex
 1093
 1094\end{document}
 1095*/
 1096
 1097
 1098:- include(library(dialect/logicmoo/dialect_loader_incl)). 1099
 1100prolog:dialect_reads(icl, on_icl_read)