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