33% :- module(nfsdl,[nnf/2, pnf/2, cf/2]).
   34
   35:- module(ec_nnf,[]).   36
   37
   38/*
   39% SWI Prolog modules do not export operators by default
   40% so they must be explicitly placed in the user namespace
   41
   42:- ( prolog_engine(swi) ->
   43     op( 400, fy, user:(box) ),	% Necessity, Always
   44     op( 400, fy, user:(dia) ),	% Possibly, Eventually
   45     op( 400, fy, user:(cir) )	% Next time
   46   ;
   47:- (
   48     op(400,fy,box),		% Necessity, Always
   49     op(400,fy,dia),	        % Possibly, Eventually
   50     op(400,fy,cir)		% Next time
   51   ).
   52*/
   53:- export(clausify_pnf/2).   54clausify_pnf(PNF, Cla):-
   55  notrace(catch(clausify_pnf1(PNF, Cla),_,fail)),!.
   56clausify_pnf(PNF, Cla):-
   57  rtrace(clausify_pnf1(PNF, Cla)),!.
   58
   59clausify_pnf1(PNF, Cla):-
   60 tolerate_elaboration(PNF,PNF0),
   61 clausify_pnf_v2(PNF0, Cla0),!,
   62 modal_cleansup(Cla0,Cla),
   63  !.
   64
   65modal_cleansup(Cla0,Cla):- 
   66   f_modal(_,Cla0,Cla1), d_modal(_,Cla1,Cla2),
   67  r_modal(_,Cla2,Cla3),r_modal(_,Cla3,Cla4),r_modal(_,Cla4,Cla),!.
   68
   69:- export(tolerate_elaboration/2).   
   70%tolerate_elaboration(I,I):-!.
   71tolerate_elaboration(I,O):-  fail,
   72 numbervars(I,0,_,[attvar(bind)]),!,
   73  tolerate_elaboration0(I,O).
   74tolerate_elaboration(I,I):-!.
   75tolerate_elaboration(I,O):- 
   76  with_vars_locked(I,tolerate_elaboration0(I,O)),!.
   77
   78tolerate_elaboration0(I,O):-   
   79  correct_common('->'(poss(I),nesc(I)),I0),
   80 % correct_common(nesc(I),I0),
   81   negations_inward(I0,O),!.
   82
   83:- export(correct_common/2).   84correct_common(I,O):- correct_modal(_,I,O),!.
   85
   86:- export(negations_inward/2).   87negations_inward(Formula, NNF):-  
   88 nnf(not(Formula), NNF ).
   89
   90:- use_module(library(logicmoo/portray_vars)).   91
   92clausify_pnf_v1( Formula, CF ):-
   93  negations_inward(Formula, NNF), 
   94    pnf( NNF, PNF ), cf( PNF, CF ),!.
   95
   96clausify_pnf_v2(PNF, ClaS):- 
   97   declare_fact(PNF),
   98   findall(saved_clauz(E,Vs),retract(saved_clauz(E,Vs)),Cla), E\==[], !,
   99   maplist(cla_to_clas,Cla,ClaS).
  100
  101cla_to_clas(saved_clauz(E,Vs),E):- maplist(to_wasvar,Vs).
  102
  103to_numbars(N=V):- ignore(V='$VAR'(N)).
  104to_wasvar(N=V):-    
  105   prolog_load_context(variable_names,VsO),
  106   (member(N=V,VsO) -> true ; debug_var(N,V)).
  107
  108var_or_atomic(Fml):- notrace(var_or_atomic0(Fml)).
  109var_or_atomic0(Fml):- \+ compound_gt(Fml,0), !.
  110var_or_atomic0('$VAR'(_)).
  111
  112non_expandable(Fml):- notrace(non_expandable0(Fml)).
  113non_expandable0(Fml):- var_or_atomic0(Fml),!.
  114non_expandable0(Fml):- arg(_,Fml,E), var(E),!.
  115
  116correct_holds(_,Fml,Fml):- var_or_atomic(Fml),!.
  117correct_holds(_,Fml,Fml):- arg(1,Fml,Var), var(Var),!.
  118correct_holds(neg, not(initially(NegP)),initially((P))):- compound(NegP),NegP=neg(P).
  119correct_holds(neg, not(initially(P)),initially(neg(P))):-!.
  120correct_holds(neg, not(holds_at(NegP,T)),holds_at((P),T)):- compound(NegP),NegP=neg(P).
  121correct_holds(neg, not(holds_at(P,T)),holds_at(neg(P),T)).
  122correct_holds(neg, not(diff(P,T)),equals(P,T)).
  123correct_holds(neg, holds_at(not(P),T),holds_at(neg(P),T)).
  124correct_holds(inward,  not(holds_at(P,T)),holds_at(not(P),T)).
  125correct_holds(outward2, holds_at(neg(P),T),not(holds_at(P,T))).
  126correct_holds(outward, holds_at(not(P),T),not(holds_at(P,T))).
  127correct_holds(IO, P,PP):-
  128  compound_name_arguments(P,F,Args),
  129  maplist(correct_holds(IO),Args,FArgs),
  130  compound_name_arguments(PP,F,FArgs).
  131
  132
  133cir_until2(next,until).
  134box_dia(always,eventually).
  135
  136box_dia((impl),(proves)).
  137box_dia(nesc,poss).
  138box_dia(will,can).
  139box_dia(knows,believes).
  140box_dia(BOX,DIA):- compound_gt(BOX, 0), !, 
  141  BOX=..[K|ARGS],
  142  box_dia(K,B), !,
  143  DIA=..[B|ARGS].
  144box_dia(BOX,DIA):- compound_gt(DIA, 0), !, 
  145  DIA=..[B|ARGS],
  146  box_dia(K,B), !,
  147  BOX=..[K|ARGS].
  148
  149aliased_rel(possibly,poss).
  150aliased_rel((~), not).
  151
  152
  153correct_modal(_,Fml,Fml):- var_or_atomic(Fml),!.
  154correct_modal(M, P, O ):- P=..[F|A], aliased_rel(F,FF),!, PP=..[FF|A], correct_modal(M, PP, O ).
  155correct_modal(M, P, box(FA,E) ):- P=..[F,A,D],box_dia(F,_),!,correct_modal(M,D,E),FA=..[F,A].
  156correct_modal(M, P, dia(FA,E) ):- P=..[F,A,D],box_dia(_,F),!,correct_modal(M,D,E),FA=..[F,A].
  157correct_modal(M, P, box(F,E) ):- P=..[F,D],box_dia(F,_),!,correct_modal(M,D,E).
  158correct_modal(M, P, dia(F,E) ):- P=..[F,D],box_dia(_,F),!,correct_modal(M,D,E).
  159correct_modal(M, P, cir(F,E) ):- P=..[F,D],cir_until2(F,_),!,correct_modal(M,D,E).
  160correct_modal(M, P, until2(F,E,U) ):- P=..[F,D,X],cir_until2(_,F),!,correct_modal(M,D,E),correct_modal(M,X,U).
  161correct_modal(M, P, PP):-
  162  compound_name_arguments(P,F,Args),
  163  maplist(correct_modal(M),Args,FArgs),
  164  compound_name_arguments(PP,F,FArgs),!.
  165
  166
  167f_modal(_,Fml,Fml):- non_expandable(Fml),!.
  168f_modal(M, P, O ):- P=..[F|A], aliased_rel(F,FF),!, PP=..[FF|A], f_modal(M, PP, O ).
  169f_modal(M, not(dia(FA, P)), O ):- box_dia(nesc,FA), f_modal(M, not(P), O ).
  170%f_modal(M, not(box(FA, P)), O ):- f_modal(M, P, PP ), !, f_modal(M, dia(FA, not(PP)), O ).
  171f_modal(M, box(FA, not(P)), O ):- box_dia(FA,poss), !, f_modal(M, not(P), O ).
  172%f_modal(M, not(dia(FA, P)), O ):- !, f_modal(M, not(t(FA,P)), O ).
  173f_modal(M, P, PP):-
  174  compound_name_arguments(P,F,Args),
  175  maplist(f_modal(M),Args,FArgs),
  176  compound_name_arguments(PP,F,FArgs),!.
  177
  178
  179is_modL(cir). is_modL(box). is_modL(dia). is_modL(until2).
  180d_modal(_,Fml,Fml):- var_or_atomic(Fml),!.
  181d_modal(M, P, O ):- P=..[F|A], aliased_rel(F,FF),!, PP=..[FF|A], d_modal(M, PP, O ).
  182d_modal(M, P, O ):- P=..[F,FA|Args], is_modL(F),!, maplist(d_modal(M),Args,ARGS0), append_term_l(FA,ARGS0,O).
  183d_modal(M, P, PP):-
  184  compound_name_arguments(P,F,Args),
  185  maplist(d_modal(M),Args,FArgs),
  186  compound_name_arguments(PP,F,FArgs),!.
  187
  188append_term_l(P,A,O):- P=..FA,append(FA,A,FAO),O=..FAO.
  189
  190r_modal(_,Fml,Fml):- non_expandable(Fml),!.
  191r_modal(M, not(poss(P)), O ):- !, r_modal(M, not(P), O ).
  192r_modal(M, nesc(not(P)), O ):- !, r_modal(M, not(P), O ).
  193r_modal(M, not(not(P)), O ):- !, r_modal(M, poss(P), O ).
  194r_modal(M, poss((A,B)), O ):- !, r_modal(M, (poss(A),poss(B)), O ).
  195r_modal(_, not(not(P)), \+ not(P) ):- !.
  196r_modal(_, poss(not(P)), \+ P ):- !.
  197
  198%r_modal(_, equals(A,B), false ):- A\=B, !.
  199r_modal(_, equals(X,Y), {X=Y} ):-  \+ \+ ((unlock_vars(X),nonvar(Y),X=Y)),!.
  200
  201
  202r_modal(_, not(false), true ).
  203r_modal(_, poss(false), false ).
  204r_modal(_, \+ false, true ).
  205r_modal(_, \+ true, false ).
  206
  207r_modal(_, ( _, false), false ).
  208r_modal(_, ( false, _), false ).
  209r_modal(_, ( true; _), true ).
  210r_modal(_, ( _; true), true ).
  211
  212r_modal(M, ( true, X), Y ):- r_modal(M,X,Y).
  213r_modal(M, ( false; X), Y ):- r_modal(M,X,Y).
  214
  215%r_modal(M, not(box(FA, P)), O ):- r_modal(M, P, PP ), !, r_modal(M, dia(FA, not(PP)), O ).
  216%r_modal(M, box(FA, not(P)), O ):- box_dia(FA,poss), !, r_modal(M, not(P), O ).
  217%r_modal(M, not(dia(FA, P)), O ):- !, r_modal(M, not(t(FA,P)), O ).
  218r_modal(M, P, PP):-
  219  compound_name_arguments(P,F,Args),
  220  maplist(r_modal(M),Args,FArgs),
  221  compound_name_arguments(PP,F,FArgs),!.
  222
  223
  224%%% Negation Normal Form
  225
  226% Usage: nnf(+Fml, ?NNF)
  227
  228:- export(nnf/2).  229
  230nnf(Fml,NNF) :- 
  231  nnf1(Fml,NNF1),
  232  nnf1(not(NNF1),NNF),
  233  must(ignore(NNF1==NNF)).
  234
  235nnf1(Fml,NNF) :- 
  236   correct_holds(outward,Fml,Holds),
  237   nnf(Holds,even,Fml0),!, nnf(Fml0,[],NNF,_), !.
  238
  239% -----------------------------------------------------------------
  240%  nnf(+Fml,+FreeV,-NNF,-Paths)
  241%
  242% Fml,NNF:    See above.
  243% FreeV:      List of free variables in Fml.
  244% Paths:      Number of disjunctive paths in Fml.
  245nnf(Fml,_FreeV,Fml,1):- var_or_atomic(FmlO), !, Fml=FmlO,!.
  246nnf(not(Fml),_FreeV,not(Fml),1):- var_or_atomic(Fml), !.
  247nnf(box(BP,F),FreeV,BOX,Paths) :- !,
  248	nnf(F,FreeV,NNF,Paths), cnf(NNF,CNF), boxRule(box(BP,CNF), BOX).
  249
  250nnf(dia(DP,F),FreeV,DIA,Paths) :- !,
  251	nnf(F,FreeV,NNF,Paths), dnf(NNF,DNF), diaRule(dia(DP,DNF), DIA).
  252
  253nnf(cir(CP,F),FreeV,CIR,Paths) :- !,
  254	nnf(F,FreeV,NNF,Paths), cirRule(cir(CP,NNF), CIR).
  255
  256nnf(until2(PU,A,B),FreeV,NNF,Paths) :- !,
  257	nnf(A,FreeV,NNF1,Paths1),
  258	nnf(B,FreeV,NNF2,Paths2),
  259	Paths is Paths1 + Paths2,
  260	NNF = until2(PU,NNF1, NNF2).
  261
  262nnf(all(X,F),FreeV,all(X,NNF),Paths) :- !,
  263	nnf(F,[X|FreeV],NNF,Paths).
  264
  265nnf(exists(X,Fml),FreeV,NNF,Paths) :- % trace, 
  266        !,
  267	skolem_v2(Fml,X,FreeV,FmlSk),
  268	nnf(FmlSk,FreeV,NNF,Paths).
  269
  270/*
  271nnf(atleast(1,X,Fml),FreeV,NNF,Paths) :-
  272	!,
  273	nnf(exists(X,Fml),FreeV,NNF,Paths).
  274nnf(atleast(N,X,Fml),FreeV,NNF,Paths) :-
  275	!,
  276	NewN is N - 1,
  277	nnf(','(exists(X,Fml),atleast(NewN,Y,Fml)),FreeV,NNF,Paths).
  278
  279nnf(atmost(1,X,Fml),FreeV,NNF,Paths) :-
  280	!,
  281	nnf(not(','(exists(Y,Fml),exists(Z,Fml))),FreeV,NNF,Paths).
  282nnf(atmost(N,X,Fml),FreeV,NNF,Paths) :-
  283	!,
  284	NewN is N - 1,
  285	nnf(','(exists(Y,Fml),atmost(NewN,X,Fml)),FreeV,NNF,Paths).
  286*/
  287
  288nnf(','(A,B),FreeV,NNF,Paths) :- !,
  289	nnf(A,FreeV,NNF1,Paths1),
  290	nnf(B,FreeV,NNF2,Paths2),
  291	Paths is Paths1 * Paths2,
  292	(Paths1 > Paths2 -> NNF = ','(NNF2,NNF1);
  293		            NNF = ','(NNF1,NNF2)).
  294
  295nnf(';'(A,B),FreeV,NNF,Paths) :- !,
  296	nnf(A,FreeV,NNF1,Paths1),
  297	nnf(B,FreeV,NNF2,Paths2),
  298	Paths is Paths1 + Paths2,
  299	(Paths1 > Paths2 -> NNF = ';'(NNF2,NNF1);
  300		            NNF = ';'(NNF1,NNF2)).
  301
  302nnf('<-'(B,A),FreeV,NNF,Paths) :- !,
  303         nnf(( not(A); B ),FreeV,NNF,Paths).
  304
  305nnf('->'(A,B),FreeV,NNF,Paths) :- !,
  306         nnf(( not(A); B ),FreeV,NNF,Paths).
  307
  308nnf('<->'(A,B),FreeV,NNF,Paths) :- !,
  309         nnf(';'( ','(A, B), ','(not(A), not(B))),FreeV,NNF,Paths).
  310
  311
  312nnf(not(Fml),FreeV,NNF,Paths) :- compound(Fml),
  313	(Fml = not(A)   -> Fml1 = A;
  314	 Fml = box(BP,F)      -> (must(box_dia(BP,DP)), Fml1 = dia(DP,not(F)));
  315	 Fml = dia(DP,F)      -> (must(box_dia(BP,DP)), Fml1 = box(BP,not(F)));
  316	 Fml = cir(CP,F)      -> Fml1 = cir(CP,not(F));
  317	 Fml = until2(PU,A,B) -> (nnf(not(A),FreeV,NNA,_), 
  318                                  nnf(not(B),FreeV,NNB,_),
  319                                  % circ_until(_CP,PU),
  320                                  Fml1 = ( all(_,NNB) ; until2(PU,NNB,','(NNA,NNB))));
  321	 Fml = all(X,F)   -> Fml1 = exists(X,not(F));
  322	 Fml = exists(X,F)    -> Fml1 = all(X,not(F));
  323/*
  324	 Fml = not(atleast(N,X,F)) -> Fml1 = atmost(N,X,F);
  325	 Fml = not(atmost(N,X,F)) -> Fml1 = atleast(N,X,F);
  326*/
  327	 Fml = (A;B)  -> Fml1 = ( not(A), not(B) );
  328	 Fml = (A,B) -> Fml1 = ( not(A); not(B) );
  329	 Fml = '->'(A,B) -> Fml1 = ( A, not(B) );
  330         Fml = '<->'(A,B) -> Fml1 = ';'( ','(A, not(B)) , ','(not(A), B) )
  331	),!,
  332	nnf(Fml1,FreeV,NNF,Paths).
  333
  334
  335nnf(Lit,_,Lit,1).
  336
  337
  338
  339boxRule(Fml,Fml):- non_expandable(Fml),!.
  340boxRule(box(BP,','(A,B)), ','(BA,BB)) :- !, boxRule(box(BP,A),BA), boxRule(box(BP,B),BB).
  341boxRule(BOX, BOX).
  342
  343
  344diaRule(Fml,Fml):- non_expandable(Fml),!.
  345diaRule(dia(DP,';'(A,B)), ';'(DA,DB)) :- !, diaRule(dia(DP,A),DA), diaRule(dia(DP,B),DB).
  346diaRule(DIA, DIA).
  347
  348cirRule(Fml,Fml):- non_expandable(Fml),!.
  349cirRule(cir(CP,';'(A,B)), ';'(DA,DB)) :- !, cirRule(cir(CP,A),DA), cirRule(cir(CP,B),DB).
  350cirRule(cir(CP,','(A,B)), ','(DA,DB)) :- !, cirRule(cir(CP,A),DA), cirRule(cir(CP,B),DB).
  351cirRule(CIR, CIR).
  352
  353
  354
  355
  356%%%
  357%%%  Conjunctive Normal Form (CNF) -- assumes Fml in NNF
  358%%%
  359
  360% Usage: cnf( +NNF, ?CNF )
  361
  362cnf(Fml,Fml):- var_or_atomic(Fml),!.
  363cnf(','(P,Q), ','(P1,Q1)):- !, cnf(P, P1), cnf(Q, Q1).
  364cnf(';'(P,Q),     CNF):- !, cnf(P, P1), cnf(Q, Q1), cnf1( ';'(P1,Q1), CNF ), !.
  365cnf(CNF,       CNF).
  366
  367cnf1(Fml,Fml):- var_or_atomic(Fml),!.
  368cnf1( ';'(PQ, R), (P1,Q1) ):- compound(PQ), PQ = ','(P,Q), !, cnf1( ';'(P,R), P1), cnf1( ';'(Q,R), Q1).
  369cnf1( ';'(P, QR), (P1,Q1) ):- compound(QR), QR = ','(Q,R), !, cnf1( ';'(P,Q), P1), cnf1( ';'(P,R), Q1).
  370cnf1( CNF,                 CNF).
  371
  372
  373%%%
  374%%% Disjunctive Normal Form (DNF) -- assumes Fml in NNF
  375%%%
  376% Usage: dnf( +NNF, ?DNF )
  377
  378dnf(Fml,Fml):- var_or_atomic(Fml),!.
  379dnf( ';'(P,Q),  ';'(P1,Q1) ) :- !, dnf(P, P1), dnf(Q, Q1).
  380dnf( ','(P,Q), DNF) :- !, dnf(P, P1), dnf(Q, Q1), dnf1( ','(P1,Q1), DNF).
  381dnf(DNF,       DNF).
  382
  383dnf1(Fml,Fml):-  var_or_atomic(Fml),!.
  384dnf1( ','(PQ, R), ';'(P1,Q1) ):- compound(PQ), PQ = ';'(P,Q), !, dnf1( ','(P,R), P1), dnf1( ','(Q,R), Q1).
  385dnf1( ','(P, QR), ';'(P1,Q1) ):- compound(QR), QR = ';'(Q,R), !, dnf1( ','(P,Q), P1), dnf1( ','(P,R), Q1).
  386dnf1( DNF,                  DNF ).
  387
  388
  389dont_copy_term(X,X).

  395% Usage: pnf( +Fml, ?PNF ) -- assumes Fml in NNF
  396
  397pnf(F,PNF) :- pnf(F,[],PNF).
  398
  399% pnf(+Fml, +Vars, ?PNF)
  400
  401pnf(Fml,_, Fml):- var_or_atomic(Fml),!.
  402
  403pnf(     all(X,F),Vs,   all(X,PNF)) :- !, pnf(F,[X|Vs], PNF).
  404pnf(  exists(X,F),Vs,exists(X,PNF)) :- !, pnf(F,[X|Vs], PNF).
  405
  406pnf(  ','(exists(X,A) , B),Vs,  exists(Y,PNF)) :- !, dont_copy_term((X,A,Vs),(Y,Ay,Vs)),
  407                                        pnf(','(Ay,B),[Y|Vs], PNF).
  408pnf(  ';'(exists(X,A), B),Vs,  exists(Y,PNF)) :- !, dont_copy_term((X,A,Vs),(Y,Ay,Vs)),
  409                                        pnf(';'(Ay,B),[Y|Vs], PNF).
  410pnf( ','(all(X,A), B),Vs, all(Y,PNF)) :- !, dont_copy_term((X,A,Vs),(Y,Ay,Vs)),
  411                                        pnf(','(Ay , B),[Y|Vs], PNF).
  412pnf( ';'(all(X,A), B),Vs, all(Y,PNF)) :- !, dont_copy_term((X,A,Vs),(Y,Ay,Vs)),
  413                                        pnf(';'(Ay,B),[Y|Vs], PNF).
  414
  415pnf( ','(A,exists(X,B)),Vs,  exists(Y,PNF)) :- !, dont_copy_term((X,B,Vs),(Y,By,Vs)),
  416                                        pnf(','(A, By),[Y|Vs], PNF).
  417pnf( ';'(A,exists(X,B)),Vs,  exists(Y,PNF)) :- !, dont_copy_term((X,B,Vs),(Y,By,Vs)),
  418                                        pnf(';'(A,By),[Y|Vs], PNF).
  419pnf( ','(A,all(X,B)),Vs, all(Y,PNF)) :- !, dont_copy_term((X,B,Vs),(Y,By,Vs)),
  420                                        pnf(','(A,By),[Y|Vs], PNF).
  421pnf( ';'(A,all(X,B)),Vs, all(Y,PNF)) :- !, dont_copy_term((X,B,Vs),(Y,By,Vs)),
  422                                        pnf(';'(A,By),[Y|Vs], PNF).
  423
  424pnf( ','(A, B),Vs,       PNF ) :- pnf(A,Vs,Ap), pnf(B,Vs,Bp), 
  425                                     (A\=Ap; B\=Bp), pnf(','(Ap,Bp),Vs,PNF).
  426pnf( ';'(A, B),Vs,       PNF ) :- pnf(A,Vs,Ap), pnf(B,Vs,Bp), 
  427                                     (A\=Ap; B\=Bp), pnf(';'(Ap,Bp),Vs,PNF).
  428
  429pnf(          PNF, _,       PNF ).
  430
  431%%%  Clausal Form (CF) -- assumes Fml in PNF ','
  432%                                 each quantified variable is unique
  433
  434% cf(+Fml, ?Cs)
  435% Cs is a list of the form: [cl(Head,Body), ...]
  436% Head ',' Body are lists.
  437
  438cf(PNF, Cla):- removeQ(PNF,[], UnQ), cnf(UnQ,CNF), clausify(CNF,Cla,[]).
  439
  440% removes quantifiers
  441removeQ( all(X,F),Vars, RQ) :- removeQ(F,[X|Vars], RQ).
  442
  443removeQ( exists(XVs,F),Vars, RQ) :- \+ var(XVs), term_variables(XVs,[X]), !, removeQ( exists(X,F),Vars, RQ).
  444
  445removeQ( exists(XVs,F),Vars, RQ) :- term_variables(XVs,[X]), 
  446        (Vars\==[] -> UVars=Vars ; term_variables(X+F,[X|UVars])),
  447        skolem_v3(F,X,UVars,Sk),
  448        debug_var(exists,X),
  449	removeQ('->'(some(X, Sk), F),Vars, RQ).
  450
  451removeQ( exists(XVs,F),Vars, RQ) :- term_variables(XVs,[X]), 
  452        (Vars\==[] -> UVars=Vars ; term_variables(X+F,[X|UVars])),
  453        skolem_v2(F,X,UVars,Fsk),
  454	removeQ(Fsk,Vars, RQ).
  455removeQ( F,_,F ).
  456
  457clausify( ','(P,Q), C1, C2 ) :-
  458	!,
  459	clausify( P, C1, C3 ),
  460	clausify( Q, C3, C2 ).
  461clausify( P, [cl(A,B)|Cs], Cs ) :-
  462	inclause( P, A, [], B, [] ),
  463	!.
  464clausify( _, C, C ).
  465
  466inclause( ';'(P,Q), A, A1, B, B1 ) :-
  467	!,
  468	inclause( P, A2, A1, B2, B1 ),
  469	inclause( Q, A,  A2, B,  B2 ).
  470inclause( not(P), A,  A, B1, B ) :-
  471	!,
  472	notin( P, A ),
  473	putin( P, B, B1 ).
  474inclause( P,  A1, A, B,  B ) :-
  475	!,
  476	notin( P, B ),
  477	putin( P, A, A1 ).
  478
  479notin(X,[Y|_]) :- X==Y, !, fail.
  480notin(X,[_|Y]) :- !,notin(X,Y).
  481notin(_,[]).
  482
  483putin(X,[],   [X]   ) :- !.
  484putin(X,[Y|L],[Y|L] ) :- X == Y,!.
  485putin(X,[Y|L],[Y|L1]) :- putin(X,L,L1).
  486
  487
  488
  489%%%  Skolemizing -- method 1
  490
  491% Usage: skolemize(+Fml,+X,+FreeV,?FmlSk)
  492% Replaces existentially quantified variable with the formula
  493% VARIABLES MUST BE PROLOG VARIABLES
  494% ex(X,p(X)) --> p(p(ex))
  495
  496skolem_v1(Fml,X,FreeV,FmlSk):-
  497	copy_term((X,Fml,FreeV),(Fml,Fml1,FreeV)),
  498	copy_term((X,Fml1,FreeV),(exists,FmlSk,FreeV)).
  499
  500
  501
  502%%%  Skolemizing -- method 2
  503
  504% Usage: skolem( +Fml, +X, +FreeV, ?FmlSk )
  505% Replaces existentially quantified variable with a unique function
  506% fN(Vars) N=1,...
  507% VARIABLES MAYBE EITHER PROLOG VARIABLES OR TERMS
  508
  509skolem_v2( F, X, FreeV, FmlSk) :-
  510	gensym('$kolem_Fn_' , Fun ),
  511	Sk =..[Fun|FreeV],
  512	subst( F, X, Sk, FmlSk ).
  513
  514skolem_v3( _F, _X, FreeV,  Sk) :-
  515	gensym('$kolem_Fn_' , Fun ),
  516	Sk =..[Fun|FreeV].
  517	
  518
  519
  520%%% generate new atomic symbols
  521/*
  522genatom( A ) :-
  523	db_recorded( nfsdl, Inc, Ref ),
  524	!,
  525	erase( Ref ),
  526	NewInc is Inc + 1,
  527	db_recordz( nfsdl, NewInc, _ ),
  528	atom_concat( f, NewInc, A ).
  529genatom( f1 ) :-
  530	db_recordz( nfsdl, 1, _ ).
  531
  532%%% Substitution
  533
  534% Usage: subst(+Fml,+X,+Sk,?FmlSk)
  535
  536subst(   all(Y,P), X,Sk,   all(Y,P1) ) :- !, subst( P,X,Sk,P1 ).
  537subst(exists(Y,P), X,Sk,exists(Y,P1) ) :- !, subst( P,X,Sk,P1 ).
  538subst( ','(P,Q), X,Sk,','(P1,Q1) ) :- !, subst( P,X,Sk,P1 ), subst( Q,X,Sk,Q1 ).
  539subst(  ';'(P,Q), X,Sk, ';'(P1,Q1) ) :- !, subst( P,X,Sk,P1 ), subst( Q,X,Sk,Q1 ).
  540subst(       P,    X,Sk,       P1    ) :- functor(P,_,N), subst1( X, Sk, P, N, P1 ).
  541
  542subst1( _,  _, P, 0, P  ).
  543subst1( X, Sk, P, N, P1 ) :- N > 0, P =..[F|Args], subst2( X, Sk, Args, ArgS ),
  544                             P1 =..[F|ArgS].
  545
  546subst2( _,  _, [], [] ).
  547subst2( X, Sk, [A|As], [Sk|AS] ) :- X == A, !, subst2( X, Sk, As, AS).
  548subst2( X, Sk, [A|As], [A|AS]  ) :- var(A), !, subst2( X, Sk, As, AS).
  549subst2( X, Sk, [A|As], [Ap|AS] ) :- subst( A,X,Sk,Ap ),
  550                                    subst2( X, Sk, As, AS).
  551*/
  552
  553% this is both a latex file ',' a quintus prolog file
  554% the only difference is that the latex version comments out the following
  555% line:
  556
  557%:- module(snark_theorist,[]).
  558
  559%:- module(snark_theorist).
  560
  561/* 
  562\documentstyle[12pt,makeidx]{article}
  563\pagestyle{myheadings}
  564\markright{Theorist to Prolog (th2.tex)}
  565\makeindex
  566\newtheorem{example}{Example}
  567\newtheorem{algorithm}{Algorithm}
  568\newtheorem{theorem}{Theorem}
  569\newtheorem{lemma}[theorem]{Lemma}
  570\newtheorem{definition}{Definition}
  571\newtheorem{corollary}[theorem]{Corollary}
  572\newenvironment{proof}{\begin{quote} {\bf Proof: }}{$\Box$\end{quote}}
  573\newenvironment{prolog}{\begin{tabbing} \hbox{2cm}\=\hbox{1cm}\=\kill
  574    }{\end{tabbing}}
  575\newcommand{\IF}{\ $:-$\\\>}
  576\newcommand{\AND}{,\\\>}
  577\title{A Theorist to Prolog Compiler (th2.tex)\thanks{Copyright \copyright 1990
  578David Poole. All rights reserved.}}
  579\author{David Poole\\
  580Department of Computer Science,\\
  581University of British Columbia,\\
  582Vancouver, B.C. Canada V6T 1W5
  583(604) 228-6254\\
  584poole@cs.ubc.ca}
  585\begin{document}
  586\maketitle
  587\begin{abstract}
  588Artificial intelligence researchers have been designing representation
  589systems for default ',' abductive reasoning.
  590Logic Programming researchers have been working on techniques to improve
  591the efficiency of Horn Clause deduction systems.
  592This paper describes how {\em Theorist\/} can be
  593translated into Quintus Prolog.
  594The verbatim code is the actual running code.
  595
  596This should not be seen as {\em The Theorist System}, but rather
  597as one implementation of the Theorist framework. Theorist should be
  598seen as the idea that much reasoning can be done by theory formation
  599from a fixed set of possible hypotheses.
  600This implementation is based on a complete linear resolution theorem prover
  601which does not multiply out subterms. It also carries out incremental
  602consistency checking.
  603Note that there is nothing in this document which forces the control strategy
  604of Prolog. This is a compiler from Theorist to a Horn-clause reasoner
  605with negation as failure; nothing precludes any other search strategy
  606(e.g., dependency directed backtracking, constraint propagation).
  607This is intended to be a runnable specification, which runs fast
  608(e.g., for the common intersection between Theorist ',' Prolog (i.e., Horn
  609clauses) Theorist code runs about half the speed of compiled Quintus
  610Prolog code).
  611
  612This code is available electronically from the author.
  613\end{abstract}
  614\tableofcontents
  615\section{Introduction}
  616Many people in Artificial Intelligence have been working on default reasoning
  617',' abductive diagnosis systems 
  618\cite{reiter80,mccarthy86,cox87,poole:lf}. The systems implemented so far
  619(eg., \cite{brewka86,lifschitz85,ginsberg87,pga}) are only prototypes ';'
  620have been developed in ways that cannot take full advantage in the
  621advances of logic programming implementation technology.
  622
  623Many people are working on making logic programming systems more efficient.
  624These systems, however, usually assume that the input is in the form of
  625Horn clauses with negation as failure. This paper shows how to implement
  626the default reasoning system Theorist \cite{poole:lf,pga}
  627by compiling its input into Horn clauses with negation as failure, thereby
  628allowing direct
  629use the advances in logic programming implementation technology.
  630Both the compiler ',' the compiled code can take advantage of 
  631these improvements.
  632
  633We have been running this implementation on standard
  634Prolog compilers (in particular Quintus Prolog) ',' it outperforms
  635all other default reasoning systems that the author is aware of.
  636It is, however, not restricted to the control structure of Prolog. There is
  637nothing in the compiled code which forces it to use Prolog's
  638search strategy.
  639Logic programming ',' other researchers are working on alternate
  640control structures which seem very appropriate for default 
  641',' abductive reasoning.
  642Advances in parallel inference (e.g.,\ \cite{pie}),
  643constraint satisfaction \cite{dincbas,vanh} ',' dependency directed backtracking
  644\cite{dekleer86,doyle79,cox82} 
  645should be able to be directly applicable to the code produced by this compiler.
  646
  647We are thus effecting a clear
  648distinction between the control ',' logic of our default reasoning systems
  649\cite{kowalski}. We can let the control people concentrate on efficiency
  650of Horn clause systems, ',' these will then be directly applicable to
  651those of us building richer representation systems.
  652The Theorist system has been designed to allow maximum flexibility in
  653control strategies while still giving us the power of assumption-based
  654reasoning that are required for default ',' abductive reasoning.
  655
  656This is a step towards having representation ',' reasoning systems
  657which are designed for correctness being able to use the most
  658efficient of control
  659strategies, so we can have the best of expressibility ',' efficiency.
  660\section{Theorist Framework} \label{theorist}
  661
  662Theorist \cite{poole:lf,pga} is a logical reasoning system for default reasoning
  663',' diagnosis. It is based on the idea of theory formation from a fixed
  664set of possible hypotheses.
  665
  666This implementation is of the version of Theorist described in \cite{poole:lf}.
  667The user provides three sets of first order formulae
  668\begin{itemize}
  669\item[${\cal F}$] is a set of closed formulae called the {\em facts\/}.
  670These are intended to be true in the world being modelled.
  671\item[$\Delta$] is a set of formulae which
  672act as {\em possible hypotheses}, any ground instance of which
  673can be used in an explanation if consistent.
  674\item[$\cal C$] is a set of closed formulae taken as constraints.
  675The constraints restrict what can be hypothesised.
  676\end{itemize}
  677
  678We assume that ${\cal F}\cup C$ is consistent.
  679
  680\begin{definition} \em
  681a {\bf  scenario} of ${\cal F},\Delta$ is a set $D \cup {\cal F}$ where
  682$D$ is a set of ground instances of elements
  683of $\Delta$ such that $D\cup {\cal F} \cup C$ is consistent.
  684\end{definition}
  685
  686\begin{definition} \em
  687If $g$ is a closed formula then an {\bf explanation} of $g$ from ${\cal F},\Delta$
  688is a  scenario of ${\cal F},\Delta$ which implies $g$.
  689\end{definition}
  690That is, $g$ is explainable from ${\cal F},\Delta$ if there is a set
  691$D$ of ground instances of elements of $\Delta$ such that
  692\begin{quote}
  693${\cal F} \cup D \models g$ ','\\
  694${\cal F} \cup D \cup C$ is consistent
  695\end{quote}
  696${\cal F} \cup D$ is an explanation of $g$.
  697
  698In other papers we have described how this can be the basis of
  699default ',' abductive reasoning systems \cite{pga,poole:lf,poole:dc,poole:dd}.
  700If we are using this for prediction then possible hypotheses can be seen
  701as defaults. \cite{poole:lf} describes how this formalism can account
  702for default reasoning. This is also a framework for abductive reasoning
  703where the possible hypotheses are the base causes we are prepared
  704to accept as to why some observation was made \cite{pga}.
  705We will refer to possible hypotheses as defaults.
  706
  707One restriction that can be made with no loss of expressive power
  708is to restrict possible hypotheses to just atomic forms with no
  709structure \cite{poole:lf}. This is done by naming the defaults.
  710\subsection{Syntax} \label{syntax}
  711The syntax of Theorist is designed to be of maximum flexibility.
  712Virtually any syntax is appropriate for wffs; the formulae are translated
  713into Prolog clauses without mapping out subterms. The theorem
  714prover implemented in the Compiler can be seen as a non-clausal theorem
  715prover \cite{poole:clausal}.
  716
  717A {\em wff\/} is a well formed formula made up of arbitrary combination of
  718equivalence (``=='', ``$equiv$''),
  719implication (``$=>$'', ``$<-$''), disjunction (``$or$'', ``;''),
  720conjunction (``$and$'', ``$\&$'', ``,'') ',' negation (``$not$'', ``\~{}'')
  721of atomic symbols. Variables follow the Prolog convention
  722of being in upper case. There is no explicit quantification.
  723
  724A {\em name\/} is an atomic symbol with only free variables as arguments.
  725
  726The following gives the syntax of the Theorist code:
  727\begin{description}
  728\item[\bf fact]
  729$w.$\\
  730where $w$ is a wff,
  731means that $(\forall w) \in {\cal F}$; i.e., the universal closure of $w$ (all
  732variables universally quantified) is a fact.
  733\item[\bf default]
  734$d.$\\
  735where $d$ is a name,
  736means that $d\in \Delta$; i.e., $d$ is a default (a possible hypothesis).
  737\item[\bf default]
  738$d:w.$\\
  739where $d$ is a name ',' $w$ is a wff means $w$, with name $d$ can
  740be used in a scenario if it is consistent.
  741Formally it means $d\in  \Delta$ ','
  742$(\forall d\Rightarrow w) \in {\cal F}$.
  743\item[\bf constraint]
  744$w.$\\
  745where $w$ is a wff means $\forall w\in \cal C$.
  746\item[\bf prolog]
  747$p.$\\
  748where $p$ is an atomic symbol means any Theorist call to $p$ should
  749be proven in Prolog. This allows us to use built-in predicates of pure Prolog.
  750One should not expect Prolog's control predicates to work.
  751\item[\bf explain]
  752$w.$\\
  753where $w$ is an arbitrary wff,
  754gives all explanations of $\exists w$.
  755\item[\bf predict]
  756$w.$\\
  757where $w$ is a arbitrary ground wff,
  758returns ``yes'' if $w$ is in every extension of the defaults
  759',' ``no'' otherwise.
  760If it returns ``yes'', a set of explanations is returned, if
  761it returns ``no'' then a scenario from which $g$ cannot be explained is
  762returned (this follows the framework of \cite{poole:dc}).
  763
  764\end{description}
  765
  766In this compiler these are interpreted as commands to Prolog.
  767The interface will thus be the Prolog interface with some predefined
  768commands.
  769
  770\subsection{Compiler Directives}
  771The following are compiler directives:
  772\begin{description}
  773\item[\bf thconsult] {\em filename.}\\
  774reads commands from {\em filename}, ',' asserts ','/';' executes them.
  775\item[\bf thtrans] {\em filename.}\\
  776reads commands from {\em filename} ',' translates them into Prolog
  777code in the file {\em filename.pl}.
  778\item[\bf thcompile] {\em filename.}\\
  779reads commands from {\em filename}, translates them into the file
  780{\em filename.pl} ',' then compiles this file. ``explain'' commands in
  781the file are not interpreted.
  782\item[\bf dyn] {\em atom.}\\
  783should be in a file ',' declares that anything matching the atom
  784is allowed to be asked ';' added to. This should appear before any
  785use of the atom. This corresponds to the ``dynamic'' declaration of
  786Quintus Prolog. This is ignored except when compiling a file.
  787\end{description}
  788There are some other commands which allow one to set flags. See section
  789\ref{flags} for more detail on setting checking ',' resetting flags.
  790
  791\section{Overview of Implementation}
  792In this section we assume that we have a deduction system 
  793(denoted $\vdash$) which has the 
  794following properties (such a deduction system will be defined in the
  795next section):
  796\begin{enumerate}
  797\item It is sound (i.e., if $A\vdash g$ then $A\models g$).
  798\item It is complete in the sense that if $g$ follows from a consistent
  799set of formulae, then $g$ can be proven. I.e., if $A$ is consistent ','
  800$A\models g$ then $A\vdash g$.
  801\item If $A\vdash g$ then $A\cup B\vdash g$; i.e., adding in extra facts will
  802not prevent the system from finding a proof which previously existed.
  803\item It can return instances of predicates which were used in the proof.
  804\end{enumerate}
  805
  806The basic idea of the implementation follows the definition on explainability:
  807\begin{algorithm}\em \label{basic-alg}
  808to explain $g$
  809\begin{enumerate}
  810\item try to prove $g$ from ${\cal F}\cup \Delta$. If no proof exists, then
  811$g$ is not explainable. If there is a proof, let $D$ be the set of instances of
  812elements of $\Delta$ used in the proof. We then know
  813\[{\cal F}\cup D \models g\]
  814by the soundness of our proof procedure.
  815\item show $D$ is consistent with ${\cal F}\cup C$
  816by failing to prove it is inconsistent.
  817\end{enumerate}
  818\end{algorithm}
  819
  820\subsection{Consistency Checking}
  821The following two theorems are important for implementing the consistency
  822check:
  823\begin{lemma} \label{incremantal}
  824If $A$ is a consistent set of formulae ','
  825$D$ is a finite set of ground instances of possible hypotheses, then
  826if we impose arbitrary ordering on the elements of $D=\{d_1,...,d_n\}$
  827\begin{center}
  828$A\cup D$ is inconsistent\\if ',' only if\\
  829there is some $i$, $1\leq i \leq n$ such that
  830$A\cup \{d_1,...,d_{i-1}\}$ is consistent ','\\
  831$A\cup \{d_1,...,d_{i-1}\}\models \neg d_i$.
  832\end{center}
  833\end{lemma}
  834\begin{proof}
  835If $A \cup D $ is inconsistent there is some least $i$ such
  836that $A\cup \{d_1,...,d_i\}$ is inconsistent. Then we must have
  837$A\cup \{d_1,...,d_{i-1}\}$ is consistent (as $i$ is minimal) ','
  838$A\cup \{d_1,...,d_{i-1}\}\models \neg d_i$ (by inconsistency).
  839\end{proof}
  840
  841This lemma says that we can show that ${\cal F}\cup C \cup \{d_1,...,d_n\}$ is 
  842consistent if we can show that for all $i$, $1\leq i \leq n$,
  843${\cal F}\cup C\cup \{d_1,...,d_{i-1}\}\not\vdash \neg d_i$.
  844If our theorem prover can show there is no proof of all of
  845the $\neg d_i$, then we have consistency.
  846
  847This lemma indicates that we can implement Theorist by incrementally failing to
  848prove inconsistency. We need to try to prove the negation of the
  849default in the context of all previously assumed defaults.
  850Note that this ordering is arbitrary.
  851
  852The following theorem expands on how explainability can be computed:
  853\begin{theorem} \label{consisthm}
  854If ${\cal F} \cup C$ is consistent,
  855$g$ is explainable from ${\cal F},\Delta$ if ',' only if there is a ground
  856proof of $g$ from ${\cal F}\cup D$ where $D=\{d_1,...,d_n\}$
  857is a set of ground instances
  858of elements of $\Delta$ such that
  859${\cal F} \wedge C \wedge \{d_1,...,d_{i-1}\}\not\vdash \neg d_i$
  860for all $i,1\leq i \leq n$.
  861\end{theorem}
  862\begin{proof}
  863If $g$ is explainable from ${\cal F},\Delta$, there is a set $D$ of ground instances
  864of elements of $\Delta$ such that ${\cal F}\cup D \models g$ ',' ${\cal F} \cup D \cup C$
  865is consistent. So there is a ground proof of $g$ from ${\cal F} \cup D$.
  866By the preceding lemma
  867${\cal F}\cup D \cup C$ is consistent so there can be no sound proof
  868of inconsistency. That is, we cannot prove
  869${\cal F} \wedge C \wedge \{d_1,...,d_{i-1}\}\vdash \neg d_i$ for any $i$.
  870\end{proof}
  871
  872This leads us to the refinement of algorithm \ref{basic-alg}:
  873\begin{algorithm} \em
  874to explain $g$ from ${\cal F},\Delta$
  875\begin{enumerate}
  876\item Build a ground proof of $g$ from ${\cal F}\cup \Delta$. Make $D$ 
  877the set of instances of elements of $\Delta$ used in the proof.
  878\item For each $i$, try to prove $\neg d_i$ from ${\cal F} \wedge C
  879\wedge \{d_1,...,d_{i-1}\}$. If all
  880such proofs fail, $D$ is an explanation for $g$.
  881\end{enumerate}
  882\end{algorithm}
  883
  884Note that the ordering imposed on the $D$ is arbitrary. A sensible one is
  885the order in which the elements of $D$ were generated. Thus when
  886a new hypothesis is used in the proof, we try to prove its negation from
  887the facts ',' the previously used hypotheses. These proofs are independent
  888of the original proof ',' can be done as they are generated
  889as in negation as failure (see section \ref{incremental}), ';' can be done
  890concurrently.
  891
  892\subsection{Variables}
  893Notice that theorem \ref{consisthm} says that $g$ is explainable
  894if there is a ground proof. There is a problem that arises
  895to translate the preceding algorithm (which assumes ground proofs)
  896into an algorithm which does not build ground proofs (eg., a standard
  897resolution theorem prover), as we may have variables in the forms
  898we are trying to prove the negation of.
  899
  900A problem arises
  901when there are variables in the $D$ generated.
  902 Consider the following example:
  903\begin{example}\em
  904Let $ \Delta = \{p(X)\}$. That is, any instance of $p$ can be used if it is
  905consistent.
  906Let ${\cal F} = \{ \forall Y (p(Y) \Rightarrow g), \neg p(a)\}$. That is, $g$ is
  907true if there is a $Y$ such that $p(Y)$.
  908
  909According to our semantics,
  910$g$ is explainable with the explanation $\{p(b)\}$,
  911which is consistent with ${\cal F}$ (consider the interpretation $I=\{\neg p(a),p(b)\}$
  912on the domain $\{a,b\}$), ',' implies $g$.
  913
  914However,
  915if we try to prove $g$, we generate $D=\{p(Y)\}$ where $Y$ is free
  916(implicitly a universally quantified variable).
  917The existence of the fact $\neg p(a)$ should not make it
  918inconsistent, as we want $g$ to be explainable.
  919\end{example}
  920\begin{theorem}
  921It is not adequate to only consider interpretations in the
  922Herbrand universe of ${\cal F}\cup \Delta \cup C$ to determine explainability.
  923\end{theorem}
  924\begin{proof}
  925consider the example above; the Herbrand universe is just
  926the set $\{a\}$. Within this domain there is no consistent 
  927explanation to explain $g$.
  928\end{proof}
  929
  930This shows that Herbrand's theorem is not applicable to the whole system.
  931It is, however, applicable to each of the deduction steps \cite{chang}.
  932
  933So we need to generate a ground proof of $g$. This leads us to:
  934
  935\begin{algorithm} \em \label{det-alg}
  936To determine if $g$ is explainable from ${\cal F},\Delta$
  937\begin{enumerate}
  938\item generate a proof of $g$ using elements of ${\cal F}$ ',' $ \Delta$ as axioms.
  939Make $D_0$ the set of instances of $ \Delta$ used in the proof;
  940\item form $D_1$ by replacing free variables in $D_0$ with unique constants;
  941\item add $D_1$ to ${\cal F}$ ',' try to prove an inconsistency (as in the
  942previous case). If a
  943complete search for a proof fails, $g$ is explainable.
  944\end{enumerate}
  945\end{algorithm}
  946
  947This algorithm can now be directly implemented by a resolution theorem prover.
  948
  949\begin{example}\em
  950Consider ${\cal F}$ ',' $\Delta$ as in example 1 above.
  951If we try to prove $g$, we use the hypothesis instance $p(Y)$.
  952This means that $g$ is provable from any instance of $p(Y)$.
  953To show $g$ cannot be explained, we must show that all of the instances
  954are inconsistent. The above algorithm says
  955we replace $Y$ with a constant $\beta$.
  956$p(\beta)$ is consistent with the facts.
  957Thus we can show $g$ is explainable.
  958\end{example}
  959
  960\subsection{Incremental Consistency Checking} \label{incremental}
  961Algorithm \ref{det-alg} assumed that we only check consistency at the end.
  962We cannot replace free variables by a unique constant until the end
  963of the computation.
  964This algorithm can be further refined by considering cases
  965where we can check consistency at the time the hypothesis is generated.
  966
  967Theorem \ref{incremantal} shows that we can check consistency incrementally
  968in whatever order we like. The problem is to determine whether we have
  969generated the final version of a set of hypotheses.
  970If there are no variables in our set of hypotheses, then we can check
  971consistency as soon as they are generated.
  972If there are variables in a hypothesis, then we cannot guarantee that the
  973form generated will be the final form of the hypothesis.
  974\begin{example}\em
  975Consider the two alternate set of facts:
  976\begin{eqnarray*}
  977\Delta&=\{&p(X)\ \}\\
  978{\cal F}_1&=\{&\forall X \ p(X) \wedge q(X) \Rightarrow g,\\
  979&&\neg p(a),\\
  980&&q(b) \ \}\\
  981{\cal F}_2&=\{&\forall X \ p(X) \wedge q(X) \Rightarrow g,\\
  982&&\neg p(a),\\
  983&&q(a) \ \}
  984\end{eqnarray*}
  985Suppose we try to explain $g$ by first explaining $p$ ',' then explaining $q$.
  986Once we have generated the hypothesis $p(X)$, we have not enough information to
  987determine whether the consistency check should succeed ';' fail.
  988The consistency check for ${\cal F}_1$ should succeed (i.e, we should conclude
  989with a consistent instance, namely $X=b$), but the 
  990consistency check for ${\cal F}_2$ should fail (there is no consistent value
  991for the $X$ which satisfies $p$ ',' $q$).
  992We can only determine the consistency after we have proven $q$.
  993\end{example}
  994
  995There seems to be two obvious solutions to this problem,
  996the first is to allow the consistency check to return constraints on the
  997values (eg., \cite{edmonson}). The alternate (',' simpler) solution is
  998to delay the evaluation of the consistency check until all of the variables
  999are bound (as in \cite{naish86}), ';' until we know that the variables
 1000cannot be bound any more. In particular we know that a variable cannot be
 1001bound any more at the end of the computation.
 1002
 1003The implementation described in this paper
 1004does the simplest form of incremental consistency checking, namely it computes
 1005consistency immediately for those hypotheses with no variables ',' delays
 1006consistency checking until the end for hypotheses containing variables
 1007at the time they are generated.
 1008\section{The Deduction System} \label{deduction}
 1009
 1010This implementation is based on linear resolution \cite{chang,loveland78}.
 1011This is complete in the
 1012sense that if $g$ logically follows from some {\em consistent} set of
 1013clauses $A$, then there is a linear resolution proof of $g$ from $A$.
 1014
 1015SLD resolution of Prolog \cite{lloyd} can be seen as linear resolution with
 1016the contrapositive ',' ancestor search removed.
 1017
 1018To implement linear resolution in Prolog, we add two things
 1019\begin{enumerate}
 1020\item we use the contrapositive of our clauses. If we have the clause
 1021\begin{verse}
 1022$L_1 \vee L_2 \vee ... \vee L_n$
 1023\end{verse}
 1024then we create the $n$ rules
 1025\begin{verse}
 1026$L_1 \leftarrow \neg L_2 \wedge ... \wedge \neg L_n$\\
 1027$L_2 \leftarrow \neg L_1 \wedge \neg L_3 \wedge ... \wedge \neg L_n$\\
 1028$...$\\
 1029$L_n \leftarrow \neg L_1 \wedge ... \wedge \neg L_{n-1}$
 1030\end{verse}
 1031as rules. Each of these can then be used to prove the left hand literal
 1032if we know the other literals are false. Here we are treating the negation
 1033of an atom as a different Prolog atom (i.e.,\ we treat $\neg p(\overline{X})$
 1034as an atom $notp(\overline{X})$).
 1035\item the ancestor cancellation rule. While trying to prove $L$ we can assume
 1036$\neg L$. We have a subgoal proven if it unifies with the negation of
 1037an ancestor in the proof tree.
 1038This is an instance of proof by contradiction. We can see this as assuming
 1039$\neg L$ ',' then when we have proven $L$ we can discharge the assumption.
 1040\end{enumerate}
 1041
 1042One property of the deduction system that we want is the ability to
 1043implement definite clauses with a constant factor overhead over
 1044using Prolog. One way to do this is to keep two lists of ancestors
 1045of any node: $P$ the positive (non negated atoms) ancestors
 1046',' $N$ the negated ancestors. Thus for a positive subgoal we
 1047only need to search for membership in $N$ ',' for a negated subgoal we only
 1048need to search $P$.
 1049When we have definite clauses, there are no negated subgoals, ',' so 
 1050$N$ is always empty. Thus the ancestor search always consists
 1051of checking for membership in an empty list. The alternate
 1052contrapositive form of the clauses are never used.
 1053
 1054Alternate, more complicated ways to do ancestor search
 1055have been investigated \cite{poole:grace}, but this implementation
 1056uses the very simple form given above.
 1057Another tempting possibility is to use the near-Horn resolution
 1058of \cite{loveland87}. More work needs to be done on this area.
 1059\subsection{Disjunctive Answers}
 1060For the compiler to work properly we need to be able to return
 1061disjunctive answers. We need disjunctive answers for the case
 1062that we can prove only a disjunctive form of the query.
 1063
 1064For example, if we can prove $p(a)\vee p(b)$ for the
 1065query $?p(X)$, then we want the answer $X= a$ ';' $b$.
 1066This can be seen as ``if the answer is not $a$ then the
 1067answer is $b$''.
 1068
 1069To have the answer $a_1\vee...\vee a_n$, we need to have a proof
 1070of ``If the answer is not $a_1$ ',' not $a_2$ ',' ... ',' not $a_{n-1}$
 1071then the answer is $a_n$''.
 1072We collect up conditions on the proof of
 1073alternate answers that we are assuming are not true in order to have
 1074the disjunctive answer.
 1075
 1076This is implemented by being able to assume the negation of the top level
 1077goal as long as we add it to the set of answers. To do this we carry a list
 1078of the alternate disjuncts that we are assuming in proving the top level goal.
 1079\subsection{Conversion to Clausal Form}
 1080It is desirable that we can convert an
 1081arbitrary well formed formula into clausal (';' rule) form
 1082without mapping out subterms. Instead of distributing, we do this by
 1083creating a new term to refer to the disjunct.
 1084
 1085Once a formula is in negation normal form, then the normal way 
 1086to convert to clausal form \cite{chang} is to
 1087convert something of the form
 1088\[\alpha \vee (\beta \wedge \gamma)\]
 1089by distribution into
 1090\[(\alpha \vee \beta) \wedge (\alpha \vee \gamma)\]
 1091',' so mapping out subterms.
 1092
 1093The alternate \cite{poole:clausal} is to create a new relation $p$ parameterised
 1094with the variables in common with $\alpha$ ',' $\beta \wedge \gamma$.
 1095We can then replace $\beta \wedge \gamma$ by $p$ ',' then add
 1096\[(\neg p \vee \beta)\wedge (\neg p \vee \gamma)\]
 1097to the set of formulae.
 1098
 1099This can be embedded into the compiler by using
 1100Prolog ``';''' instead of actually building the $p$. 
 1101(Alternatively we can define ``';''' by defining the
 1102clause $(p;q)\leftarrow p$ ',' $(p;q)\leftarrow q$.)
 1103We build up the clauses so that the computation runs
 1104without any multiplying out of subterms.
 1105This is an instance of the general procedure of making clausal
 1106theorem provers into non-clausal theorem provers \cite{poole:clausal}.
 1107\section{Details of the Compiler}
 1108In this section we give actual code which converts
 1109Theorist code into Prolog code.
 1110The compiler is described here in a bottom up fashion; from the
 1111construction of the atoms to compilation of general formulae.
 1112
 1113The compiler is written in Prolog ',' the
 1114target code for the compiler is Prolog code (in particular Horn
 1115clauses with negation as failure). There are no ``cuts'' ';' other
 1116non-logical ``features'' of Prolog which depend on Prolog's
 1117search strategy in the compiled code.
 1118Each Theorist wff gets locally translated into a set of
 1119Prolog clauses.
 1120\subsection{Target Atoms}
 1121For each Theorist predicate symbol $r$ there are 4 target predicate
 1122symbols, with the following informal meanings:
 1123\begin{description}
 1124\item[prv\_tru\_r] meaning $r$ can be proven from the facts ',' the constraints.
 1125\item[prv\_not\_r] meaning $\neg r$ can be proven from the facts 
 1126',' the constraints.
 1127\item[ex\_tru\_r] meaning $r$ can be explained from ${\cal F},\Delta$.
 1128\item[ex\_not\_r] meaning $\neg r$ can be explained from ${\cal F},\Delta$.
 1129\end{description}
 1130
 1131The arguments to these built predicate symbols will contain all
 1132of the information that we need to prove ';' explain instances of the source
 1133predicates.
 1134\subsubsection{Proving}
 1135For relation $r(-args-)$ in the source code we want to produce object
 1136code which says that $r(-args-)$ (';' its negation)
 1137can be proven from the facts ',' constraints ',' the current set
 1138of assumed hypotheses.
 1139
 1140For the source relation
 1141\[r( - args -)\]
 1142(which is to mean that $r$ is a relation with $-args-$ being the
 1143sequence of its arguments),
 1144we have the corresponding target relations
 1145\[prv\_tru\_r( - args - , Ths, Anc)\]
 1146\[prv\_not\_r( - args - , Ths, Anc)\]
 1147which are to mean that $r$ (';' $\neg r$) can be proven
 1148>from the facts ',' ground hypotheses
 1149$Ths$ with ancestor structure $Anc$.
 1150These extra arguments are:
 1151
 1152\begin{description}
 1153\item $Ths$ is a list of ground defaults.
 1154These are the defaults we have already assumed ',' so define the context in
 1155which to prove $r(-args-)$.
 1156\item $Anc$ is a structure of the form $anc(P,N)$ where $P$ ',' $N$ are
 1157lists of source atoms. Interpreted procedurally,
 1158$P$ is the list of positive (not negated) ancestors of
 1159the goal in a proof ',' $N$ is the list of negated ancestors
 1160in a proof. As described in section \ref{deduction} we conclude some goal
 1161if it unifies with its negated ancestors.
 1162\end{description}
 1163
 1164Declaratively,
 1165\[prv\_tru\_r( - args - , Ths, anc(P,N))\]
 1166means
 1167\[{\cal F}\cup Ths \cup \neg P \cup N \models r(-args-)\]
 1168
 1169\subsubsection{Explaining}
 1170There are two target relations for explaining associated with
 1171each source relation $r$. These are $ex\_tru\_r$ ',' $ex\_not\_r$.
 1172
 1173For the source relation:
 1174\[r( - args -)\]
 1175we have two target new relations for explaining $r$:
 1176\[ex\_tru\_r( - args - , Ths, Anc, Ans)\]
 1177\[ex\_not\_r( - args - , Ths, Anc, Ans)\]
 1178These mean that $r(-args-)$ (';' $\neg r(-args-)$) can be explained, with
 1179\begin{description}
 1180\item[$Ths$] is the structure of the incrementally built hypotheses
 1181used in explaining $r$. There are two statuses of hypotheses we
 1182use; one the defaults that are ground ',' so can be proven
 1183consistent at the time of generation;
 1184the other the hypotheses with free variables at the time they
 1185are needed in the proof, for which we defer consistency
 1186checking (in case the free variables get instantiated later in the proof).
 1187$Ths$ is essentially
 1188two difference lists, one of the ground defaults already
 1189proven consistent ',' one of the
 1190deferred defaults. $Ths$ is of the form
 1191\[ths(T_1,T_2,D_1,D_2)\]
 1192which is to mean that $T_1$ is the consistent hypotheses before
 1193we try to explain $r$, ','
 1194',' $T_2$ is the list of consistent hypotheses which includes
 1195$T_1$ ',' those hypotheses assumed to explain $r$.
 1196Similarly, $D_1$ is the list of deferred hypotheses before we consider the goal
 1197',' $D_2$ is the list of resulting deferred hypotheses used in explaining $r$.
 1198
 1199\item[$Anc$] contains the ancestors of the goal. As in the previous case,
 1200this is a pair of the form
 1201$anc(P,N)$ where $P$ is the list of positive ancestors of the goal,
 1202',' $N$ is the list of negated ancestors of the goal.
 1203
 1204\item[$Ans$] contains the answers we are considering in difference list form
 1205$ans(A_1,A_2)$, where $A_1$ is the answers before
 1206proving the goal, ',' $A_2$ is the answers after proving the goal.
 1207\end{description}
 1208
 1209The semantics of
 1210\[ex\_tru\_r(-args-,ths(T_1,T_2,D_1,D_2),anc(P,N),ans(A_1,A_2))\]
 1211is defined by
 1212\[{\cal F}\cup T_2 \cup D_2 \cup \neg P \cup N \cup A_2 \models r(-args-) \]
 1213where $T_1\subseteq T_2$, $D_1\subseteq D_2$ ',' $A_1\subseteq A_2$, ','
 1214such that
 1215\[{\cal F}\cup T_2 \hbox{ is consistent}\]
 1216
 1217\subsubsection{Building Atoms}
 1218The procedure {\em new\_lit$($Prefix, Reln, Newargs, Newreln\/}$)$ constructs
 1219a new atom, $Newreln$, with predicate symbol made up of
 1220$Prefix$ prepended to the
 1221predicate symbol of $Reln$, ',' taking as arguments the arguments of $Reln$
 1222together with $Newargs$.
 1223For example,
 1224\begin{quote}
 1225?-- new\_lit(`ex\_tru\_`,reln(a,b,c),[T,A,B],N).
 1226\end{quote}
 1227yields
 1228\begin{quote}
 1229N = ex\_tru\_reln(a,b,c,T,A,B)
 1230\end{quote}
 1231
 1232The procedure is defined as follows\footnote{The verbatim code
 1233is the actual implementation code given in standard Edinburgh notation.
 1234I assume that the reader is familiar with such notation.}:
 1235\index{new\_lit}
 1236\index{add\_prefix}
 1237\begin{verbatim} */
 1238
 1239
 1240new_lit(_Prefix, Reln, _NewArgs, NewReln) :- is_thbuiltin(Reln),!,NewReln=Reln.
 1241
 1242new_lit(Prefix, Reln, NewArgs, NewReln) :-
 1243   Reln =.. [Pred | Args],
 1244   add_prefix(Prefix,Pred,NewPred),
 1245   append(Args, NewArgs, AllArgs),
 1246   NewReln =.. [NewPred | AllArgs].
 1247
 1248add_prefix(Prefix,Pred,NewPred) :-
 1249    trace,
 1250   string_codes(Prefix,PrefixC),
 1251   name(Pred,PredName),
 1252   append(PrefixC, PredName, NewPredName),
 1253   name(NewPred,NewPredName).
 1254
 1255
 1256/* \end{verbatim}
 1257\subsection{Compiling Rules}
 1258The next simplest compilation form we consider is the intermediate form
 1259called a ``rule''.
 1260Rules are statements of how to conclude
 1261the value of some relation. Each Theorist fact corresponds to a number
 1262of rules (one for each literal in the fact).
 1263Each rule gets translated into Prolog rules to explain
 1264',' prove the head of the rule. 
 1265
 1266Rules use the intermediate form called a ``literal''.
 1267A literal is either an atomic symbol ; of the form $n(A)$ where $A$ is
 1268an atomic symbol.
 1269A rules is either a literal ';'
 1270of the form {\em H $\leftarrow$ Body} (written ``{\tt <-(H,Body)}'')
 1271where $H$ is a literal
 1272',' $Body$ is a conjunction ',' disjunction of literals.
 1273
 1274We translate rules of the form
 1275\[h(-x-) \leftarrow b_1(-x_1-), b_2(-x_2-), ... ,b_N(-x_n-);\]
 1276into the internal form (assuming that $h$ is not negated)
 1277\begin{prolog}
 1278$ex\_tru\_h(-x-,ths(T_0,T_n,D_0,D_n), anc(P,N), ans(A_0,A_n)) $\IF
 1279$ex\_tru\_b_1(-x_1-,ths(T_0,T_1,D_0,D_1), anc([h(-x-)|P],N), ans(A_0,A_1))$\AND
 1280$ex\_tru\_b_2(-x_2-,ths(T_1,T_2,D_1,D_2), anc([h(-x-)|P],N), ans(A_1,A_2))$\AND
 1281$...$\AND
 1282$ex\_tru\_b_n(-x_n-,ths(T_{n-1},T_n,D_{n-1},D_n), anc([h(-x-)|P],N),
 1283ans(A_{n-1},A_n)).$
 1284\end{prolog}
 1285That is, we explain $h$ if we explain each of the $b_i$,
 1286accumulating the explanations ',' the answers.
 1287Note that if $h$ is negated, then the head of the clause will be of
 1288the form $ex\_not\_h$, ',' the ancestor form will be
 1289$anc(P,[h(-x-)|N])$. If any of the $b_i$ are negated, then the
 1290corresponding predicate will be $ex\_not\_b_i$.
 1291
 1292\begin{example}\em
 1293the rule
 1294\begin{quote}
 1295$gr(X,Y) \leftarrow f(X,Z), p(Z,Y)$
 1296\end{quote}
 1297gets translated into
 1298\begin{prolog}
 1299$ex\_tru\_gr(X,Y,ths(D,E,F,G),anc(H,I),ans(J,K))$\IF
 1300$ex\_tru\_f(X,Z,ths(D,M,F,N),anc([gr(X,Y)|H],I),ans(J,O))$\AND
 1301$ex\_tru\_p(Z,Y,ths(M,E,N,G),anc([gr(X,Y)|H],I),ans(O,K)).$
 1302\end{prolog}
 1303To explain $gr$ we explain both $f$ ',' $p$.
 1304The initial assumptions for $f$ should be the initial assumptions for
 1305$gr$, ',' the initial assumptions for $p$ should be the initial assumptions
 1306plus those made to explain $f$. The resulting assumptions after proving $p$ are
 1307are the assumptions made in explaining $gr$.
 1308\end{example}
 1309
 1310\begin{example} \em the fact
 1311\begin{quote}
 1312$father(randy,jodi)$
 1313\end{quote}
 1314gets translated into
 1315\begin{quote}
 1316$ex\_tru\_father(randy,jodi,ths(T,T,D,D),\_,ans(A,A)).$
 1317\end{quote}
 1318We can explain $father(randy,jodi)$ independently of the ancestors;
 1319we need no extra assumptions, ',' we create no extra answers.
 1320\end{example}
 1321
 1322Similarly we translate rules of the form
 1323\[h(-x-) \leftarrow b_1(-x_1-), b_2(-x_2-), ... ,b_N(-x_n-);\]
 1324into
 1325\begin{prolog}
 1326$prv\_tru\_h(-x-, T, anc(P,N))$\IF
 1327$prv\_tru\_b_1(-x_1-,T,anc([h(-x-)|P],N))$\AND
 1328$...$\AND
 1329$prv\_tru\_b_n(-x_n-,T,anc([h(-x-)|P],N)).$
 1330\end{prolog}
 1331
 1332\begin{example} \em the rule
 1333\begin{quote}
 1334$gr(X,Y) \leftarrow f(X,Z), p(Z,Y)$
 1335\end{quote}
 1336gets translated into
 1337\begin{prolog}
 1338$prv\_tru\_gr(X,Y,D,anc(H,I))$\IF
 1339$prv\_tru\_f(X,Z,D,anc([gr(X,Y)|H],I))$\AND
 1340$prv\_tru\_p(Z,Y,D,anc([gr(X,Y)|H],I)).$
 1341\end{prolog}
 1342That is, we can prove $gr$ if we can prove $f$ ',' $p$.
 1343Having $gr(X,Y)$ in the ancestors means that we can prove $gr(X,Y)$
 1344by assuming that $\neg gr(X,Y)$ ',' then proving $gr(X,Y)$.
 1345\end{example}
 1346
 1347\begin{example} \em the fact
 1348\begin{quote}
 1349$father(randy,jodi)$
 1350\end{quote}
 1351gets translated into
 1352\begin{quote}
 1353$prv\_tru\_father(randy,jodi,\_,\_).$
 1354\end{quote}
 1355Thus we can prove $father(randy,jodi)$ for any explanation ','
 1356for any ancestors.
 1357\end{example}
 1358
 1359Disjuncts in the source body (;) get mapped into Prolog's disjunction.
 1360The answers ',' assumed hypotheses should be accumulated from
 1361whichever branch was taken.
 1362This is then executed without mapping out subterms.
 1363\begin{example} \em
 1364The rule
 1365\begin{quote}
 1366$p(A) \leftarrow q(A),(r(A),s(A);t(A)),m(A).$
 1367\end{quote}
 1368gets translated into
 1369\begin{tabbing}\hbox{2cm}\=\hbox{1cm}\=\kill
 1370$prv\_tru\_p(A,B,anc(C,D)):-$\\
 1371\>$prv\_tru\_q(A,B,anc([p(A)|C],D)),$\\
 1372\>(\>$prv\_tru\_r(A,B,anc([p(A)|C],D)),$\\
 1373\>\>$prv\_tru\_s(A,B,anc([p(A)|C],D))$\\
 1374\>;\>$prv\_tru\_t(A,B,anc([p(A)|C],D))),$\\
 1375\>$prv\_tru\_m(A,B,anc([p(A)|C],D)).$\\\\
 1376
 1377$ex\_tru\_p(A,ths(B,C,D,E),anc(F,G),ans(H,I)):-$\\
 1378\>$ex\_tru\_q(A,ths(B,J,D,K),anc([p(A)|F],G),ans(H,L)),$\\
 1379\>(\>$ex\_tru\_r(A,ths(J,M,K,N),anc([p(A)|F],G),ans(L,O)),$\\
 1380\>\>$ex\_tru\_s(A,ths(M,P,N,Q),anc([p(A)|F],G),ans(O,R))$\\
 1381\>;\>$ex\_tru\_t(A,ths(J,P,K,Q),anc([p(A)|F],G),ans(L,R))),$\\
 1382\>$ex\_tru\_m(A,ths(P,C,Q,E),anc([p(A)|F],G),ans(R,I))$
 1383\end{tabbing}
 1384Note that $P$ is the resulting explanation from either executing
 1385$r$ ',' $s$ ';' executing $t$ from the explanation $J$.
 1386\end{example}
 1387
 1388\subsubsection{The Code to Compile Rules}
 1389The following relation builds the desired structure for the bodies:
 1390\[make\_bodies(B,T,[Ths,Anc,Ans],ProveB,ExB)\]
 1391where $B$ is a disjunct/conjunct of literals (the body
 1392of the rule), $T$ is a theory for the proving,
 1393$Ths$ is a theory structure for explaining,
 1394$Anc$ is an ancestor
 1395structure (of form $anc(P,N)$), $Ans$ is an answer structure
 1396(of form $ans(A0,A1)$). This procedure
 1397makes $ProveB$ the body of forms $prv\_tru\_b_i$ (',' $prv\_not\_b_i$),
 1398',' $ExB$ a body of the forms $ex\_tru\_b_i$.
 1399
 1400\index{make\_bodies}
 1401\begin{verbatim} */
 1402
 1403
 1404make_bodies(CoA,(H,B), T, [ths(T1,T3,D1,D3), Anc, ans(A1,A3)],
 1405                    (ProveH,ProveB), (ExH,ExB)) :-
 1406   !,
 1407   make_bodies(CoA,H,T,[ths(T1,T2,D1,D2),Anc,ans(A1,A2)],ProveH,ExH),
 1408   make_bodies(CoA,B,T,[ths(T2,T3,D2,D3),Anc,ans(A2,A3)],ProveB,ExB).
 1409
 1410make_bodies(CoA,(H;B),T,Ths,(ProveH;ProveB),(ExH;ExB)) :-
 1411   !,
 1412   make_bodies(CoA,H,T,Ths,ProveH,ExH),
 1413   make_bodies(CoA,B,T,Ths,ProveB,ExB).
 1414
 1415
 1416make_bodies(callable,not(Builtin),_,[ths(T,T,D,D),_,ans(A,A)], \+ Builtin, \+ Builtin) :- is_thbuiltin(Builtin),!.
 1417make_bodies(_CoA,not(A), T, [Ths,Anc,Ans], ProveA, ExA) :-
 1418   !, trace,
 1419   new_lit(`prv_not_`, A, [T,Anc], ProveA),
 1420   new_lit(`ex_not_`, A, [Ths,Anc,Ans], ExA).
 1421
 1422make_bodies(_CoA,Builtin,_,[ths(T,T,D,D),_,ans(A,A)],Builtin,Builtin) :- is_thbuiltin(Builtin),!.
 1423make_bodies(_CoA,A, T, [Ths,Anc,Ans], ProveA, ExA) :- 
 1424   !, trace,
 1425   new_lit(`prv_tru_`, A, [T,Anc], ProveA),
 1426   new_lit(`ex_tru_`, A, [Ths,Anc,Ans], ExA).
 1427
 1428
 1429:- dynamic(declared_as_prolog/1). 1430is_thbuiltin(V):- is_ftVar(V),fail.
 1431is_thbuiltin(true).
 1432is_thbuiltin(unifii(_,_)).
 1433is_thbuiltin( \+ (_)).
 1434is_thbuiltin(call(_)).
 1435is_thbuiltin('{}'(_)).
 1436is_thbuiltin(G):-declared_as_prolog(G).
 1437
 1438
 1439/* \end{verbatim}
 1440
 1441The procedure $rule(F,R)$ declares $R$ to be a fact
 1442';' constraint rule (depending on the value of $F$).
 1443Constraints can only be used for proving;
 1444facts can be used for explaining as well as proving.
 1445$R$ is either a literal ';' of the form $<-(H,B)$ where $H$ is a literal
 1446',' $B$ is a body.
 1447
 1448This $rule$ first checks to see whether we want sound unification ','
 1449then uses $drule(F,R)$ to decare the rule.
 1450
 1451$prolog\_cl(C)$ is a way of asserting to Prolog the clause $C$.
 1452This can either be asserted ';' written to a file to be consulted
 1453';' compiled. The simplest form is to just assert $C$.
 1454
 1455$make\_anc(H)$ is a procedure which ensures that the ancestor search
 1456is set up properly for $H$. It is described in section \ref{anc-section},
 1457',' can be ignored on first reading.
 1458
 1459\index{rule}
 1460\index{drule}
 1461\begin{verbatim} */
 1462
 1463drule(X):- default(X).
 1464
 1465rule(F,R) :- fail, 
 1466   flagth((sound_unification,on)),!,
 1467   make_sound(R,S),
 1468   drule(F,S).
 1469rule(F,R) :-
 1470   drule(F,R).
 1471
 1472drule(_F,<-(H,B)):-
 1473   prolog_cl((H:-B)),!.
 1474/*
 1475drule(F,<-(H,B)) :-
 1476   !,
 1477   make_anc(H),
 1478   make_bodies(assertable,H,T,[Ths,Anc,Ans],ProveH,ExH),
 1479   form_anc(H,Anc,Newanc),
 1480   make_bodies(callable,B,T,[Ths,Newanc,Ans],ProveB,ExB),
 1481   prolog_cl((ProveH:-ProveB)),
 1482   ( F= (fact),
 1483     prolog_cl((ExH:-ExB))
 1484   ; F= (constraint)).
 1485*/
 1486drule(_F,H) :-
 1487  % make_anc(H),
 1488   % make_bodies(assertable,H,T,[ths(T,T,D,D),_,ans(A,A)],ProveH,ExH),
 1489   prolog_cl(H).
 1490
 1491
 1492/* \end{verbatim}
 1493
 1494$form\_anc(L,A1,A2)$ means that $A2$ is the ancestor form for
 1495subgoal $L$ with previous ancestor form $A1$.
 1496
 1497\index{form\_anc}
 1498\begin{verbatim} */
 1499
 1500
 1501form_anc(not(G), anc(P,N), anc(P,[G|N])) :- !.
 1502form_anc(G, anc(P,N), anc([G|P],N)).
 1503
 1504
 1505/* \end{verbatim}
 1506\subsection{Forming Contrapositives}
 1507For both facts ',' constraints we convert the user
 1508syntax into negation normal
 1509form (section \ref{nnf}), form the contrapositives,
 1510',' declare these as rules.
 1511
 1512Note that here we choose an arbitrary ordering for the clauses
 1513in the bodies of the contrapositive forms of the facts. No
 1514attempt has been made to optimise this, although it is noted that some
 1515orderings are more efficient than others (see for example \cite{smith86}
 1516for a discussion of such issues).
 1517
 1518The declarations are as follows:
 1519\index{declare\_fact}
 1520\index{declare\_constraint}
 1521\begin{verbatim} */
 1522
 1523
 1524declare_fact(PNF) :-
 1525   removeQ(PNF,[], UnQ),
 1526   nnf(UnQ,N),
 1527   %wdmsgl(nnf=N),
 1528   rulify(fact,N).
 1529
 1530declare_constraint(C) :-
 1531   nnf(C,N),
 1532   % wdmsgl(cnnf=N),
 1533   rulify(constraint,N).
 1534
 1535
 1536/* \end{verbatim}
 1537
 1538{\em nnf\/$($Wff,Parity,Nnf\/$)$} (section \ref{nnf})
 1539means that {\em Nnf\/} is the negation normal form
 1540of {\em Wff} if {\em Parity=even} ',' of $\neg${\em Wff}
 1541if {\em Parity=odd}. Note that we {\em rulify} the normal form
 1542of the negation of the formula.
 1543
 1544{\em rulify\/}$(H,N)$ where $H$ is
 1545either ``{\em fact\/}'' ';' ``{\em constraint\/}''
 1546',' $N$ is the negation of a fact ';' constraint
 1547in negation normal form (see section \ref{nnf}),
 1548means that all rules which can be formed from $N$ (by allowing each
 1549atom in $N$ being the head of some rule) should be declared as such.
 1550\index{rulify}
 1551\begin{verbatim} */
 1552
 1553
 1554rulify(H,(A,B)) :- !,
 1555   contrapos(H,B,A),
 1556   contrapos(H,A,B).
 1557
 1558rulify(H,(A;B)) :- !,
 1559   rulify(H,A),
 1560   rulify(H,B).
 1561
 1562rulify(H,not(A)) :- !,
 1563   rule(H,A).
 1564
 1565rulify(H,A) :-
 1566   rule(H,not(A)).
 1567
 1568
 1569/* \end{verbatim}
 1570
 1571$contrapos(H,D,T)$ where $H$ is either ``{\em fact\/}'' 
 1572';' ``{\em constraint\/}'', ',' $(D,T)$ is (the negation of)
 1573a formula in negation normal form means that all rules
 1574which can be formed from $(D,T)$ with head of the rule coming from $T$
 1575should be formed.
 1576Think of $D$ as the literals for which the rules with them as heads
 1577have been formed, ',' $T$ as those which remain to be as the head of
 1578some rule.
 1579\index{contrapos}
 1580\begin{verbatim} */
 1581
 1582
 1583contrapos(H,D, (L,R)) :- !,
 1584   contrapos(H,(R,D),L),
 1585   contrapos(H,(L,D),R).
 1586
 1587contrapos(H,D,(L;R)) :- !,
 1588   contrapos(H,D,L),
 1589   contrapos(H,D,R).
 1590
 1591contrapos(H,D,not(A)) :- !,
 1592   rule(H,<-(A,D)).
 1593
 1594contrapos(H,D,A) :-
 1595   rule(H,<-(not(A),D)).
 1596
 1597
 1598/* \end{verbatim}
 1599\begin{example} \em
 1600if we are to {\em rulify} the negation normal form
 1601\begin{quote}
 1602$n(p(A)),q(A),(r(A),s(A);t(A)),m(A)$
 1603\end{quote}
 1604we generate the following rule forms, which can then be given to {\em rule}
 1605\begin{quote}
 1606$p(A)\leftarrow q(A),(r(A),s(A);t(A)),m(A)$\\
 1607$n(q(A))\leftarrow (r(A),s(A);t(A)),m(A),n(p(A))$\\
 1608$n(r(A))\leftarrow s(A),m(A),q(A),n(p(A))$\\
 1609$n(s(A))\leftarrow r(A),m(A),q(A),n(p(A))$\\
 1610$n(t(A))\leftarrow m(A),q(A),n(p(A))$\\
 1611$n(m(A))\leftarrow (r(A),s(A);t(A)),q(A),n(p(A))$
 1612\end{quote}
 1613\end{example}
 1614\subsection{Sound Unification}
 1615Sound unification works, by checking for repeated variables in the left
 1616hand side of a rule, ',' then unifies them by hand. This idea was stolen from 
 1617Stickel's implementation.
 1618
 1619\index{make\_sound}
 1620\index{rms}
 1621\begin{verbatim} */
 1622
 1623dmiles.
 1624
 1625make_sound(I,I):- dmiles, !.
 1626
 1627make_sound(<-(H,B),<-(NH,NB)) :- !,
 1628   rms(H,NH,[],_,B,NB).
 1629
 1630make_sound(H,NR) :-
 1631   rms(H,NH,[],_,true,NB),
 1632   (NB=true,NR=H;
 1633    NR= '<-'(NH,NB)),!.
 1634
 1635rms(V,V1,L,L,B,(unifii(V,V1),B)) :-
 1636   var(V),
 1637   id_member(V,L),!.
 1638rms(V,V,L,[V|L],B,B) :-
 1639   var(V),!.
 1640rms([H|T],[H1|T1],L1,L3,B1,B3) :- !,
 1641   rms(H,H1,L1,L2,B1,B2),
 1642   rms(T,T1,L2,L3,B2,B3).
 1643rms(A,A,L,L,B,B) :-
 1644   atomic(A),!.
 1645rms(S,S2,L1,L2,B1,B2) :-
 1646   S =.. L,
 1647   rms(L,LR,L1,L2,B1,B2),
 1648   S2 =.. LR.
 1649
 1650
 1651/* \end{verbatim}
 1652
 1653\index{unifii}
 1654\index{appears\_in}
 1655\begin{verbatim} */
 1656
 1657unifii(X,Y) :- unify_with_occurs_check(X,Y).
 1658/*
 1659unifii(X,Y) :-
 1660   var(X), var(Y), X=Y,!.
 1661unifii(X,Y) :-
 1662   var(X),!,
 1663   \+ appears_in(X,Y),
 1664   X=Y.
 1665unifii(X,Y) :-
 1666   var(Y),!,
 1667   \+ appears_in(Y,X),
 1668   X=Y.
 1669unifii(X,Y) :-
 1670   atomic(X),!,X=Y.
 1671unifii([H1|T1],[H2|T2]) :- !,
 1672   unifii(H1,H2),
 1673   unifii(T1,T2).
 1674unifii(X,Y) :-
 1675   \+ atomic(Y),
 1676   X=..XS,
 1677   Y=..YS,
 1678   unifii(XS,YS).
 1679
 1680appears_in(X,Y) :-
 1681   var(Y),!,X==Y.
 1682appears_in(X,[H|T]) :- !,
 1683   (appears_in(X,H); appears_in(X,T)).
 1684appears_in(X,S) :-
 1685   \+ atomic(S),
 1686   S =.. L,
 1687   appears_in(X,L).
 1688*/
 1689
 1690/* \end{verbatim}
 1691\subsection{Possible Hypotheses}
 1692The other class of things we have to worry about is the class
 1693of possible hypotheses. As described in \cite{poole:lf}
 1694',' outlined in section \ref{theorist},
 1695we only need worry about atomic possible hypotheses.
 1696
 1697If $d(-args-)$ is a possible hypothesis (default),
 1698then we want to form the target code as follows:
 1699
 1700\begin{enumerate}
 1701\item We can only prove a hypothesis if we have already assumed it:
 1702\begin{prolog}
 1703$prv\_tru\_d(-args-,Ths,Anc) $\IF
 1704$member(d(-args-),Ths).$
 1705\end{prolog}
 1706\item We can explain a default if we have already assumed it:
 1707\begin{prolog}
 1708$ex\_tru\_d(-args-,ths(T,T,D,D),Anc,ans(A,A)) $\IF
 1709$member(d(-args-),T).$
 1710\end{prolog}
 1711\item We can explain a hypothesis by assuming it,
 1712if it has no free variables, we have not
 1713already assumed it ',' it is consistent with everything assumed before:
 1714\begin{prolog} \em
 1715$ex\_tru\_d(-args-,ths(T,[d(-args-)|T],D,D),Anc,ans(A,A)) $\IF
 1716variable\_free$(d(-args-))$\AND
 1717$\backslash+(member(d(-args-),T))$\AND
 1718$\backslash+(prv\_not\_d(-args-,[d(-args-)|T],anc([],[]))).$
 1719\end{prolog}
 1720\item 
 1721If a hypothesis has free variables, it can be explained
 1722by adding it to the deferred defaults list (making no assumptions about
 1723its consistency; this will be checked at the end of the explanation phase):
 1724\begin{prolog}
 1725$ex\_tru\_d(-args-,ths(T,T,D,[d(-args-)|D],Anc,ans(A,A)) $\IF
 1726$\backslash+($variable\_free$(d(-args-))).$
 1727\end{prolog}
 1728\end{enumerate}
 1729
 1730The following compiles directly into such code:
 1731\index{declare\_default}
 1732\begin{verbatim} )*/
 1733
 1734
 1735declare_default(D) :-
 1736   make_anc(D),
 1737   new_lit(`prv_tru_`,D,[T,_],Pr_D),
 1738   prolog_cl((Pr_D :- member(D,T))),
 1739   new_lit(`ex_tru_`,D, [ths(T,T,Defer,Defer), _, ans(A,A)], ExD),
 1740   prolog_cl((ExD :- member(D, T))),
 1741   new_lit(`ex_tru_`,D, [ths(T,[D|T],Defer,Defer), _, ans(A,A)], ExDass),
 1742   new_lit(`prv_not_`,D, [[D|T],anc([],[])],Pr_not_D),
 1743   prolog_cl((ExDass :- variable_free(D), \+member(D,T),
 1744                 \+Pr_not_D)),
 1745   new_lit(`ex_tru_`,D, [ths(T,T,Defer,[D|Defer]), _, ans(A,A)], ExDefer),
 1746   prolog_cl((ExDefer :- \+ variable_free(D))).
 1747
 1748
 1749/* \end{verbatim}
 1750
 1751\begin{example}\em
 1752The default
 1753\begin{quote} \em
 1754birdsfly$(A)$
 1755\end{quote}
 1756gets translated into \em
 1757\begin{prolog}
 1758prv\_tru\_birdsfly$(A,B,C):-$\\
 1759\>member$(\hbox{birdsfly}(A),B)$\\
 1760ex\_tru\_birdsfly$(A,ths(B,B,C,C),D,ans(E,E)):-$\\
 1761\>member$(\hbox{birdsfly}(A),B)$\\
 1762ex\_tru\_birdsfly$(A,ths(B,[\hbox{birdsfly}(A)|B],C,C),D,ans(E,E)):-$\\
 1763\>variable\_free$(\hbox{birdsfly}(A)) ,$\\
 1764\>$\backslash+$member$(\hbox{birdsfly}(A),B),$\\
 1765\>$\backslash+$prv\_not\_birdsfly$(A,[\hbox{birdsfly}(A)|B],anc([],[]))$\\
 1766ex\_tru\_birdsfly$(A,ths(B,B,C,[\hbox{birdsfly}(A)|C]),D,ans(E,E)):- $\\
 1767\>$\backslash+$variable\_free$(\hbox{birdsfly}( A))$
 1768\end{prolog}
 1769\end{example}
 1770\subsection{Relations defined in Prolog}
 1771We can define some relations to be executed in Prolog.
 1772This means that we can prove the $prove$ ',' $ex$ forms by calling 
 1773the appropriate Prolog definition.
 1774\index{declare\_prolog}
 1775\begin{verbatim} */
 1776            
 1777declare_prolog(G) :- declared_as_prolog(G),!.
 1778declare_prolog(G) :-
 1779   prolog_cl(declared_as_prolog(G)),
 1780   new_lit(`ex_tru_`,G, [ths(T,T,D,D), _, ans(A,A)], ExG),
 1781   prolog_cl((ExG :- G)),
 1782   new_lit(`prv_tru_`,G,[_,_],PrG),
 1783   prolog_cl((PrG :- G)),!.
 1784
 1785
 1786/* \end{verbatim}
 1787
 1788\subsection{Explaining Observations}
 1789$expl(G,T0,T1,A)$ means that $T1$ is an explanation of $G$ ';' $A$ ($A$ being
 1790the alternate answers) from the facts given $T0$ is already assumed.
 1791$G$ is an arbitrary wff.
 1792\index{expl}
 1793\begin{verbatim} */
 1794
 1795
 1796expl(G,T0,T1,Ans) :-
 1797   trace, make_ground(N),
 1798   once(declare_fact('<-'(newans(N,G) , G))),
 1799     ex_tru_newans(N,G,ths(T0,T,[],D),anc([],[]),ans([],Ans)),
 1800   make_ground(D),
 1801   check_consis(D,T,T1).
 1802
 1803
 1804/* \end{verbatim}
 1805
 1806\index{check\_consis}
 1807\begin{verbatim} */
 1808
 1809
 1810check_consis([],T,T).
 1811check_consis([H|D],T1,T) :-
 1812   new_lit(`prv_not_`,H, [T1,anc([],[])], Pr_n_H),
 1813   \+ Pr_n_H,
 1814   check_consis(D,[H|T1],T).
 1815
 1816
 1817/* \end{verbatim}
 1818To obtain disjunctive answers we have to know if the negation of the top
 1819level goal is called. This is done by declaring the fact
 1820$newans(G) \leftarrow G$, ',' if we ever try to
 1821prove the negation of a top level goal, we add that instance to the
 1822list of alternate answers. In this implementation we also check
 1823that $G$ is not identical to a higher level goal. This removes most cases
 1824where we have a redundant assumption (i.e., when we are not gaining a new
 1825answer, but only adding redundant information).
 1826\index{ex\_not\_newans}
 1827\index{id\_anc}
 1828\begin{verbatim} */
 1829
 1830
 1831:- dynamic ex_not_newans/5. 1832:- dynamic ex_tru_newans/5. 1833:- dynamic prv_not_newans/4. 1834ex_not_newans(N,G,ths(T,T,D,D),anc(Pos,Neg),ans(A,[G|A])) :-
 1835   member(newans(N,_),Pos),
 1836   \+ id_anc(G,anc(Pos,Neg)).
 1837
 1838id_anc(not(G),anc(_,N)) :- !, id_member(G,N).
 1839id_anc(G,anc(P,_)) :- id_member(G,P).
 1840
 1841
 1842/* \end{verbatim}
 1843
 1844\subsection{Ancestor Search} \label{anc-section}
 1845Our linear resolution
 1846theorem prover must recognise that a goal has been proven if
 1847it unifies with an ancestor in the search tree. To do this, it keeps
 1848two lists of ancestors, one containing the positive (non negated)
 1849ancestors ',' the other the negated ancestors.
 1850When the ancestor search rules for predicate $p$ are defined, we assert
 1851{\em ancestor\_recorded(p)}, so that we do not attempt to redefine the
 1852ancestor search rules.
 1853\index{make\_ex\_tru\_anc}
 1854\index{flagth,ancestor\_search}
 1855\index{flagth,loop\_check}
 1856\begin{verbatim} */
 1857
 1858
 1859:- dynamic ancestor_recorded/1. 1860ancestor_recorded(P):-is_thbuiltin(P). 
 1861
 1862make_anc(_) :-
 1863   flagth((ancestor_search,off)),
 1864   flagth((loop_check,off)),
 1865   flagth((depth_bound,off)),
 1866   !.
 1867make_anc(Name) :-
 1868   ancestor_recorded(Name),
 1869   !.
 1870make_anc(not(Goal)) :-
 1871   !,
 1872   make_anc(Goal).
 1873
 1874make_anc(Goal) :-
 1875   Goal =.. [Pred|Args],
 1876   same_length_nnf(Args,Nargs),
 1877   NG =.. [Pred|Nargs],
 1878   make_bodies(assertable,NG,_,[ths(T,T,D,D),anc(P,N),ans(A,A)],ProveG,ExG),
 1879   make_bodies(assertable,not(NG),_,[ths(T,T,D,D),anc(P,N),ans(A,A)],ProvenG,ExnG),
 1880   ( flagth((loop_check,off))
 1881   ;
 1882     prolog_cl((ProveG :- id_member(NG,P),!,fail)),
 1883     prolog_cl((ProvenG :- id_member(NG,N),!,fail)),
 1884     prolog_cl((ExG :- id_member(NG,P),!,fail)),
 1885     prolog_cl((ExnG :- id_member(NG,N),!,fail))
 1886   ),
 1887   ( flagth((ancestor_search,off))
 1888   ;
 1889     prolog_cl((ProveG :- member(NG,N))),
 1890     prolog_cl((ProvenG :- member(NG,P))),
 1891     prolog_cl((ExG :- member(NG,N))),
 1892     prolog_cl((ExnG :- member(NG,P)))
 1893   ),
 1894   ( flagth((depth_bound,off)), !
 1895   ;
 1896     prolog_cl((ProveG :- (flagth((depth_bound,MD))),
 1897            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1898     prolog_cl((ProvenG :- (flagth((depth_bound,MD))),
 1899            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1900     prolog_cl((ExG :- (flagth((depth_bound,MD))),
 1901            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1902      prolog_cl((ExnG :- (flagth((depth_bound,MD))),
 1903            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail))
 1904   ),
 1905   assert(ancestor_recorded(NG)),
 1906   !.
 1907
 1908
 1909/* \end{verbatim}
 1910
 1911\begin{example} \em
 1912If we do a call
 1913\begin{quote}
 1914make\_anc(gr(A,B))
 1915\end{quote}
 1916we create the Prolog clauses
 1917\begin{prolog}
 1918prv\_tru\_gr(A,B,C,anc(D,E))\IF
 1919member(gr(A,B),E).\\
 1920prv\_not\_gr(A,B,C,anc(D,E))\IF
 1921member(gr(A,B),D).\\
 1922ex\_tru\_gr(A,B,ths(C,C,D,D),anc(E,F),ans(G,G))\IF
 1923member(gr(A,B),F).\\
 1924ex\_not\_gr(A,B,ths(C,C,D,D),anc(E,F),ans(G,G))\IF
 1925member(gr(A,B),E).
 1926\end{prolog}
 1927This is only done once for the $gr$ relation.
 1928\end{example}
 1929
 1930\section{Interface}
 1931In this section a minimal interface is given. We try to give
 1932enough so that we can understand the conversion of the wff form
 1933into negation normal form ','
 1934the parsing of facts ',' defaults. There is, of course,
 1935much more in any usable interface than described here.
 1936\subsection{Syntax Declarations}
 1937All of the declarations we use will be defined as operators.
 1938This will allow us to use infix forms of our wffs, for extra readability.
 1939Here we use the standard Edinburgh operator declarations which are
 1940given in the spirit of being enough to make the rest of the description
 1941self contained.
 1942\begin{verbatim} */
 1943
 1944     
 1945:- dynamic((flagth)/1). 1946:- op(1150,fx,'drule'). 1947:- op(1150,fx,'default'). 1948:- op(1150,fx,'fact'). 1949:- op(1150,fx,constraint). 1950%:- op(1150,fx,prolog).
 1951:- op(1150,fx,explain). 1952:- op(1150,fx,predict). 1953:- op(1150,fx,define). 1954:- op(1150,fx,set). 1955:- op(1150,fx,flagth). 1956:- op(1150,fx,reset). 1957:- op(1150,fy,h). 1958:- op(1150,fx,thconsult). 1959:- op(1150,fx,thtrans). 1960:- op(1150,fx,thcompile). 1961%:- op(1130,xfx,:).
 1962
 1963/*
 1964:- op(1120,xfx,==).
 1965:- op(1120,xfx,<=>).
 1966:- op(1120,xfx,equiv).
 1967*/
 1968:- op(1110,xfx,<-). 1969/*
 1970:- op(1110,xfx,=>).
 1971:- op(1000,xfy,&).
 1972:- op(1100,xfy,';').
 1973:- op(1000,xfy,',').
 1974:- op(950,fy,~).
 1975*/
 1976:- op(950,fy,not). 1977
 1978
 1979/* \end{verbatim}
 1980
 1981
 1982\subsection{Converting to Negation Normal Form} \label{nnf}
 1983We want to convert an arbitrarily complex formula into a standard form
 1984called {\em negation normal form\/}. Negation normal form of a formula is
 1985an equivalent formula consisting of conjunctions ',' disjunctions of
 1986literals (either an atom ';' of the form $n(A)$ where $A$ is an atom).
 1987The relation defined here puts formulae into negation normal form
 1988without mapping out subterms.
 1989Usually we want to find the negation normal form of the negation of the
 1990formula, as this is the form suitable for use in the body of a rule.
 1991
 1992The predicate used is of the form
 1993\[nnf(Fla,Parity,Body)\]
 1994where
 1995\begin{description}
 1996\item[$Fla$] is a formula with input syntax
 1997\item[$Parity$] is either $odd$ ';' $even$ ',' denotes whether $Fla$ is
 1998in the context of an odd ';' even number of negations.
 1999\item[$Body$] is a tuple which represents the negation normal form
 2000of the negation of $Fla$
 2001if parity is even ',' the negation normal form of $Fla$ if parity is odd. 
 2002\end{description}
 2003\index{nnf}
 2004\begin{verbatim} */
 2005
 2006nnf(F,odd,FF):- var_or_atomic(F), !, xlit(F,FF).
 2007nnf(F,even,not(FF)):- var_or_atomic(F), !, xlit(F,FF).
 2008
 2009nnf('<->'(X , Y), P,B) :- !,
 2010   nnf(((Y ; not(X)) , (X ; not(Y))),P,B).
 2011nnf((X == Y), P,B) :- compound(X), compound(Y), !, nnf('<->'(X , Y), P,B).
 2012
 2013nnf(all(_, Y), P,B) :- !,nnf(Y, P,B).
 2014nnf(exists(E, Y), P, exists(E, B)) :- !,nnf(Y, P,B).
 2015
 2016nnf('->'(X,Y), P,B) :- !,
 2017   nnf((Y ; not(X)),P,B).
 2018
 2019nnf(','(X, Y),P,B) :- !,
 2020   opposite_parity(P,OP),
 2021   nnf((not(X) ; not(Y)),OP,B).
 2022
 2023nnf((X | Y), P,B) :- !, nnf(xor(X,Y),P,B).
 2024nnf(xor(X, Y), P,B) :- !, nnf(';'(','(not(X),Y),','(X,not(Y))),P,B).
 2025
 2026
 2027nnf(';'(X,Y),even,(XB,YB)) :- !,
 2028   nnf(X,even,XB),
 2029   nnf(Y,even,YB).
 2030nnf(';'(X,Y),odd,(XB;YB)) :- !,
 2031   nnf(X,odd,XB),
 2032   nnf(Y,odd,YB).
 2033
 2034nnf('~'( X),P,B) :- !,
 2035   nnf((not(X)),P,B).
 2036
 2037nnf((not(X)),P,B) :- !,
 2038   opposite_parity(P,OP),
 2039   nnf(X,OP,B).
 2040
 2041% nnf((Y <- X), P,B) :-  !, nnf((Y ';' not(X)),P,B).
 2042nnf(not(F),even,FF) :- !,xlit(F,FF).
 2043nnf(F,odd,FF):- xlit(F,FF).
 2044nnf(F,even,not(FF)):- xlit(F,FF).
 2045
 2046xlit(F,F):- \+ compound(F),!.
 2047xlit({X},{X}).
 2048xlit(=(A,B),equals(A,B)).
 2049xlit(neq(A,B),{dif(A,B)}).
 2050xlit(\=(A,B),{dif(A,B)}).
 2051xlit(>(A,B),comparison(A,B,>)).
 2052xlit(<(A,B),comparison(A,B,<)).
 2053xlit(>=(A,B),comparison(A,B,>=)).
 2054xlit(=<(A,B),comparison(A,B,=<)).
 2055xlit([F|Args],OUT):- maplist(xlit,[F|Args],OUT).
 2056xlit(P,PP):- 
 2057  compound_name_arguments(P,F,Args),
 2058  maplist(xlit,Args,FArgs),
 2059  compound_name_arguments(PP,F,FArgs).
 2060
 2061
 2062/* \end{verbatim}
 2063\index{opposite\_parity}
 2064\begin{verbatim} */
 2065
 2066
 2067opposite_parity(even,odd).
 2068opposite_parity(odd,even).
 2069
 2070
 2071/* \end{verbatim}
 2072
 2073\begin{example} \em
 2074the wff
 2075\begin{quote} \em
 2076(a ';' not b) ',' c $\Rightarrow$ d ',' (not e ';' f)
 2077\end{quote}
 2078with parity {\em odd} gets translated into
 2079\begin{quote}
 2080$d,(e;f);n(a),b;n(c) $
 2081\end{quote}
 2082the same wff with parity {\em even} (i.e., the negation of the wff)
 2083has negation normal form:
 2084\begin{quote}
 2085$(n(d);e,n(f)),(a;n(b)),c$
 2086\end{quote}
 2087\end{example}
 2088
 2089\subsection{Theorist Declarations}
 2090The following define the Theorist declarations.
 2091Essentially these operators just call the appropriate compiler
 2092instruction. These commands cannot be undone by doing a retry to them;
 2093the compiler assertions will be undone on backtracking.
 2094\index{fact}
 2095\begin{verbatim} */
 2096
 2097
 2098fact(F) :- declare_fact(F),!.
 2099
 2100
 2101/* \end{verbatim}
 2102
 2103The $default$ declaration makes the appropriate equivalences between the
 2104named defaults ',' the unnamed defaults.
 2105\index{default}
 2106\begin{verbatim} */
 2107
 2108
 2109
 2110
 2111default((N : H)):-
 2112   !,
 2113   declare_default(N),
 2114   declare_fact((H <-N)),
 2115   !.
 2116default( N ):-
 2117   declare_default(N),
 2118   !.
 2119/* \end{verbatim}
 2120\index{default}
 2121\begin{verbatim} */
 2122
 2123
 2124constraint((C)) :-
 2125   declare_constraint(C),
 2126   !.
 2127/* \end{verbatim}
 2128The $prolog$ command says that the atom $G$ should be proven in the
 2129Prolog system. The argument of the $define$ statement is a Prolog
 2130definition which should be asserted (N.B. that it should be in
 2131parentheses if it contains a ``{\tt :-}''.
 2132\index{prolog}
 2133\begin{verbatim} */
 2134
 2135                                   
 2136prolog(( G )) :-
 2137   declare_prolog(G).
 2138
 2139
 2140/* \end{verbatim}
 2141\index{define}
 2142\begin{verbatim} */
 2143
 2144
 2145define( G ):-
 2146   prolog_cl(G).
 2147
 2148
 2149/* \end{verbatim}
 2150
 2151The $explain$ command keeps writing out all of the explanations found.
 2152This is done by finding one, writing the answer, ',' then retrying so that
 2153the next answer is found. This is done so that the computation is left in
 2154an appropriate state at the end of the computation.
 2155\index{explain}
 2156\begin{verbatim} */
 2157explain_th(G) :- 
 2158  ignore((explain_goal(G)*->fail;(format('~nUntrue: ~p.~n',[G]),forall(explain_goal('~'(G)),true)))).
 2159
 2160explain_goal(G) :-
 2161   (flagth((timing,on))),!,
 2162    statistics(runtime,_),
 2163    expl(G,[],D,A),
 2164    statistics(runtime,[_,Time]),
 2165    writeans(G,D,A),
 2166    format('took ~3d sec.~n~n',[Time])
 2167    
 2168  ;
 2169    expl(G,[],D,A),
 2170    writeans(G,D,A).
 2171/* \end{verbatim}
 2172\index{writeans}
 2173\index{writedisj}
 2174\begin{verbatim} */
 2175
 2176
 2177writeans(G,D,A) :-
 2178   format('~nAnswer is ~p', [G]),
 2179   writedisj(A),
 2180   format('~nTheory is ~p~n', [D]),
 2181   !.
 2182
 2183writedisj([]).
 2184writedisj([H|T]) :-
 2185   writedisj(T),
 2186   format(' not ~p',[H]).
 2187
 2188
 2189/* \end{verbatim}
 2190
 2191\subsection{Prediction}
 2192In \cite{poole:lf} we present a sceptical view of prediction
 2193argue that one should predict what is in every extension.
 2194The following theorem proved in \cite{poole:lf} gives us a hint
 2195as to how it should be implemented.
 2196\begin{theorem} \label{everythm}
 2197$g$ is not in every extension iff there exists a scenario $S$ such
 2198that $g$ is not explainable from $S$.
 2199\end{theorem}
 2200
 2201The intuition is that
 2202if $g$ is not in every extension then there is no reason to rule out
 2203$S$ (based on the information given) ',' so we should not predict $g$.
 2204                      
 2205We can use theorem \ref{everythm} to consider another way to view membership
 2206in every extension. Consider two antagonistic agents $Y$ ',' $N$ trying to
 2207determine whether $g$ should be predicted ';' not. $Y$ comes
 2208up with explanations of $g$, ',' $N$ tries to find where these explanations
 2209fall down (i.e., tries to find a scenario $S$ which is inconsistent with
 2210all of $Y$''s explanations). $Y$ then tries to find an explanation of $g$
 2211given $S$.
 2212If $N$ cannot find a defeater for $Y$'s explanations then
 2213$g$ is in every extension, ',' if $Y$ cannot find an explanation from
 2214some $S$ constructed by $N$ then $g$ is not in every extension.
 2215                                                                       
 2216The following code implements this, but (as we cannot implement
 2217coroutines as needed above in Prolog), it may generate more
 2218explanations of the goal than is needed. What we really want is for the
 2219first ``bagof'' to generate the explanations in a demand-driven fashion,
 2220',' then just print the explanations needed.
 2221
 2222\index{predict}
 2223\begin{verbatim} */
 2224                     
 2225
 2226predict(( G )):-
 2227  bagof(E,expl(G,[],E,[]),Es),
 2228  predct(G,Es). 
 2229 
 2230predct(G,Es) :- 
 2231  simplify_expls(Es,SEs),
 2232    ( find_counter(SEs,[],S),
 2233      !,
 2234      format('No, ~q is not explainable from ~q.~n',[G,S])
 2235    ; format('Yes, ~q is in all extensions.~nExplanations are:~n',[G]),
 2236      list_scens(1,SEs)).
 2237
 2238
 2239/* \end{verbatim}
 2240
 2241\index{find\_counter}
 2242\begin{verbatim} */
 2243
 2244
 2245find_counter([],S,S).
 2246find_counter([E|R],S0,S2) :-
 2247   member(D,E),
 2248   expl2not(D,S0,S1),
 2249   find_counter(R,S1,S2).
 2250
 2251
 2252/* \end{verbatim}
 2253
 2254\index{list\_scens}
 2255\begin{verbatim} */
 2256
 2257
 2258list_scens(_,[]).
 2259list_scens(N,[H|T]) :-
 2260   format('~q: ~q.~n',[N,H]),
 2261   N1 is N+1,
 2262   list_scens(N1,T).
 2263
 2264
 2265/* \end{verbatim}
 2266
 2267$expl2not(G,T0,T1)$ is true if ground $\neg G$ is explainable starting from
 2268scenario $T0$, with resulting explanation $T1$. No disjunctive answers are
 2269formed.
 2270\index{expl2}
 2271\begin{verbatim} */
 2272
 2273
 2274expl2not(G,T0,T1) :-
 2275   new_lit(`ex_not_`,G,[ths(T0,T,[],D),anc([],[]),ans([],[])],ExG),
 2276   ExG,
 2277   trace, make_ground(D),
 2278   check_consis(D,T,T1).
 2279
 2280
 2281/* \end{verbatim}
 2282
 2283\subsection{Simplifying Explanations}
 2284\index{simplify\_obs}
 2285\begin{verbatim} */
 2286                                   
 2287
 2288simplify_expls([S],[S]).
 2289
 2290simplify_expls([H|T], S) :-
 2291   simplify_expls(T, TS),
 2292   mergeinto(H,TS,S).
 2293
 2294
 2295/* \end{verbatim}
 2296\index{mergeinto}
 2297\begin{verbatim} */
 2298
 2299
 2300mergeinto(L,[],[L]).
 2301
 2302mergeinto(L,[A|R],[A|R]) :-
 2303   instance_of(A,L),
 2304   !.
 2305
 2306mergeinto(L,[A|R],N) :-
 2307   instance_of(L,A),
 2308   !,
 2309   mergeinto(L,R,N).
 2310
 2311mergeinto(L,[A|R],[A|N]) :-
 2312   mergeinto(L,R,N).
 2313
 2314                         
 2315/* \end{verbatim}
 2316
 2317\index{instance\_of}
 2318\begin{verbatim} */
 2319
 2320
 2321instance_of(D,S) :-
 2322   remove_all_nnf(D,S,_).
 2323                           
 2324
 2325/* \end{verbatim}
 2326
 2327\subsection{File Handling}
 2328To consult a Theorist file, you should do a,
 2329\begin{verse}
 2330{\bf thconsult} \em filename.
 2331\end{verse}
 2332The following is the definition of {\em thconsult}. Basicly we just
 2333keep reading the file ',' executing the commands in it until we stop.
 2334\index{thconsult}
 2335\begin{verbatim} */
 2336
 2337thconsult(( File0 )):-
 2338   fix_absolute_file_name(File0,File),
 2339   current_input(OldFile),
 2340   open(File,read,Input),
 2341   set_input(Input),
 2342   th_read(T),
 2343   read_all(T),!,
 2344   set_input(OldFile).
 2345
 2346
 2347/* \end{verbatim}
 2348\index{read\_all}
 2349\begin{verbatim} */
 2350
 2351
 2352:- meta_predicate(read_all(*)). 2353read_all(end_of_file) :- !.
 2354
 2355read_all(T) :-
 2356   ((flagth(( asserting,on))),!; format('~n% ~p.~n',[T])),
 2357   (thmust(T) *-> true ; format('% Warning: ~p failed~n',[T])),
 2358   th_read(T2),
 2359   read_all(T2).
 2360
 2361th_read(T):- read_term(T,[module(snark_theorist),variable_names(Vs)/*,double_quotes(codes)*/]),b_setval('$variable_names',Vs).
 2362                 
 2363thmust(G):- call(G),!.
 2364thmust(G):- rtrace(G),!.
 2365
 2366/* \end{verbatim}
 2367
 2368{\em thtrans} is like the previous version, but the generated code is written
 2369to a file. This code is neither loaded ';' compiled.
 2370\index{thtrans}
 2371\begin{verbatim} */
 2372
 2373fix_absolute_file_name(I,O):- is_list(I),!,string_to_atom(I,A),absolute_file_name(A,O).
 2374fix_absolute_file_name(I,O):- absolute_file_name(I,O),!.
 2375fix_absolute_file_name(I,O):- I=O.
 2376
 2377
 2378thtrans(( File0 )):-
 2379   fix_absolute_file_name(File0,File),
 2380   string_codes(File, Fname),
 2381   append(Fname,`.pl`,Plfname),
 2382   name(Plfile, Plfname),
 2383   current_output(Oldoutput),
 2384   open(Plfile,write,Output),
 2385   set_output(Output),
 2386   thtrans2out(File),
 2387   close(Output),
 2388   set_output(Oldoutput),!.
 2389   
 2390
 2391thtrans2out(File0):-
 2392   fix_absolute_file_name(File0,File),
 2393   current_input(Oldinput),
 2394   open(File,read,Input),
 2395   set_input(Input),
 2396   format(':- dynamic contrapos_recorded/1.~n',[]),
 2397   format(':- style_check(- singleton).~n',[]),
 2398   format(':- style_check(- discontiguous).~n',[]),
 2399   (setth((asserting,off))),
 2400   th_read(T),
 2401   read_all(T),
 2402   set_input(Oldinput),
 2403   resetth(( asserting)),!.
 2404
 2405/* \end{verbatim}
 2406To compile a Theorist file, you should do a,
 2407\begin{verse}
 2408{\bf thconsult} \em filename.
 2409\end{verse}
 2410
 2411This translates the code to Prolog ',' then compiles the prolog code.
 2412
 2413{\em thcompile} translates the file to Prolog
 2414which is then compiled using the Prolog compiler.
 2415\index{thcompile}
 2416\begin{verbatim} */
 2417
 2418
 2419thcompile(( File )):-
 2420   (thtrans(( File))),
 2421%   no_style_check(all),
 2422   compile(File).  
 2423
 2424
 2425/* \end{verbatim}
 2426
 2427
 2428\subsection{Flag Setting} \label{flags}
 2429There are a number of Theorist options which can be set by flagth declarations.
 2430Flags, by default, are {\tt on}.
 2431To set the flagth $f$ to value $v$ you can issue the command
 2432\begin{verse}
 2433\bf set $f,v.$
 2434\end{verse}
 2435To find out the value of the flagth $f$ issue the command
 2436\begin{verse}
 2437\bf flagth $f,V.$
 2438\end{verse}
 2439You can reset the value of flagth $f$ to its old value by
 2440\begin{verse}
 2441\bf reset $f.$
 2442\end{verse}
 2443The list of all flags is given by the command
 2444\begin{verse}
 2445\bf flags.
 2446\end{verse}
 2447
 2448The following is the definition of these
 2449\index{set}
 2450\begin{verbatim} */
 2451
 2452
 2453setth((F,V)):-
 2454   prolog_decl((flagth((F,V1)):- !,V=V1)),!.
 2455
 2456
 2457/* \end{verbatim}
 2458\index{flagth}
 2459\begin{verbatim} */
 2460
 2461
 2462flagth((_,on)).
 2463
 2464
 2465/* \end{verbatim}
 2466\index{reset}
 2467\begin{verbatim} */
 2468
 2469
 2470resetth(F) :-
 2471   retract((flagth((F,_)) :- !,_=_)).
 2472
 2473
 2474/* \end{verbatim}
 2475\index{flags}
 2476\begin{verbatim} */
 2477
 2478
 2479flags :- list_flags([asserting,ancestor_search,loop_check,
 2480                     depth_bound,sound_unification,timing]).
 2481list_flags([]).
 2482list_flags([H|T]) :-
 2483   (flagth((H,V))),
 2484   format('flagth((~w,~w)).~n',[H,V]),
 2485   list_flags(T).
 2486                          
 2487
 2488/* \end{verbatim}
 2489\subsection{Compiler Directives}
 2490There are some compiler directives which need to be added to Theorist
 2491code so that the Prolog to assembly language compiler can work
 2492(these are translated into the appropriate Quintus compiler directives).
 2493
 2494So that the Quintus compiler can correctly compile the code,
 2495we should declare that all calls for which we can assert the goal
 2496';' the negative are dynamic, this is done by the command
 2497\begin{verse}
 2498\bf dyn $n.$
 2499\end{verse}
 2500This need only be given in files,
 2501',' should be given before the atomic symbol $n$ is ever used.
 2502
 2503The following gives the appropriate translation.
 2504Essentially we then must say that the appropriate Prolog code is dynamic.
 2505\index{explainable}
 2506\begin{verbatim} */
 2507
 2508
 2509:- op(1150,fx,(dyn)). 2510dyn(not(G)) :-
 2511   !,
 2512   (dyn(G)).
 2513dyn(G):-
 2514   G =.. [R|Args],
 2515   add_prefix(`ex_not_`,R,ExNR),
 2516   add_prefix(`ex_tru_`,R,ExR),
 2517   length(Args,NA),
 2518   ExL is NA + 3,
 2519   decl_dyn(ExNR/ExL),
 2520   decl_dyn(ExR/ExL),
 2521   add_prefix(`prv_not_`,R,PrNR),
 2522   add_prefix(`prv_tru_`,R,PrR),
 2523   PrL is NA + 2,
 2524   decl_dyn(PrNR/PrL),
 2525   decl_dyn(PrR/PrL).
 2526
 2527decl_dyn(F/A) :- (flagth((asserting, on))),!,dynamic(F/A).
 2528decl_dyn(FA):- format(':- dynamic ~q.~n',[FA]).
 2529
 2530
 2531%:- op(1150,fx,explainable).
 2532explainable(G) :- dyn(G). 
 2533
 2534                       
 2535/* \end{verbatim}
 2536
 2537\subsection{Using the Compiled Rules}
 2538The use of conditional asserting (prolog\_cl) is twofold.
 2539The first is to write the condition to a file if that is desired.
 2540The second is to be a backtrackable assert otherwise.
 2541\index{prolog\_cl}
 2542\index{flagth,asserting}
 2543\begin{verbatim} */
 2544
 2545% if_dbg(_G):-true,!.
 2546if_dbg(G):-call(G).
 2547
 2548print_clause(C) :- portray_clause(C).
 2549/*
 2550print_clause(C) :- 
 2551   \+ \+ (    
 2552     tnumbervars(C,0,_),
 2553     writeq(C),
 2554     write('.'),
 2555     nl).
 2556*/
 2557%prolog_cl(({C}:-B)):- !, prolog_cl((C:-B)).
 2558%prolog_cl({C}):- !, prolog_cl(C).
 2559
 2560prolog_cl((C:-B)):- \+ \+ ( C = B),!.
 2561prolog_cl(C) :-    
 2562   flagth((asserting,off)),!,
 2563   print_clause(C),!.
 2564
 2565prolog_cl(C) :-
 2566   prolog_load_context(variable_names,Vs),
 2567   (clause_asserted(C)->! ; ( %trace,
 2568      assertz( saved_clauz(C,Vs)),call(if_dbg(print_clause((C)))))),!.
 2569prolog_cl(C) :-
 2570   if_dbg(print_clause(retract(C))),
 2571   break,retract(C),
 2572   fail.
 2573
 2574
 2575/* \end{verbatim}
 2576$prolog\_decl$ is like the above predicate, but is both
 2577written to the file ',' asserted.
 2578\index{prolog\_decl}
 2579\begin{verbatim} */
 2580                     
 2581
 2582prolog_decl(C) :-
 2583   flagth((asserting,off)),
 2584   print_clause(C),
 2585   fail.
 2586prolog_decl(C) :-
 2587   asserta(C).
 2588prolog_decl(C) :-
 2589   retract(C),
 2590   fail.          
 2591              
 2592
 2593/* \end{verbatim}
 2594\subsection{Saving Theorist}
 2595The command ``save'' automagically saves the state of the Theorist code
 2596as the command `theorist`. This is normally done straight after compiling this
 2597file.
 2598\index{save}
 2599\begin{verbatim} */
 2600
 2601
 2602save :-
 2603   call(call,quintus:save_program(th,
 2604   format('~nWelcome to THEORIST 1.1.1  (4 December 89 version)
 2605For help type ``h.''.
 2606Any Problems see David Poole (poole@cs.ubc.ca)~n',
 2607  []))).
 2608
 2609
 2610/* \end{verbatim}
 2611\section{Utility Functions}
 2612\subsection{List Predicates}
 2613$append(X,Y,Z)$ is the normal append function
 2614\index{append}
 2615\begin{verbatim} 
 2616append([],L,L).
 2617
 2618append([H|X],Y,[H|Z]) :-
 2619   append(X,Y,Z).
 2620\end{verbatim}
 2621
 2622\index{member}
 2623\begin{verbatim} */
 2624
 2625/*
 2626member(A,[A|_]).
 2627member(A,[_|R]) :-
 2628   member(A,R).
 2629*/
 2630
 2631/* \end{verbatim}
 2632
 2633$id\_member(X,L)$ is true if $X$ is identical to some member of list $L$.
 2634\index{id\_member}
 2635\begin{verbatim} */
 2636
 2637
 2638id_member(A,[B|_]) :-
 2639   A==B.
 2640id_member(A,[_|R]) :-
 2641   id_member(A,R).
 2642
 2643
 2644/* \end{verbatim}
 2645
 2646\index{same\_length}
 2647\begin{verbatim} */
 2648
 2649
 2650same_length_nnf([],[]).
 2651same_length_nnf([_|L1],[_|L2]) :-
 2652   same_length_nnf(L1,L2).
 2653
 2654
 2655/* \end{verbatim}
 2656
 2657\index{remove_nnf}
 2658\begin{verbatim} */
 2659
 2660
 2661remove_nnf(A,[A|B],B).
 2662remove_nnf(A,[H|T],[H|R]) :-
 2663   remove_nnf(A,T,R).
 2664
 2665
 2666/* \end{verbatim}
 2667
 2668\index{remove_nnf\_all}
 2669\begin{verbatim} */
 2670
 2671
 2672remove_all_nnf([],L,L).
 2673remove_all_nnf([H|T],L,L2) :-
 2674   remove_nnf(H,L,L1),
 2675   remove_all_nnf(T,L1,L2).
 2676
 2677
 2678/* \end{verbatim}
 2679
 2680\subsection{Looking at Terms}
 2681\index{variable\_free}
 2682\begin{verbatim} */
 2683
 2684variable_free(X) :- !, \+ ground(X).
 2685
 2686variable_free(X) :-
 2687   atomic(X),
 2688   !.
 2689variable_free(X) :-
 2690   var(X),
 2691   !,
 2692   fail.
 2693variable_free([H|T]) :-
 2694   !,
 2695   variable_free(H),
 2696   variable_free(T).
 2697variable_free(X) :-
 2698   X =.. Y,
 2699   variable_free(Y).
 2700
 2701
 2702/* \end{verbatim}
 2703
 2704\index{make\_ground}
 2705\begin{verbatim} */
 2706
 2707
 2708make_ground(X) :-
 2709   retract(groundseed(N)),
 2710   tnumbervars(X,N,NN),
 2711   asserta(groundseed(NN)).
 2712
 2713:- dynamic groundseed/1. 2714groundseed(26).
 2715
 2716
 2717
 2718/* \end{verbatim}
 2719
 2720\index{reverse}
 2721\begin{verbatim} */
 2722
 2723
 2724reverse([],T,T).
 2725reverse([H|T],A,B) :-
 2726   reverse(T,A,[H|B]).
 2727
 2728
 2729/* \end{verbatim}
 2730                                                     
 2731\subsection{Help Commands}
 2732\index{h}
 2733\begin{verbatim} */
 2734
 2735
 2736(h) :- format('This is Theorist 1.1 (all complaints to David Poole)
 2737For more details issue the command:
 2738   h H.
 2739where H is one of:~n',
 2740[]),
 2741   unix(system('ls /faculty/poole/theorist/help')).
 2742
 2743(h(( H))) :- !,
 2744   add_prefix(`more /faculty/poole/theorist/help/`,H,Cmd),
 2745   unix(system(Cmd)).
 2746                              
 2747
 2748
 2749/* \end{verbatim}
 2750
 2751\subsection{Runtime Considerations}
 2752What is given here is the core part of our current implementation of
 2753Theorist.
 2754This code has been used with Waterloo Unix Prolog, Quintus Prolog,
 2755C-prolog ',' Mac-Prolog.
 2756For those Prologs with compilers we can actually compile the resulting
 2757code from this translater as we could any other Prolog code;
 2758this make it very fast indeed.
 2759
 2760The resulting code when the Theorist code is of the form of definite clauses 
 2761(the only case where a comparison makes sense,
 2762as it is what the two systems have in common), runs at about a quarter
 2763the speed
 2764of the corresponding interpreted ';' compiled code of the underlying
 2765Prolog system. About half of this extra cost is
 2766for the extra arguments to unify,
 2767',' the other factor is for one membership
 2768of an empty list for each procedure call.
 2769For each procedure call we do one extra Prolog call which immediately fails.
 2770For the definite clause case, the contrapositive of the clauses are never used.
 2771\section{Conclusion}
 2772This paper has described in detail how we can translate Theorist code into
 2773prolog so that we can use the advances in Prolog implementation Technology.
 2774
 2775As far as this compiler is concerned there are a few issues which
 2776arise:
 2777\begin{itemize}                      
 2778\item Is there a more efficient way to determine that a goal can succeed because
 2779it unifies with an ancestor \cite{poole:grace,loveland87}?
 2780\item Can we incorporate a cycle check that has a low overhead?
 2781A simple, but expensive, version is implemented in some versions of
 2782our compiler which checks for identical ancestors.
 2783\item Are there optimal ordering which we can put the compiled
 2784clauses in so that we get answer most quickly \cite{smith86}?
 2785At the moment the compiler just puts the elements of the bodies
 2786in an arbitrary ordering. The optimal ordering depends, of course,
 2787on the underlying control structure.
 2788\item Are there better ways to do the consistency checking when there are
 2789variables in the hypotheses?
 2790\end{itemize}
 2791
 2792
 2793We are currently working on many applications of default ',' abductive
 2794reasoning.
 2795Hopefully with compilers based on the ideas presented in this paper
 2796we will be able to take full advantage of
 2797advances in Prolog implementation technology while still allowing
 2798flexibility in specification of the problems to be solved.
 2799\section*{Acknowledgements}
 2800This work could not have been done without the ideas,
 2801criticism ',' feedback from Randy Goebel, Eric Neufeld,
 2802Paul Van Arragon, Scott Goodwin ',' Denis Gagn\'e.
 2803Thanks to Brenda Parsons ',' Amar Shan for valuable comments on
 2804a previous version of this paper.
 2805This research was supported under NSERC grant A6260.
 2806\begin{thebibliography}{McDer80}
 2807\bibitem[Brewka86]{brewka86}
 2808G.\ Brewka,
 2809``Tweety -- Still Flying: Some Remarks on Abnormal Birds, Applicable Rules
 2810',' a Default Prover'',
 2811{\em Proc.\ AAAI-86}, pp.\ 8-12.
 2812
 2813\bibitem[Chang73]{chang}
 2814C-L.\ Chang ',' R.\ C-T.\ Lee,
 2815{\em Symbolic Logic ',' Mechanical Theorem Proving},
 2816Academic Press, 1973.
 2817
 2818\bibitem[Cox82]{cox82}
 2819P.\ T.\ Cox, {\em Dependency-directed backtracking for Prolog Programs}.
 2820
 2821\bibitem[Cox87]{cox87}
 2822P.\ T.\ Cox ',' T.\ Pietrzykowski, {\em General Diagnosis by Abductive
 2823Inference}, Technical report CS8701, School of Computer Science,
 2824Technical University of Nova Scotia, April 1987.
 2825
 2826\bibitem[Dincbas87]{dincbas}
 2827M.~Dincbas, H.~Simonis ',' P.~Van Hentenryck,
 2828{\em Solving Large Combinatorial Problems in Logic Programming\/},
 2829ECRC Technical Report, TR-LP-21, June 1987.
 2830
 2831\bibitem[Doyle79]{doyle79}
 2832J.\ Doyle,
 2833``A Truth Maintenance System'',
 2834{\em Artificial Intelligence},
 2835Vol.\ 12, pp 231-273.
 2836
 2837\bibitem[de Kleer86]{dekleer86}
 2838J.\ de Kleer,
 2839``An Assumption-based TMS'',
 2840{\em Artificial Intelligence, Vol.\ 28, No.\ 2}, pp.\ 127-162.
 2841
 2842\bibitem[Edmonson87]{edmonson}
 2843R.~Edmonson, ????
 2844
 2845\bibitem[Enderton72]{enderton}
 2846H.\ B.\ Enderton, {\em A Mathematical Introduction to Logic},
 2847Academic Press, Orlando.
 2848
 2849\bibitem[Genesereth87]{genesereth87}
 2850M.\ Genesereth ',' N.\ Nilsson,
 2851{\em Logical Foundations of Artificial Intelligence},
 2852Morgan-Kaufmann, Los Altos, California.
 2853
 2854\bibitem[Ginsberg87]{ginsberg87}
 2855M.~L.~Ginsberg, {\em Computing Circumscription\/},
 2856Stanford Logic Group Report Logic-87-8, June 1987.
 2857
 2858\bibitem[Goebel87]{goebel87}
 2859R.\ G.\ Goebel ',' S.\ D.\ Goodwin,
 2860``Applying theory formation to the planning problem''
 2861in F.\ M.\ Brown (Ed.),
 2862{\em Proceedings of the 1987 Workshop on The Frame Problem in Artificial
 2863Intelligence}, Morgan Kaufmann, pp.\ 207-232.
 2864
 2865\bibitem[Kowalski79]{kowalski}
 2866R.~Kowalski, ``Algorithm = Logic + Control'',
 2867{\em Comm.~A.C.M.} Vol 22, No 7, pp.~424-436.
 2868
 2869\bibitem[Lifschitz85]{lifschitz85}
 2870V.~Lifschitz, ``Computing Circumscription'',
 2871{\em Proc.~IJCAI85}, pp.~121-127.
 2872
 2873\bibitem[Lloyd87]{lloyd}
 2874J.~Lloyd, {\em Foundations of Logic Programming},
 2875Springer-Verlag, 2nd Edition.
 2876
 2877\bibitem[Loveland78]{loveland78}
 2878D.~W.~Loveland, {\em Automated Theorem Proving: a logical basis},
 2879North-Holland, Amsterdam.
 2880
 2881\bibitem[Loveland87]{loveland87}
 2882D.~W.~Loveland, ``Near-Horn Logic Programming'',
 2883{\em Proc. 6th International Logic Programming Conference}.
 2884
 2885\bibitem[McCarthy86]{mccarthy86}
 2886J.\ McCarthy, ``Applications of Circumscription to Formalising
 2887Common Sense Knowledge'', {\em Artificial Intelligence}, Vol.\ 28, No.\ 1,
 2888pp.\ 89-116.
 2889
 2890\bibitem[Moto-Oka84]{pie}
 2891T.~Moto-Oka, H.~Tanaka, H.~Aida, k.~Hirata ',' T.~Maruyama,
 2892``The Architecture of a Parallel Inference Engine --- PIE'',
 2893{\em Proc.\ Int.\ Conf.\ on Fifth Generation Computing Systems},
 2894pp.~479-488.
 2895
 2896\bibitem[Naish86]{naish86}
 2897L.~Naish, ``Negation ',' Quantifiers in NU-PROLOG'',
 2898{\em Proc.~3rd Int.\ Conf.\ on Logic Programming},
 2899Springer-Verlag, pp.~624-634.
 2900
 2901\bibitem[Neufeld87]{neufeld87}
 2902E.\ M.\ Neufeld ',' D.\ Poole,
 2903``Towards solving the multiple extension problem:
 2904combining defaults ',' probabilities'',
 2905{\em Proc.\ Third AAAI Workshop on Reasoning with Uncertainty},
 2906Seattle, pp.\ 305-312.
 2907
 2908\bibitem[Poole84]{poole:clausal}
 2909D.\ L.\ Poole,
 2910``Making Clausal theorem provers Non-clausal'',
 2911{\em Proc.\ CSCSI-84}. pp.~124-125.
 2912
 2913\bibitem[Poole86]{poole:grace}
 2914D.\ L.\ Poole,
 2915``Gracefully adding Negation to Prolog'',
 2916{\em Proc.~Fifth International Logic Programming Conference},
 2917London, pp.~635-641.
 2918
 2919\bibitem[Poole86]{poole:dd}
 2920D.\ L.\ Poole,
 2921``Default Reasoning ',' Diagnosis as Theory Formation'',
 2922Technical Report, CS-86-08, Department of Computer Science,
 2923University of Waterloo, March 1986.
 2924
 2925\bibitem[Poole87a]{poole:vars}
 2926D.\ L.\ Poole,
 2927``Variables in Hypotheses'', 
 2928{\em Proc.~IJCAI-87}, pp.\ 905-908.
 2929
 2930\bibitem[Poole87b]{poole:dc}
 2931D.\ L.\ Poole,
 2932{\em Defaults ',' Conjectures: Hypothetical Reasoning for Explanation ','
 2933Prediction}, Research Report CS-87-54, Department of
 2934Computer Science, University of Waterloo, October 1987, 49 pages.
 2935
 2936\bibitem[Poole88]{poole:lf}
 2937D.\ L.\ Poole,
 2938{\it A Logical Framework for Default Reasoning},
 2939to appear {\em Artificial Intelligence}, Spring 1987.
 2940
 2941\bibitem[PGA87]{pga}
 2942D.\ L.\ Poole, R.\ G.\ Goebel ',' R.\ Aleliunas,
 2943``Theorist: A Logical Reasoning System for Defaults ',' Diagnosis'',
 2944in N. Cercone ',' G. McCalla (Eds.)
 2945{\it The Knowledge Frontier: Essays in the Representation of
 2946Knowledge},
 2947Springer Varlag, New York, 1987, pp.\ 331-352.
 2948
 2949\bibitem[Reiter80]{reiter80}
 2950R.\ Reiter,
 2951``A Logic for Default Reasoning'',
 2952{\em Artificial Intelligence},
 2953Vol.\ 13, pp 81-132.
 2954                      
 2955\bibitem[Smith86]{smith86}
 2956D.~Smith ',' M.~Genesereth,
 2957``Ordering Conjunctive Queries'',
 2958{\em Artificial Intelligence}.
 2959
 2960\bibitem[Van Hentenryck87]{vanh}
 2961P.\ Van Hentenryck,
 2962``A Framework for consistency techniques in Logic Programming''
 2963IJCAI-87, Milan, Italy.
 2964\end{thebibliography}
 2965\printindex
 2966\end{document}
 2967*/
 2968
 2969tnumbervars(Term, N, M):- numbervars(Term, N, M).
 2970/*
 2971tnumbervars(Term, N, Nplus1) :-
 2972  var(Term), !,
 2973  Term = var/N,
 2974  Nplus1 is N + 1.
 2975tnumbervars(Term, N, M) :-
 2976  Term =.. [_|Args],
 2977  numberargs(Args,N,M).
 2978
 2979numberargs([],N,N) :- !.
 2980numberargs([X|L], N, M) :-
 2981  numberargs(X, N, N1),
 2982  numberargs(L, N1, M).      
 2983*/
 2984
 2985
 2986%:- include(snark_klsnl).
 2987
 2988%:- thconsult(all_ex).
 2989
 2990:- fixup_exports.