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

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