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