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