1/* 2 3 ABDUCTIVE EVENT CALCULUS 4 5 MURRAY SHANAHAN 6 7 Version 1.9a 8 9 September 1997 10 11 Written for LPA MacProlog 32 12 13*/ 14 15%:- include(ec_common). 16 17/* 18 19 This is an abductive meta-interpreter for abduction with negation-as- 20 failure, with built-in features for handling event calculus queries. 21 In effect this implements a partial-order planner. not(clipped) facts 22 correspond to protected links. The planner will also perform 23 hierarchical decomposition, given definitions of compound events 24 (happens if happens clauses). 25 26 The form of queries is as follows. 27 28 abdemo(Goals,Residue) 29 30 Goals is a list of atoms (goals). Residue is a pair of lists of atoms 31 [RH,RB], where RH contains happens facts and RB contains temporal 32 ordering facts. Negations is a list of lists of atoms. 33 34 Roughly speaking, the above formulae should hold if, 35 36 EC and CIRC[Domain] and CIRC[ResidueOut] |= Goals 37 38 where EC is the event calculus axioms, CIRC[Domain] is the completion 39 of initiates, terminates and releases, and CIRC[ResidueOut] is the 40 completion of happens. (Note that completion isn't applied to temporal 41 ordering facts.) 42 43 F is expected to be fully bound when we call abdemo(holds_at(F,T)). 44 It's assumed that all primitive actions (two argument happens) are 45 in the residue. 46 47 Although the interpreter will work with any logic program, the axioms of 48 the event calculus are compiled in to the meta-level. 49 50 The function symbol "neg" is introduced to represent classically 51 negated fluents. holds_at(neg(F)) corresponds to not holds_at(F) 52 (with classical "not"). terminates formulae play a role in clipping 53 positive fluents and initiating negative fluents. Conversely, 54 initiates formulae play a role in clipping negative fluents and 55 initiating positive ones. 56 57*/ 58 59 60 61 62/* 63 Top level calls to abdemo have to be transformed to the following form. 64 65 abdemo(Goals,ResidueIn,ResidueOut,NegationsIn,NegationsOut) 66*/ 67 68 69 70abdemo(Gs,R) :- abdemo(Gs,[[],[]],R,[],N). 71 72abdemo_timed(Gs,R) :- 73 ticks(Z1), abdemo(Gs,[[],[]],R,[],N), ticks(Z2), 74 Z is (Z2-Z1)/60, write('Total time taken '), writenl(Z), nl. 75 76abdemo([],R,R,N,N). 77 78 79/* 80 The next few clauses are the result of compiling the axioms of 81 the event calculus into the meta-level. The first of these clauses 82 checks to see whether a holds_at goal is already provable from the 83 residue. (Note that, in such cases, we still need to record and 84 preserve the not(clipped) facts the goal depends on.) 85 DANGER: The cut in the following clause is a source of incompleteness, 86 but without it we get duplicate solutions. 87*/ 88 89abdemo([holds_at(F,T)|Gs],R1,R2,N1,N3) :- 90 demo([holds_at(F,T)],R1,N1,N2), !, abdemo(Gs,R1,R2,N2,N3). 91 92/* 93 Now we have two clauses which are meta-level representation of the two 94 event calculus axioms for holds_at. 95 96 holds_at(F,T) <- initiallyp(F) and not clipped(0,F,T) 97 98 holds_at(F,T3) <- 99 happens(A,T1,T2) and T2 < T3 and 100 initiates(A,F,T1) and not clipped(T1,F,T2) 101*/ 102 103abdemo([holds_at(F1,T)|Gs1],R1,R3,N1,N4) :- 104 F1 \= neg(F2), abresolve(initially(F1),R1,Gs2,R1,B), 105 append(Gs2,Gs1,Gs3), add_neg([clipped(0,F1,T)],N1,N2), 106 abdemo_naf([clipped(0,F1,T)],R1,R2,N2,N3), 107 abdemo(Gs3,R2,R3,N3,N4). 108 109/* 110 The order in which resolution steps are carried out in the next 111 clause is crucial. We resolve initiates first in order to instantiate 112 A, but we don't want to proceed with sub-goals of initiates until 113 we've added the corresponding happens and b facts to the residue. 114*/ 115 116abdemo([holds_at(F1,T3)|Gs1],R1,R7,N1,N6) :- 117 F1 \= neg(F2), abresolve(initiates(A,F1,T1),R1,Gs2,R1,B1), 118 abresolve(happens(A,T1,T2),R1,Gs3,R2,B2), 119 abdemo(Gs3,R2,R3,N1,N2), 120 abresolve(b(T2,T3),R3,[],R4,B3), 121 append(Gs2,Gs1,Gs4), check_nafs(B2,N2,R4,R5,N2,N3), 122 add_neg([clipped(T1,F1,T3)],N3,N4), 123 abdemo_naf([clipped(T1,F1,T3)],R5,R6,N4,N5), 124 abdemo(Gs4,R6,R7,N5,N6). 125 126/* 127 The next two clauses are a meta-level representation of the two 128 event calculus axioms for not holds_at. 129 130 not holds_at(F,T) <- initiallyn(F) and not declipped(0,F,T) 131 132 not holds_at(F,T3) <- 133 happens(A,T1,T2) and T2 < T3 and 134 terminates(A,F,T1) and not declipped(T1,F,T2) 135*/ 136 137abdemo([holds_at(neg(F),T)|Gs1],R1,R3,N1,N4) :- 138 abresolve(initially(neg(F)),R1,Gs2,R1,B), 139 append(Gs2,Gs1,Gs3), add_neg([declipped(0,F,T)],N1,N2), 140 abdemo_naf([declipped(0,F,T)],R1,R2,N2,N3), 141 abdemo(Gs3,R2,R3,N3,N4). 142 143abdemo([holds_at(neg(F),T3)|Gs1],R1,R7,N1,N6) :- 144 abresolve(terminates(A,F,T1),R1,Gs2,R1,B1), 145 abresolve(happens(A,T1,T2),R1,Gs3,R2,B2), 146 abdemo(Gs3,R2,R3,N1,N2), 147 abresolve(b(T2,T3),R3,[],R4,B3), 148 append(Gs2,Gs1,Gs4), check_nafs(B2,N2,R4,R5,N2,N3), 149 add_neg([declipped(T1,F,T3)],N3,N4), 150 abdemo_naf([declipped(T1,F,T3)],R5,R6,N4,N5), 151 abdemo(Gs4,R6,R7,N5,N6). 152 153/* 154 The last two clauses cater for the general case (ie: goals other 155 than holds_at). 156*/ 157 158abdemo([not(G)|Gs],R1,R3,N1,N4) :- 159 !, abdemo_naf([G],R1,R2,N1,N2), add_neg([G],N2,N3), 160 abdemo(Gs,R2,R3,N3,N4). 161 162abdemo([G|Gs1],R1,R3,N1,N2) :- 163 abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3), 164 abdemo(Gs3,R2,R3,N1,N2). 165 166 167 168 169/* 170 The form of a call to abresolve is as follows. 171 172 abresolve(Goal,ResidueIn,Goals,ResidueOut,Flag) 173 174 where Goals is the body of clause resolved with, and Flag is set to true 175 if a happens fact has been added to the residue. 176*/ 177 178abresolve(happens(A,T,T),R1,Gs,R2,B) :- abresolve(happens(A,T),R1,Gs,R2,B). 179 180abresolve(happens(A,T1,T2),R,Gs,R,false) :- !, axiom(happens(A,T1,T2),Gs). 181 182/* 183 happens goals get checked to see if they are already in the residue. 184 This permits the re-use of actions already in the residue. However, 185 this decision may lead to later failure, in which case we try adding 186 a new action to the residue. 187*/ 188 189abresolve(happens(A,T),[RH,RB],[],[RH,RB],false) :- member(happens(A,T),RH). 190 191/* 192 Time variables get skolemised, but not action variables because 193 they end up getting instantiated anyway. 194*/ 195 196abresolve(happens(A,T),[RH,RB],[],[[happens(A,T)|RH],RB],true) :- 197 !, skolemise(T), executable(A). 198 199/* 200 It's assumed that X and Y are bound when we call abresolve(b(X,Y)). 201 If either X or Y is not bound, we may miss solutions due to the cut in 202 the following clause. 203*/ 204 205abresolve(b(X,Y),[RH,RB],[],[RH,RB],false) :- demo_before(X,Y,RB), !. 206 207abresolve(b(X,Y),[RH,RB1],[],[RH,RB2],false) :- 208 !, skolemise(X), skolemise(Y), \+ demo_beq(Y,X,RB1), 209 add_before(X,Y,RB1,RB2). 210 211/* 212 The predicates "diff" (meaning not equal) and "is" (for evaluating 213 arithmetic expressions) are built in. 214*/ 215 216abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y. 217 218abresolve(is(X,Y),R,[],R,false) :- !, X is Y. 219 220abresolve(G,R,[],[G|R],false) :- abducible(G). 221 222abresolve(G,R,Gs,R,false) :- axiom(G,Gs). 223 224 225 226 227/* 228 add_neg(N,Ns1,Ns2) adds goal N to the list of (lists of) negations Ns1, 229 giving Ns2. Duplicates are ignored, but N must be fully bound. 230*/ 231 232add_neg(N,Ns,Ns) :- member(N,Ns), !. 233 234add_neg(N,Ns,[N|Ns]). 235 236 237/* append_negs is just append, but ignoring duplicates. */ 238 239append_negs([],[],[]). 240 241append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4). 242 243 244 245 246/* 247 abdemo_nafs([G1...Gn],R1,R2) demos not(G1) and ... and not(Gn). 248 249 Calls to abdemo_naf have the following form. 250 251 abdemo_nafs(Negations,ResidueIn,ResidueOut, 252 NegationsIn,NegationsOut) 253 254 where Negations is the list of negations to be established, ResidueIn 255 is the old residue, ResidueOut is the new residue (abdemo_nafs can add 256 both b and happens facts, as well as other abducibles, to the 257 residue), NegationsIn is the old list of negations (same as Negations 258 for top-level call), and NegationsOut is the new list of negations 259 (abdemo_nafs can add new clipped goals to NegationsIn). 260*/ 261 262 263abdemo_nafs([],R,R,N,N). 264 265abdemo_nafs([N|Ns],R1,R3,N1,N3) :- 266 abdemo_naf(N,R1,R2,N1,N2), abdemo_nafs(Ns,R2,R3,N2,N3). 267 268 269 270 271/* 272 abdemo_naf([G1...Gn],R1,R2) demos not((G1) and ... and (Gn)). 273 274 As for abdemo, the main event calculus axioms are compiled into the 275 meta-level in abdemo_naf. In addition to the two holds_at axioms, we 276 have, 277 278 clipped(T1,F,T3) <- 279 happens(A,T2) and T1 < T2 < T3 and 280 [terminates(A,F,T2) or releases(A,F,T2)] 281 282 declipped(T1,F,T3) <- 283 happens(A,T2) and T1 < T2 < T3 and 284 [initiates(A,F,T2) or releases(A,F,T2)] 285 286 We have to use findall here, because all ways of achieving a goal 287 have to fail for the goal itself to fail. 288*/ 289 290abdemo_naf([clipped(T1,F,T3)|Gs1],R1,R2,N1,N2) :- 291 !, findall(Gs3, 292 (resolve(terms_or_rels(A,F,T2),R1,Gs2), 293 resolve(happens(A,T2),R1,[]), 294 append([b(T1,T2),b(T2,T3)|Gs2],Gs1,Gs3)),Gss), 295 abdemo_nafs(Gss,R1,R2,N1,N2). 296 297abdemo_naf([declipped(T1,F,T3)|Gs1],R1,R2,N1,N2) :- 298 !, findall(Gs3, 299 (resolve(inits_or_rels(A,F,T2),R1,Gs2), 300 resolve(happens(A,T2),R1,[]), 301 append([b(T1,T2),b(T2,T3)|Gs2],Gs1,Gs3)),Gss), 302 abdemo_nafs(Gss,R1,R2,N1,N2). 303 304/* 305 To show the classical negation of holds_at(F) (which is what we want), we 306 have to show that holds_at(neg(F)). Conversely, to show the classical 307 negation of holds_at(neg(F)) we have to show holds_at(F). Within a call 308 to abdemo_naf, we can add both happens and b (and other abducibles) 309 to the residue. This removes a potential source of incompleteness. 310 However, we only want to add to the residue as a last resort. Accordingly, 311 holds_at goals are postponed if they can't be proved without adding to 312 the residue. A postponed holds_at goal appears in the goal list as 313 postponed(holds_at(F,T)). 314*/ 315 316abdemo_naf([holds_at(F1,T)|Gs],R,R,N1,N2) :- 317 opposite(F1,F2), demo([holds_at(F2,T)],R,N1,N2), !. 318 319abdemo_naf([holds_at(F,T)|Gs1],R1,R2,N1,N2) :- 320 !, append(Gs1,[postponed(holds_at(F,T))],Gs2), 321 abdemo_naf(Gs2,R1,R2,N1,N2). 322 323abdemo_naf([postponed(holds_at(F1,T))|Gs],R1,R3,N1,N3) :- 324 opposite(F1,F2), abdemo([holds_at(F2,T)],R1,R2,N1,N2), !, 325 abdemo_naf_cont(R1,Gs,R2,R3,N2,N3). 326 327abdemo_naf([postponed(holds_at(F,T))|Gs],R1,R2,N1,N2) :- 328 !, abdemo_naf(Gs,R1,R2,N1,N2). 329 330/* 331 Special facilities for handling temporal ordering facts are built in. 332 We can add a b fact to the residue to preserve the failure of 333 a clipped goal. The failure of a b goal does NOT mean that the 334 negation of that goal is assumed to be true. (The Clark completion is 335 not applicable to temporal ordering facts.) Rather, to make b(X,Y) 336 fail, b(Y,X) has to follow. One way to achieve this is to add 337 b(Y,X) to the residue. 338*/ 339 340abdemo_naf([b(X,Y)|Gs],R,R,N,N) :- X == Y, !. 341 342abdemo_naf([b(X,Y)|Gs],[RH,RB],[RH,RB],N,N) :- demo_before(Y,X,RB), !. 343 344abdemo_naf([b(X,Y)|Gs1],R1,R2,N1,N2) :- 345 !, append(Gs1,[postponed(b(X,Y))],Gs2), 346 abdemo_naf(Gs2,R1,R2,N1,N2). 347 348/* 349 A b fact is only added to the residue as a last resort. Accordingly, 350 if we encounter a b(X,Y) goal and cannot show b(Y,X), we 351 postpone that goal until we've tried other possibilities. A postponed 352 b goal appears in the goal list as postponed(b(X,Y)). 353*/ 354 355abdemo_naf([postponed(b(X,Y))|Gs],[RH,RB1],[RH,RB2],N,N) :- 356 \+ demo_beq(X,Y,RB1), add_before(Y,X,RB1,RB2). 357 358abdemo_naf([postponed(b(X,Y))|Gs],R1,R2,N1,N2) :- 359 !, abdemo_naf(Gs,R1,R2,N1,N2). 360 361/* 362 We drop through to the general case for goals other than special event 363 calculus goals. 364*/ 365 366abdemo_naf([not(G)|Gs],R1,R3,N1,N3) :- 367 abdemo([G],R1,R2,N1,N2), !, abdemo_naf_cont(R1,Gs,R2,R3,N2,N3). 368 369abdemo_naf([not(G)|Gs],R1,R2,N1,N2) :- !, abdemo_naf(Gs,R1,R2,N1,N2). 370 371abdemo_naf([G|Gs1],R,R,N,N) :- \+ resolve(G,R,Gs2), !. 372 373abdemo_naf([G1|Gs1],R1,R2,N1,N2) :- 374 findall(Gs2,(resolve(G1,R1,Gs3),append(Gs3,Gs1,Gs2)),Gss), 375 abdemo_nafs(Gss,R1,R2,N1,N2). 376 377 378/* 379 abdemo_naf_cont gets an extra opportunity to succeed if the residue 380 has been altered. This is determined by comparing R1 with R2. If 381 a sub-goal has failed and the residue hasn't been altered, there's 382 no need to look for other ways to prove the negation of the overall goal. 383*/ 384 385abdemo_naf_cont(R1,Gs,R2,R2,N,N). 386 387abdemo_naf_cont(R1,Gs,R2,R3,N1,N2) :- R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2). 388 389 390 391 392/* 393 check_nafs is just like abdemo_nafs, except that it only checks 394 negated clipped and declipped facts against the most recent event 395 added to the residue. To check one of these negations, not only can 396 we confine our attention to the most recent event, but we can ignore 397 that event if it doesn't fall inside the interval covered by the 398 clipped/declipped in question. Of course, the negated clipped/declipped 399 fact might depend on other holds_at facts. But their preservation is 400 ensured because the clipped/declipped negation they themselves depend 401 on will also be checked. 402*/ 403 404 405check_nafs(false,N1,R,R,N2,N2) :- !. 406 407check_nafs(true,N,[[happens(A,T)|RH],RB],R,N1,N2) :- 408 check_nafs(A,T,N,[[happens(A,T)|RH],RB],R,N1,N2). 409 410check_nafs(A,T,[],R,R,N,N). 411 412check_nafs(A,T,[N|Ns],R1,R3,N1,N3) :- 413 check_naf(A,T,N,R1,R2,N1,N2), check_nafs(A,T,Ns,R2,R3,N2,N3). 414 415 416check_naf(A,T2,[clipped(T1,F,T3)],R1,R2,N1,N2) :- 417 !, findall([b(T1,T2),b(T2,T3)|Gs], 418 (resolve(terms_or_rels(A,F,T2),R1,Gs)),Gss), 419 abdemo_nafs(Gss,R1,R2,N1,N2). 420 421check_naf(A,T2,[declipped(T1,F,T3)],R1,R2,N1,N2) :- 422 !, findall([b(T1,T2),b(T2,T3)|Gs], 423 (resolve(inits_or_rels(A,F,T2),R1,Gs)),Gss), 424 abdemo_nafs(Gss,R1,R2,N1,N2). 425 426check_naf(A,T2,N,R1,R2,N1,N2) :- abdemo_naf(N,R1,R2,N1,N2). 427 428 429 430 431/* 432 demo is just like abdemo, except that it doesn't add to the residue. 433 It does, however add to the list of negations. 434*/ 435 436demo([],R,N,N). 437 438demo([holds_at(F1,T)|Gs1],R,N1,N3) :- 439 F1 \= neg(F2), resolve(initially(F1),R,Gs2), 440 demo_naf([clipped(0,F1,T)],R), 441 append(Gs2,Gs1,Gs3), add_neg([clipped(0,F1,T)],N1,N2), 442 demo(Gs3,R,N2,N3). 443 444demo([holds_at(F1,T2)|Gs1],R,N1,N4) :- 445 F1 \= neg(F2), resolve(initiates(A,F1,T1),R,Gs2), 446 resolve(happens(A,T1),R,Gs3), 447 resolve(b(T1,T2),R,[]), 448 demo(Gs2,R,N1,N2), demo_naf([clipped(T1,F1,T2)],R), 449 append(Gs3,Gs1,Gs4), add_neg([clipped(T1,F1,T2)],N2,N3), 450 demo(Gs4,R,N3,N4). 451 452demo([holds_at(neg(F),T)|Gs1],R,N1,N3) :- 453 resolve(initially(neg(F)),R,Gs2), 454 demo_naf([declipped(0,F,T)],R), 455 append(Gs2,Gs1,Gs3), add_neg([declipped(0,F,T)],N1,N2), 456 demo(Gs3,R,N2,N3). 457 458demo([holds_at(neg(F),T2)|Gs1],R,N1,N4) :- 459 resolve(terminates(A,F,T1),R,Gs2), 460 resolve(happens(A,T1),R,Gs3), 461 resolve(b(T1,T2),R,[]), 462 demo(Gs2,R,N1,N2), demo_naf([declipped(T1,F,T2)],R), 463 append(Gs3,Gs1,Gs4), add_neg([declipped(T1,F,T2)],N2,N3), 464 demo(Gs4,R,N3,N4). 465 466demo([b(X,Y)|Gs],R,N1,N2) :- !, demo_before(X,Y,R), demo(Gs,R,N1,N2). 467 468demo([not(G)|Gs],R,N1,N2) :- 469 !, demo_naf([G],R), add_neg([G],N1,N2), demo(Gs,R,N2,N3). 470 471demo([G|Gs1],R,N1,N3) :- 472 resolve(G,R,Gs2), demo(Gs2,R,N1,N2), demo(Gs1,R,N2,N3). 473 474 475 476 477/* 478 demo_before simply checks membership of the temporal ordering part 479 of the residue. 480*/ 481 482demo_before(0,Y,R) :- !. 483 484demo_before(X,Y,R) :- member(b(X,Y),R). 485 486/* demo_beq is demo b or equal. */ 487 488demo_beq(X,Y,R) :- X == Y, !. 489 490demo_beq(X,Y,R) :- demo_before(X,Y,R). 491 492 493/* 494 add_before(X,Y,R1,R2) adds b(X,Y) to the residue R1 giving R2. 495 It does this by maintaining the transitive closure of the b relation 496 in R2, and assumes that R1 is already transitively closed. 497 R1 and R2 are just the temporal ordering parts of the residue. 498*/ 499 500add_before(X,Y,R1,R2) :- 501 find_connections(X,Y,R1,C1,C2), 502 cross_prod(C1,C2,C3,R1), append(C3,R1,R2). 503 504/* 505 find_connections(X,Y,R,C1,C2) creates two lists, C1 and C2, 506 containing respectively all the time points b X and after 507 Y according to R, which is assumed to be transitively closed. 508*/ 509 510find_connections(X,Y,[],[X],[Y]). 511 512find_connections(X,Y,[b(Z,X)|R],[Z|C1],C2) :- 513 !, find_connections(X,Y,R,C1,C2). 514 515find_connections(X,Y,[b(Y,Z)|R],C1,[Z|C2]) :- 516 !, find_connections(X,Y,R,C1,C2). 517 518find_connections(X,Y,[b(Z1,Z2)|R],C1,C2) :- 519 find_connections(X,Y,R,C1,C2). 520 521cross_prod([],C,[],R). 522 523cross_prod([X|C1],C2,R3,R) :- 524 cross_one(X,C2,R1,R), cross_prod(C1,C2,R2,R), append(R1,R2,R3). 525 526cross_one(X,[],[],R). 527 528cross_one(X,[Y|C],[b(X,Y)|R1],R) :- 529 \+ member(b(X,Y),R), !, cross_one(X,C,R1,R). 530 531cross_one(X,[Y|C],R1,R) :- cross_one(X,C,R1,R). 532 533 534 535 536/* 537 Note that resolve doesn't check for happens axioms (defining 538 compound events). This would precipitate looping. This omission is 539 justified by the assumption that a compound event only occurs if its 540 sub-events occur, which in turn follows from the completion of 541 happens. 542 543 terms_or_rels means terminates or releases. Recall that terminates(F) 544 is really shorthand for initiates(neg(F)). 545*/ 546 547resolve(terms_or_rels(A,F,T),R,Gs) :- axiom(releases(A,F,T),Gs). 548 549resolve(terms_or_rels(A,F,T),R,Gs) :- !, axiom(terminates(A,F,T),Gs). 550 551resolve(inits_or_rels(A,F,T),R,Gs) :- axiom(releases(A,F,T),Gs). 552 553resolve(inits_or_rels(A,F,T),R,Gs) :- !, axiom(initiates(A,F,T),Gs). 554 555resolve(happens(A,T,T),R,Gs) :- resolve(happens(A,T),R,Gs). 556 557resolve(happens(A,T),[RH,RB],[]) :- !, member(happens(A,T),RH). 558 559resolve(b(X,Y),[RH,RB],[]) :- !, demo_before(X,Y,RB). 560 561resolve(diff(X,Y),R,[]) :- !, X \= Y. 562 563resolve(is(X,Y),R,[]) :- !, X is Y. 564 565resolve(G,R,Gs) :- axiom(G,Gs). 566 567 568 569 570/* 571 demo_nafs([G1...Gn],R) demos not(G1) and ... and not(Gn). 572 573 demo_nafs is just like abdemo_nafs, except that it doesn't add 574 to the residue. 575*/ 576 577demo_nafs([],R). 578 579demo_nafs([N|Ns],R) :- 580 demo_naf(N,R), demo_nafs(Ns,R). 581 582 583/* 584 demo_naf([G1...Gn],R1,R2) demos not((G1) and ... and (Gn)). 585 586 Note the use of \+ demo_beq(T2,T1) rather than \+ demo_before(T1,T2) 587 in demo_naf(clipped). This ensures that "not clipped" fails if there 588 exists a linearisation of the actions in the residue which would clip 589 the fluent in question. 590 591 In effect, demo_naf(clipped) proves the classical negation of clipped, 592 given the completions of clipped, initiates, terminates, releases and 593 happens. Likewise, demo_naf(holds_at) proves the classical negation 594 of holds_at. Assuming that F is a ground term, to show the classical 595 negation of holds_at(F), we simply have to show holds_at(neg(F)), and 596 to show the classical negation of holds_at(neg(F)), we show holds_at(F). 597 This is justified by the implicit adoption of the axiom, 598 599 not holds_at(F,T) <-> holds_at(neg(F),T) 600 601 where "not" is interpreted classically. 602 603 If F is not a ground term, we can still show demo_naf([holds_at(F)|Gs]) 604 by showing demo_naf(Gs) for all values of F for which demo(holds_at(F)) 605 succeeds. (We need to be able to do this to show not(clipped(F)) in the 606 presence of terminates clauses with holds_at conditions which supply 607 context rather than being preconditions. These will have unbound fluent 608 arguments when they are called.) However, this doesn't work in all cases 609 and is a potential source of incompleteness. 610*/ 611 612demo_naf([clipped(T1,F,T3)|Gs1],[RH,RB]) :- 613 !, findall(Gs3, 614 (resolve(terms_or_rels(A,F,T2),[RH,RB],Gs2), 615 resolve(happens(A,T2),[RH,RB],[]), 616 \+ demo_beq(T2,T1,RB), \+ demo_beq(T3,T2,RB), 617 append(Gs2,Gs1,Gs3)),Gss), 618 demo_nafs(Gss,[RH,RB]). 619 620demo_naf([declipped(T1,F,T3)|Gs1],[RH,RB]) :- 621 !, findall(Gs3, 622 (resolve(inits_or_rels(A,F,T2),[RH,RB],Gs2), 623 resolve(happens(A,T2),[RH,RB],[]), 624 \+ demo_beq(T2,T1,RB), \+ demo_beq(T3,T2,RB), 625 append(Gs2,Gs1,Gs3)),Gss), 626 demo_nafs(Gss,[RH,RB]). 627 628demo_naf([holds_at(F1,T)|Gs],R) :- 629 ground(F1), opposite(F1,F2), demo([holds_at(F2,T)],R,[],N), !. 630 631demo_naf([holds_at(F,T)|Gs],R) :- ground(F), !, demo_naf(Gs,R). 632 633demo_naf([holds_at(F,T)|Gs],R) :- 634 !, forall(demo([holds_at(F,T)],R,[],N),(ground(F),demo_naf(Gs,R))). 635 636demo_naf([b(X,Y)|Gs],R) :- X == Y, !. 637 638demo_naf([b(X,Y)|Gs],[RH,RB]) :- demo_before(Y,X,RB), !. 639 640demo_naf([b(X,Y)|Gs],R) :- !, demo_naf(Gs,R). 641 642demo_naf([not(G)|Gs],R) :- demo([G],R,[],N), !. 643 644demo_naf([not(G)|Gs],R) :- !, demo_naf(Gs,R). 645 646demo_naf([G|Gs1],R) :- \+ resolve(G,R,Gs2), !. 647 648demo_naf([G1|Gs1],R) :- 649 findall(Gs2,(resolve(G1,R1,Gs3),append(Gs3,Gs1,Gs2)),Gss), 650 demo_nafs(Gss,R). 651 652 653 654 655/* Skolemisation */ 656 657skolemise(T) :- var(T), gensym(t,T), !. 658 659skolemise(T). 660 661 662 663 664/* Odds and sods */ 665 666 667opposite(neg(F),F) :- !. 668 669opposite(F,neg(F)). 670 671 672or(true,B,true) :- !. 673 674or(false,false,false). 675 676or(false,true,true)