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