1%Ensure temporal points are generated correctly under PROLOG
    2:-ensure_loaded('genSymPatches.pl').    3
    4%Sort plans based on ordering
    5:-ensure_loaded('sortPlans.pl').    6
    7% Removing redundant temporal orderings
    8:-ensure_loaded('temporalOrderCleaner.pl').    9
   10% Map paritally ordering plans to totally ordered plans
   11:-ensure_loaded('mappingTotalOrderPlan.pl').   12
   13% 
   14:-ensure_loaded('loopReduction.pl').   15
   16
   17%HTML typing and parsing
   18:-ensure_loaded('../htmlTyping/typing.pl').   19
   20
   21:- include('../knowledgeBaseCGI.pl').   22
   23
   24:-prolog_flag(compiling,_,profiledcode).   25
   26%Ensures Prolog is not lazy and does return the entire result rather than predicate(...)
   27:- prolog_flag(toplevel_print_options,_,[quoted(true),numbervars(true),portrayed(true)]).                                                                   
   28 
   29%Ensure rules included are added rather than overwriting.
   30:- multifile valid_html_form/2.   31
   32
   33/*
   34   ABDUCTIVE EVENT CALCULUS
   35
   36   MURRAY SHANAHAN
   37   Version 1.15
   38   July 1998
   39   Written for LPA MacProlog 32
   40   
   41   Joseph Wilk
   42   Version 2
   43   2004
   44   
   45   Converted to SICStus Prolog.
   46   
   47   New Features
   48   
   49   1. Impossible predicate.
   50   2. More advanced debugging information
   51   3. Sort plan
   52   4. Loop reduction
   53   5. Mapping to total order plans
   54   6. Added high level plan generation
   55   
   56   
   57   In the future :
   58   
   59   1. Possiblity of using tail recurssion optimisation to improve performance.
   60   2. More efficent way of storing depth states of every branch,
   61   3. Ensuring impossible handled for happens precdicates in composite plans.
   62   4. Dealing with recursion generating invalid plans on investigating other potential plans.
   63
   64*/
   65
   66
   67/*
   68   This is an abductive meta-interpreter for abduction with negation-as-
   69   failure, with built-in features for handling event calculus queries.
   70   In effect this implements a partial-order planner. not(clipped) facts
   71   correspond to protected links. The planner will also perform
   72   hierarchical decomposition, given definitions of compound events
   73   (happens if happens clauses).
   74
   75   The form of queries is as follows.
   76
   77        abdemo(Goals,Residue)
   78
   79   Goals is a list of atoms. Residue is a pair of [RH,RB], where RH is a
   80   list of happens facts and RB is a list of temporal ordering facts.
   81   Negations is a list of lists of atoms.
   82
   83   Roughly speaking, the above formulae should hold if,
   84
   85        EC and CIRC[Domain] and CIRC[Residue] |= Goals
   86
   87   where EC is the event calculus axioms, CIRC[Domain] is the completion
   88   of initiates, terminates and  releases, and CIRC[Residue] is the
   89   completion of happens. (Note that completion isn't applied to temporal
   90   ordering facts.)
   91
   92   F is expected to be fully bound when we call abdemo(holds_at(F,T)).
   93   It's assumed that all primitive actions (two argument happens) are
   94   in the residue (ie: none are in the program).
   95
   96   Although the interpreter will work with any logic program, the axioms of
   97   the event calculus are compiled in to the meta-level.
   98
   99   The function symbol "neg" is introduced to represent classically
  100   negated fluents. holds_at(neg(F)) corresponds to not holds_at(F)
  101   (with classical "not"). terminates formulae play a role in clipping
  102   positive fluents and initiating negative fluents. Conversely,
  103   initiates formulae play a role in clipping negative fluents and
  104   initiating positive ones.
  105
  106   Computation interleaves search (abdemo) and refinement phases. After each
  107   step of the computation, where a step is an iteration of abdemo or a
  108   refinement, the residue so far plus the remaining goal list entail the goal
  109   state. In other words, these computational steps are also proof steps.
  110
  111   An iterative deepening search strategy is employed, where depth
  112   corresponds to length of plan.
  113*/
  114
  115
  116
  117
  118/* TOP LEVEL */
  119
  120
  121/*
  122
  123Modified Joseph Wilk 21/01/04
  124
  125   Top level calls to abdemo have to be transformed to the following form.
  126
  127        abdemo_top(Goals,ResidueIn,ResidueOut,NegationsIn,NegationsOut,DepthBound, MaxDepth, HighLevel)
  128
  129   The residue has the form [[HA,HC],[BA,BC]], where HA is a list of happens
  130   atoms, HC is the transistive closure of the before-or-equal relation on times
  131   that follows from HA, BA is a list of before atoms, and BC is the transitive
  132   closure of BA.
  133   
  134   MaxDepth indicates the limit which failure is assumed for the iterative deepening
  135   
  136*/
  137
  138
  139
  140% 4/2/04 Joseph Wilk - Sorts Plans / currently only totally ordered plans!
  141
  142plan(Gs,[SortedPlan, FinalOrderings], MaxDepth, HighLevel) :-
  143	
  144	abdemo(Gs,[HA,BA], MaxDepth, HighLevel ),
  145		
  146	mapToTotalOrderPlan( HA, BA ,ValidOrderings),
  147	
  148	sortPlan([HA,ValidOrderings], SortedPlan),
  149
  150	reduceLoops(HA, ValidOrderings, FinalOrderings).
  151	
  152		
  153abdemo(Gs,[HA,BA], MaxDepth, HighLevel) :-
  154     init_gensym(t), 
  155     abdemo_top(Gs,[[[],[]],[[],[]]],[[HA,HC],[BA,BC]],[],N,0, MaxDepth, HighLevel).
  156    
  157     
  158abdemo_top(Gs,R1,R3,N1,N3,D, MaxDepth, HighLevel) :-
  159   
  160	abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth),  
  161	
  162	% ! cut removed here to generate mutli solutions -
  163	
  164	abdemo_cont(R2,R3,N2,N3,MaxDepth,HighLevel).
  165
  166/*
  167   abdemo_cont carries out one step of refinement, if necessary. It then
  168   resumes abdemo, but with an initial depth bound equal to the length of
  169   the plan so far. Obviously to start from 1 again would be pointless.
  170*/
  171
  172abdemo_cont([[HA,TC],RB],[[HA,TC],RB],N,N,MaxDepth,HighLevel) :-  all_executable(HA, HighLevel), !.
  173
  174abdemo_cont([[HA,HC],[BA,BC]],R2,N1,N3,MaxDepth,HighLevel) :-
  175     writeNoln('Abstract plan: '), writeNoln(HA), writeln(BA),
  176     
  177     refine([[HA,HC],[BA,BC]],N1,Gs,R1,N2),
  178     
  179     % Cut added here to prevent continous refinement with not(clipped(_,_,_)) added to goal
  180     % when generating multiple solutions. 
  181     % This does not have the implication that if something has mutliple refinements then only one of them
  182     % will be choosen. This is due to the fact that expand goals are treated in abdemo.
  183     !, 
  184     
  185     action_count([[HA,HC],[BA,BC]],D),
  186     
  187     abdemo_top(Gs,R1,R2,N2,N3,D,MaxDepth, HighLevel)
  188         
  189     %Joseph Wilk cut added 15/03/2004 AND removed 16/03/2004
  190     .
  191
  192     
  193/* abdemo_id is an iterative deepening version of abdemo. */
  194
  195/* 
  196Joseph Wilk
  197Modified 21/01/2004 - Support for bound on search */
  198
  199abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth) :- 
  200	D >= MaxDepth, writeNoln('No solution found within bound '), writeNoln(MaxDepth), fail. %So Stop searching
  201
  202abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth) :-
  203     D < MaxDepth, writeln('------------------------------------------------------------------------------'),
  204     writeNoln('Depth: '), writeln(D),writeln('goals:'),writeNoln(Gs), abdemo(Gs,R1,R2,N1,N2,D).
  205
  206     
  207/* Removed by Joe - No longer needed since the planner does not use iterative deepening 
  208abdemo_id(Gs,R1,R2,N1,N2,D1,MaxDepth) :- D1 < MaxDepth, 
  209																	   D2 is D1+1, 
  210																	   checkForLoop(D1),
  211																	   cleanup,
  212																	   abdemo_id(Gs,R1,R2,N1,N2,D2,MaxDepth).
  213																
  214checkForLoop(D):- fail.
  215*/
  216
  217																   
  218all_executable([], HighLevel).
  219
  220all_executable([happens(A,T1,T2)|R] ,HighLevel) :- (HighLevel =:= 0 ->
  221																		  true
  222																		;
  223																		executable(A), all_executable(R, HighLevel)
  224																		).
  225
  226
  227
  228/* ABDEMO */
  229
  230
  231/*
  232   abdemo/6 is a depth bounded abdemo. It fails if it can't generate a plan
  233   with DepthBound or fewer steps. Calls to abdemo/6 have the following form.
  234
  235        abdemo(Goals,ResidueIn,ResidueOut,
  236             NegationsIn,NegationsOut,DepthBound)
  237
  238*/
  239
  240abdemo(Gs,[[HA,TC1],[BA,TC2]],R,N1,N2,D) :-
  241    trace(on,0),
  242    writeNoln('Goals: '), writeln(Gs),
  243     writeNoln('Happens: '), writeln(HA),
  244     writeNoln('Befores: '), writeln(BA),
  245     writeNoln('Nafs: '), writeln(N1), fail.
  246
  247abdemo([],R,R,N,N,D).
  248
  249/*
  250   Now we have two clauses which are meta-level representations of the two
  251   event calculus axioms for holds_at.
  252
  253        holds_at(F,T) <- initiallyp(F) and not clipped(0,F,T)
  254
  255        holds_at(F,T3) <-
  256             happens(A,T1,T2) and T2 < T3 and
  257             initiates(A,F,T1) and not clipped(T1,F,T2)
  258
  259   Note the way the object-level axioms have been compiled into the
  260   meta-level. Note also that happens goals are not resolved against
  261   clauses in the object-level program. Instead, they're put straight into
  262   the residue. Resolving happens goals is the job of the refinement phase.
  263*/
  264
  265abdemo([holds_at(F1,T)|Gs1],R1,R3,N1,N4,D) :-
  266	
  267	 F1 \= neg(F2), 
  268     abresolve(initially(F1),R1,Gs2,R1,B),
  269     append(Gs2,Gs1,Gs3), add_neg([clipped(0,F1,T)],N1,N2),
  270     abdemo_naf([clipped(0,F1,T)],R1,R2,N2,N3,D),
  271     abdemo(Gs3,R2,R3,N3,N4,D).
  272
  273/*
  274   The order in which resolution steps are carried out in the next
  275   clause is crucial. We resolve initiates first in order to instantiate 
  276   A, but we don't want to proceed with sub-goals of initiates until
  277   we've added the corresponding happens and before facts to the residue.
  278*/
  279
  280abdemo([holds_at(F1,T3)|Gs1],R1,R6,N1,N5,D) :-
  281     
  282	 F1 \= neg(F2), 
  283     abresolve(initiates(A,F1,T1),R1,Gs2,R1,B1),
  284      
  285     %Provides Different ways to resolve a goal when backtracking
  286     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  287         
  288     abresolve(before(T2,T3),R2,[],R3,B3),
  289     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  290     add_neg([clipped(T1,F1,T3)],N2,N3),
  291     abdemo_naf([clipped(T1,F1,T3)],R4,R5,N3,N4,D),
  292     
  293     abdemo(Gs3,R5,R6,N4,N5,D),
  294          
  295     writeln('action:'),
  296     writeNoln(A),
  297     writeln('precondition:'),
  298     writeNoln(Gs2). 
  299     
  300
  301/*
  302   The next two clauses are a meta-level representation of the two
  303   event calculus axioms for not holds_at.
  304
  305        not holds_at(F,T) <- initiallyn(F) and not declipped(0,F,T)
  306
  307        not holds_at(F,T3) <-
  308             happens(A,T1,T2) and T2 < T3 and
  309             terminates(A,F,T1) and not declipped(T1,F,T2)
  310*/
  311
  312abdemo([holds_at(neg(F),T)|Gs1],R1,R3,N1,N4,D) :-
  313     abresolve(initially(neg(F)),R1,Gs2,R1,B),
  314     append(Gs2,Gs1,Gs3), add_neg([declipped(0,F,T)],N1,N2),
  315     abdemo_naf([declipped(0,F,T)],R1,R2,N2,N3,D),
  316     abdemo(Gs3,R2,R3,N3,N4,D).
  317
  318          
  319     
  320abdemo([holds_at(neg(F),T3)|Gs1],R1,R6,N1,N5,D) :-
  321     abresolve(terminates(A,F,T1),R1,Gs2,R1,B1),
  322   
  323     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  324     
  325     abresolve(before(T2,T3),R2,[],R3,B3),
  326     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  327     add_neg([declipped(T1,F,T3)],N2,N3),
  328     abdemo_naf([declipped(T1,F,T3)],R4,R5,N3,N4,D),
  329     abdemo(Gs3,R5,R6,N4,N5,D),
  330
  331      writeln('terminate action:'),
  332      writeNoln(A),
  333      
  334      writeln('precondition:'),
  335      writeNoln(Gs2). 
  336     
  337     
  338/*
  339   The next two clauses cater for happens goals.
  340
  341   Note that happens goals only appear either in the initial goal list or,
  342   in an "expand" goal, as a result of refinement. Note also that these
  343   clauses, because of the way abresolve(happens) works, will ensure sharing
  344   of sub-goals between compound events wherever possible.
  345*/
  346
  347abdemo([happens(A,T1,T2)|Gs],R1,R4,N1,N3,D) :-
  348     !, abresolve(happens(A,T1,T2),R1,[],R2,B), 
  349          
  350     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  351
  352abdemo([happens(A,T)|Gs],R1,R4,N1,N3,D) :-
  353     !, abresolve(happens(A,T),R1,[],R2,B), 
  354     
  355     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  356
  357/*
  358   The next clause deals with the expansion of compound actions. These appear
  359   as goals of the form expand([happens(A,T1,T2)|Bs]), where happens(A,T1,T2)
  360   is the compound action to be expanded and Bs is a list of "before" goals.
  361   These goals are placed in the goal list by calls to "refine". The various
  362   sub-goals generated by the expansion are treated in a careful order. First,
  363   the compound action's sub-actions are added to the residue. Then the "before"
  364   goals that "refine" took out of the residue are put back (with their newly
  365   skolemised time constants). The holds_at goals are solved next, on the
  366   assumption that they are either guards or supply context for the expansion.
  367   Then other, non event calculus goals are dealt with. Only then, with all the
  368   temporal ordering constraints sorted out, is it safe to tackle not(clipped)
  369   and not(declipped) goals, first those that are part of the compound action
  370   definition, then those recorded in the negations list.
  371*/
  372
  373abdemo([expand([happens(A,T1,T2)|Bs])|Gs1],R1,R8,N1,N8,D) :-
  374     !, axiom(happens(A,T1,T2),Gs2),
  375    
  376     add_sub_actions(Gs2,R1,R2,N1,N2,D,Hs),
  377
  378     solve_befores(Bs,R2,R3,N2,N3,D),
  379      
  380     abdemo_holds_ats(Gs2,R3,R4,N3,N4,D),
  381     
  382     % Joseph Wilk - Failure here causes a re-loop and matches another composite action resolution
  383         
  384     solve_other_goals(Gs2,R4,R5,N4,N5,D),
  385     
  386     check_clipping(Gs2,R5,R6,N5,N6,D),
  387     
  388     check_sub_action_nafs(Hs,N1,R6,R7,N6,N7,D),
  389     
  390     abdemo(Gs1,R7,R8,N7,N8,D).
  391
  392    
  393          
  394/*
  395   The last two clauses cater for the general case (ie: goals other
  396   than holds_at and happens). They're also used to tackle domain
  397   constraints (ie: holds_at if holds_at clauses).
  398*/
  399
  400abdemo([not(G)|Gs],R1,R3,N1,N4,D) :-
  401     !, abdemo_naf([G],R1,R2,N1,N2,D), add_neg([G],N2,N3),
  402     abdemo(Gs,R2,R3,N3,N4,D).
  403
  404     
  405abdemo([G|Gs1],R1,R3,N1,N2,D) :-
  406     abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
  407     abdemo(Gs3,R2,R3,N1,N2,D).
  408     
  409     %CUT added by JOE 13/03/2004 AND REMOVED! 17052004:3:23pm due to the fact that only the goal was being re-evaluated
  410     
  411
  412% currently catches abstract actions!!!!
  413abdemo([G|Gs],R1,R3,N1,N4,D ) :- writeNoln( 'currently unknown information about(may be compound!):'), writeNoln(G), 
  414fail.
  415
  416
  417/*
  418
  419Removed Joseph Wilk - depth first search is used instead!
  420
  421check_depth(R,D,L) :- trace(on,1), 
  422								   action_count(R,L), 
  423								   writeln('Actions:'),
  424								   writeln(R),
  425								   writeln('Action count:'), writeNoln(L), fail.
  426								
  427%Keep track of the current action depth
  428check_depth(R,D,L) :- action_count(R,L), L =< D, D =< 1000.
  429
  430% The action list is greater than the current Depth
  431check_depth(R,D,L) :- trace(on, 1), writeln('Maximum bound reached'),!, fail.
  432*/
  433
  434
  435action_count([[HA,TC],RB],L) :- length(HA,L).
  436
  437
  438
  439
  440/* EXPANSION OF COMPOUND ACTIONS */
  441
  442
  443/* The following collection of predicates are called by abdemo(expand). */
  444
  445
  446abdemo_holds_ats([],R,R,N,N,D).
  447
  448abdemo_holds_ats([holds_at(F,T)|Gs],R1,R3,N1,N3,D) :-
  449     !, 
  450     abdemo([holds_at(F,T)],R1,R2,N1,N2,D),
  451     
  452     %cut added Joseph Wilk 16/03/2004
  453     !,
  454     
  455     
  456     abdemo_holds_ats(Gs,R2,R3,N2,N3,D).
  457
  458abdemo_holds_ats([G|Gs],R1,R2,N1,N2,D) :-
  459 abdemo_holds_ats(Gs,R1,R2,N1,N2,D).
  460
  461
  462solve_other_goals([],R,R,N,N,D).
  463
  464solve_other_goals([G|Gs],R1,R3,N1,N3,D) :-
  465     G \= holds_at(F,T), G \= happens(A,T1,T2),
  466     G \= happens(A,T), G \= before(T1,T2),
  467    G \= not(clipped(T1,F,T2)), G \= not(declipped(T1,F,T2)), !,
  468     abdemo([G],R1,R2,N1,N2,D),
  469     solve_other_goals(Gs,R2,R3,N2,N3,D).
  470
  471solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-
  472     solve_other_goals(Gs,R1,R2,N1,N2,D).
  473
  474     
  475     
  476% Modified Joseph Wilk 24/02/2004 7:54pm
  477% The idea is if we hit this clause we are backtracking and only want to move backwards not forwards
  478
  479solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-  fail.
  480
  481
  482
  483/*
  484   In its last argument, add_sub_actions accumulates a list of new actions
  485   added to the residue, so that subsequent re-checking of not(clipped) and
  486   not(declipped) goals can be done via check_nafs rather than the less
  487   efficient abdemo_nafs.
  488*/
  489
  490add_sub_actions([],R,R,N,N,D,[]).
  491
  492add_sub_actions([happens(A,T1,T2)|Gs],R1,R3,N1,N3,D,Hs2) :-
  493     !,
  494     
  495     abresolve(happens(A,T1,T2),R1,[],R2,B),
  496     
  497     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T1,T2),Hs1,Hs2).
  498
  499add_sub_actions([happens(A,T)|Gs],R1,R3,N1,N3,D,Hs2) :-
  500     !, 
  501           
  502     abresolve(happens(A,T),R1,[],R2,B), 
  503          
  504     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T,T),Hs1,Hs2).
  505
  506add_sub_actions([before(T1,T2)|Gs],R1,R3,N1,N3,D,Hs) :-
  507     !, abresolve(before(T1,T2),R1,[],R2,B),
  508     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs).
  509
  510add_sub_actions([G|Gs],R1,R2,N1,N2,D,Hs) :-
  511	add_sub_actions(Gs,R1,R2,N1,N2,D,Hs).
  512
  513
  514cond_add(false,H,Hs,Hs) :- !.
  515
  516cond_add(true,H,Hs,[H|Hs]).
  517
  518
  519solve_befores([],R,R,N,N,D).
  520
  521
  522
  523solve_befores([before(T1,T2)|Gs],R1,R3,N1,N3,D) :-
  524     !, abdemo([before(T1,T2)],R1,R2,N1,N2,D),
  525     solve_befores(Gs,R2,R3,N2,N3,D),!. %CUT introduced by JOSEPH WILK 30/05/04
  526
  527solve_befores([G|Gs],R1,R2,N1,N2,D) :-
  528     solve_befores(Gs,R1,R2,N1,N2,D),!. %CUT introduced by JOSEPH WILK 30/05/04
  529
  530
  531check_sub_action_nafs([],N1,R,R,N2,N2,D) :- !. 
  532
  533check_sub_action_nafs([happens(A,T1,T2)|Hs],N1,R1,R3,N2,N4,D) :-
  534     check_nafs(A,T1,T2,N1,R1,R2,N2,N3,D),
  535     check_sub_action_nafs(Hs,N1,R2,R3,N3,N4,D).
  536
  537
  538check_clipping([],R,R,N,N,D) :- !. 
  539
  540check_clipping([not(clipped(T1,F,T2))|Gs],R1,R3,N1,N3,D) :-
  541     !, abdemo_naf([clipped(T1,F,T2)],R1,R2,N1,N2,D),
  542     check_clipping(Gs,R2,R3,N2,N3,D).
  543
  544check_clipping([not(declipped(T1,F,T2))|Gs],R1,R3,N1,N3,D) :-
  545     !, abdemo_naf([declipped(T1,F,T2)],R1,R2,N1,N2,D),
  546     check_clipping(Gs,R2,R3,N2,N3,D).
  547
  548check_clipping([G|Gs],R1,R2,N1,N2,D) :-
  549     check_clipping(Gs,R1,R2,N1,N2,D).
  550
  551
  552
  553
  554/* ABRESOLVE */
  555
  556
  557/*
  558   The form of a call to abresolve is as follows.
  559
  560        abresolve(Goal,ResidueIn,Goals,ResidueOut,Flag)
  561
  562   where Goals is the body of clause resolved with, and Flag is set to true
  563   if a happens fact has been added to the residue.
  564*/
  565
  566abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
  567abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- axiom(terminates(A,F,T),Gs).
  568
  569% impossible action supported
  570abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- !, axiom(impossible(A,T),Gs).
  571
  572abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
  573abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- !, axiom(initiates(A,F,T),Gs).
  574
  575/*
  576   happens goals get checked to see if they are already in the residue.
  577   This permits the re-use of actions already in the residue. However,
  578   this decision may lead to later failure, in which case we try adding
  579   a new action to the residue.
  580
  581   happens goals aren't resolved against object-level program clauses.
  582   Only goals that are marked as expand(goal) are resolved against
  583   program clauses, and this is done by abdemo.
  584
  585   Time variables get skolemised, but not action variables because
  586   they end up getting instantiated anyway.
  587*/
  588
  589abresolve(happens(A,T),R1,Gs,R2,B) :- !, abresolve(happens(A,T,T),R1,Gs,R2,B).
  590
  591abresolve(happens(A,T1,T2),[[HA,TC],RB],[],[[HA,TC],RB],false) :-
  592     member(happens(A,T1,T2),HA),
  593     
  594     %Joseph Wilk Modification
  595     %added to prevent re-evaluating happens with multiple goals
  596     %Otherwise happens occur which are duplicates in the plan
  597     !.
  598
  599abresolve(happens(A,T,T),[[HA,TC],RB],[],[[[happens(A,T,T)|HA],TC],RB],B) :-
  600     executable(A), !, B = true, skolemise(T).
  601
  602abresolve(happens(A,T1,T2),R1,[],R2,B) :-
  603     !, B = true, skolemise(T1), skolemise(T2), add_happens(A,T1,T2,R1,R2).
  604
  605/*
  606   If either X or Y is not bound in a call to abresolve(before(X,Y)) then
  607   they get skolemised.
  608*/
  609
  610abresolve(before(X,Y),R,[],R,false) :-
  611     skolemise(X), skolemise(Y), demo_before(X,Y,R), !.
  612
  613abresolve(before(X,Y),R1,[],R2,B) :-
  614     !, B = false, skolemise(X), skolemise(Y), \+ demo_beq(Y,X,R1),
  615     add_before(X,Y,R1,R2).
  616
  617/*
  618   The predicates "diff" (meaning not equal) and "is" (for evaluating
  619   arithmetic expressions) are built in.
  620*/
  621
  622abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y.
  623
  624abresolve(is(X,Y),R,[],R,false) :- !, X is Y.
  625
  626
  627
  628% Joseph wilk modification - 26/02/2004 6:56pm
  629% access to pure prolog breaking through meta-interpreter
  630
  631abresolve(prolog(Code),R,[],R,false) :- !, Code.
  632
  633%Access Knowledge base
  634abresolve(knowledgeBase(Username, GroupList),R,[],R,false) :- !, knowledgeDb :: lookupUserProlog(Username, Groups), !,listMember(GroupList, Groups),!.
  635
  636%Check html attributes
  637abresolve(valid_html_form(Type, Att),R,[],R,false):- !, valid_html_form(Type,Att).
  638
  639%Check html children
  640abresolve(valid_html_formChildren(Type, Children),R,[],R,false):- !, valid_html_formChildren(Type,Children).
  641
  642
  643
  644breakupResidual( [[X,Y],[Z,A]]   , X).
  645
  646
  647%Attempt to test for membership of Actions list
  648abresolve(notOccured(Action),R,[],R,false) :- 
  649				!,			
  650				breakupResidual(R,Actions),!,
  651				\+ member(Action, Actions).
  652				
  653abresolve(occured(Action),R,[],R,false) :- 
  654				!,			
  655				breakupResidual(R,Actions),!,
  656				member(Action, Actions).
  657
  658				
  659				
  660				
  661abresolve(G,R,[],[G|R],false) :-  abducible(G).
  662
  663abresolve(G,R,Gs,R,false) :-   writeln('--------------------'), writeNoln(G),writeln('--------------------'), axiom(G,Gs).
  664
  665
  666
  667
  668/* ABDEMO_NAFS and CHECK_NAFS */
  669
  670
  671/*
  672   abdemo_nafs([G1...Gn],R1,R2) demos not(G1) and ... and not(Gn).
  673
  674   Calls to abdemo_naf have the following form.
  675
  676        abdemo_nafs(Negations,ResidueIn,ResidueOut,
  677             NegationsIn,NegationsOut,DepthIn,DepthOut)
  678
  679   where Negations is the list of negations to be established, ResidueIn
  680   is the old residue, ResidueOut is the new residue (abdemo_nafs can add
  681   both before and happens facts, as well as other abducibles, to the
  682   residue), NegationsIn is the old list of negations (same as Negations
  683   for top-level call), and NegationsOut is the new list of negations
  684   (abdemo_nafs can add new clipped goals to NegationsIn).
  685
  686   DepthIn and DepthOut keep track of the number of sub-goals generated,
  687   for iterative deepening purposes.
  688*/
  689
  690
  691abdemo_nafs([],R,R,N,N,D).
  692
  693abdemo_nafs([N|Ns],R1,R3,N1,N3,D) :-
  694     abdemo_naf(N,R1,R2,N1,N2,D), abdemo_nafs(Ns,R2,R3,N2,N3,D).
  695
  696
  697/*
  698Joseph Wilk
  699Impossible introduced 21/01/04
  700
  701   abdemo_naf([G1...Gn],R1,R2) demos not((G1) and ... and (Gn)).
  702
  703   As for abdemo, the main event calculus axioms are compiled into the
  704   meta-level in abdemo_naf. In addition to the two holds_at axioms, we
  705   have,
  706
  707        clipped(T1,F,T3) <-
  708             happens(A,T2) and T1 < T2 < T3 and
  709             [terminates(A,F,T2) or releases(A,F,T2) or impossible(A,T2)]
  710             
  711        declipped(T1,F,T3) <-
  712             happens(A,T2) and T1 < T2 < T3 and
  713             [initiates(A,F,T2) or releases(A,F,T2) or impossible(A,T2)]
  714                          
  715
  716   We have to use findall here, because all ways of achieving a goal
  717   have to fail for the goal itself to fail.
  718
  719   Note that only the two-argument version of happens is used, because
  720   the residue only contains instantaneous actions, and 
  721   *** the effects of compound actions are assumed to match the effects of their
  722   component actions. ***
  723*/
  724
  725abdemo_naf([clipped(T1,F,T4)|Gs1],R1,R2,N1,N2,D) :-
  726     !, findall(Gs3,
  727          (abresolve(terms_or_rels_or_imposs(A,F,T2),R1,Gs2,R1,false),
  728           abresolve(happens(A,T2,T3),R1,[],R1,false),
  729          append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  730     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  731
  732abdemo_naf([declipped(T1,F,T4)|Gs1],R1,R2,N1,N2,D) :-
  733     !, findall(Gs3,
  734          (abresolve(inits_or_rels_or_imposs(A,F,T2),R1,Gs2,R1,false),
  735          abresolve(happens(A,T2,T3),R1,[],R1,false),
  736          append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  737     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  738
  739/*
  740   To show the classical negation of holds_at(F) (which is what we want), we
  741   have to show that holds_at(neg(F)). Conversely, to show the classical
  742   negation of holds_at(neg(F)) we have to show holds_at(F). Within a call
  743   to abdemo_naf, we can add both happens and before (and other abducibles)
  744   to the residue. This removes a potential source of incompleteness.
  745
  746   Note that F must be a ground term to preserve soundness and completeness.
  747   To guarantee this, all variables that occur in the body of an
  748   initiates, terminates or releases clause must occur in the fluent
  749   argument in its head.
  750*/
  751
  752/* DANGER: Cut in next clause rules out other ways to solve holds_at(F2,T). */
  753
  754abdemo_naf([holds_at(F1,T)|Gs1],R1,R3,N1,N3,D) :-
  755     opposite(F1,F2), copy_term(Gs1,Gs2),
  756     abdemo([holds_at(F2,T)],R1,R2,N1,N2,D), !,
  757     abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  758
  759abdemo_naf([holds_at(F,T)|Gs],R1,R2,N1,N2,D) :-
  760     !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  761
  762/*
  763   Special facilities for handling temporal ordering facts are built in.
  764   We can add a before fact to the residue to preserve the failure of
  765   a clipped goal. The failure of a before goal does NOT mean that the
  766   negation of that goal is assumed to be true. (The Clark completion is
  767   not applicable to temporal ordering facts.) Rather, to make before(X,Y)
  768   fail, before(Y,X) has to follow. One way to achieve this is to add
  769   before(Y,X) to the residue.
  770*/
  771
  772abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- X == Y, !.
  773
  774abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- demo_before(Y,X,R), !.
  775
  776abdemo_naf([before(X,Y)|Gs1],R1,R2,N1,N2,D) :-
  777     !, append(Gs1,[postponed(before(X,Y))],Gs2),
  778     abdemo_naf(Gs2,R1,R2,N1,N2,D).
  779
  780/*
  781   A before fact is only added to the residue as a last resort. Accordingly,
  782   if we encounter a before(X,Y) goal and cannot show before(Y,X), we
  783   postpone that goal until we've tried other possibilities. A postponed
  784   before goal appears in the goal list as postponed(before(X,Y)).
  785*/
  786
  787abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N,N,D) :-
  788     \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
  789
  790abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N1,N2,D) :-
  791     !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  792
  793/* 
  794   We drop through to the general case for goals other than special event
  795   calculus goals.
  796*/
  797
  798/* DANGER: Cut in next clause rules out other ways to solve G. */
  799
  800abdemo_naf([not(G)|Gs1],R1,R3,N1,N3,D) :-
  801     copy_term(Gs1,Gs2), abdemo([G],R1,R2,N1,N2,D), !,
  802     abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  803
  804abdemo_naf([not(G)|Gs],R1,R2,N1,N2,D) :- !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  805
  806abdemo_naf([G|Gs1],R,R,N,N,D) :- \+ abresolve(G,R,Gs2,R,false), !.
  807
  808abdemo_naf([G1|Gs1],R1,R2,N1,N2,D) :-
  809     findall(Gs2,(abresolve(G1,R1,Gs3,R1,false),append(Gs3,Gs1,Gs2)),Gss),
  810     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  811
  812
  813/*
  814   abdemo_naf_cont gets an extra opportunity to succeed if the residue
  815   has been altered. This is determined by comparing R1 with R2. If
  816   a sub-goal has failed and the residue hasn't been altered, there's
  817   no need to look for other ways to prove the negation of the overall goal.
  818*/
  819
  820abdemo_naf_cont(R1,Gs,R2,R2,N,N,D).
  821
  822abdemo_naf_cont(R1,Gs,R2,R3,N1,N2,D) :-
  823     R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2,D).
  824
  825
  826/*
  827   check_nafs is just like abdemo_nafs, except that it only checks
  828   negated clipped and declipped facts against the most recent event
  829   added to the residue. To check one of these negations, not only can
  830   we confine our attention to the most recent event, but we can ignore
  831   that event if it doesn't fall inside the interval covered by the
  832   clipped/declipped in question. Of course, the negated clipped/declipped
  833   fact might depend on other holds_at facts. But their preservation is
  834   ensured because the clipped/declipped negation they themselves depend
  835   on will also be checked.
  836*/
  837
  838
  839check_nafs(false,N1,R,R,N2,N2,D) :- !.
  840
  841check_nafs(true,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D) :-
  842     check_nafs(A,T1,T2,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D).
  843
  844check_nafs(A,T1,T2,[],R,R,N,N,D).
  845
  846check_nafs(A,T1,T2,[N|Ns],R1,R3,N1,N3,D) :-
  847     check_naf(A,T1,T2,N,R1,R2,N1,N2,D),
  848     check_nafs(A,T1,T2,Ns,R2,R3,N2,N3,D).
  849
  850
  851check_naf(A,T2,T3,[clipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  852     !, findall([before(T1,T3),before(T2,T4)|Gs],
  853          (abresolve(terms_or_rels_or_imposs(A,F,T2),R1,Gs,R1,false)),Gss),
  854     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  855
  856check_naf(A,T2,T3,[declipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  857     !, findall([before(T1,T3),before(T2,T4)|Gs],
  858          (abresolve(inits_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
  859     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  860
  861check_naf(A,T1,T2,N,R1,R2,N1,N2,D) :- abdemo_naf(N,R1,R2,N1,N2,D).
  862
  863
  864
  865
  866/* DEMO_BEFORE, ADD_BEFORE and ADD_HAPPENS */
  867
  868
  869/*
  870   demo_before simply checks membership of the transitive closure half of
  871   the temporal ordering part of the residue. Likewise demo_beq checks for
  872   demo_before or for membership of the transitive closure half of the
  873   happens part of the residue.
  874*/
  875
  876demo_before(0,Y,R) :- !, Y \= 0.
  877
  878demo_before(X,Y,[RH,[BA,TC]]) :- member(before(X,Y),TC).
  879
  880/* demo_beq is demo before or equal. */
  881
  882demo_beq(X,Y,R) :- X == Y, !.
  883
  884demo_beq(X,Y,R) :- demo_before(X,Y,R), !.
  885
  886demo_beq(X,Y,[[HA,TC],RB]) :- member(beq(X,Y),TC).
  887
  888
  889/*
  890   add_before(X,Y,R1,R2) adds before(X,Y) to the residue R1 giving R2.
  891   It does this by maintaining the transitive closure of the before and beq
  892   relations in R2, and assumes that R1 is already transitively closed.
  893   R1 and R2 are just the temporal ordering parts of the residue.
  894*/
  895
  896add_before(X,Y,[RH,[BA,TC]],[RH,[BA,TC]]) :- member(before(X,Y),TC), !.
  897
  898add_before(X,Y,[[HA,HC],[BA,BC1]],[[HA,HC],[[before(X,Y)|BA],BC2]]) :-
  899     \+ demo_beq(Y,X,[[HA,HC],[BA,BC1]]), find_bef_connections(X,Y,BC1,C1,C2),
  900     find_beq_connections(X,Y,HC,C3,C4), delete(C3,X,C5), delete(C4,Y,C6),
  901     append(C5,C1,C7), append(C6,C2,C8),
  902     cross_prod_bef(C7,C8,C9,BC1), append(C9,BC1,BC2).
  903
  904/*
  905   add_happens(A,T1,T2,R1,R2) adds happens(A,T1,T2) to the residue R1
  906   giving R2. Because happens(A,T1,T2) -> T1 <= T2, this necessitates
  907   updating the transitive closures of the before and beq facts in the residue.
  908   Duplicates aren't checked for, as it's assumed this is done by the
  909   calling predicate.
  910*/
  911
  912add_happens(A,T1,T2,[[HA,HC1],[BA,BC1]],[[[happens(A,T1,T2)|HA],HC2],[BA,BC2]]) :-
  913     \+ demo_before(T2,T1,[[HA,HC1],[BA,BC1]]),
  914     find_beq_connections(T1,T2,HC1,C1,C2), cross_prod_beq(C1,C2,C3,HC1),
  915     append(C3,HC1,HC2), find_bef_connections(T1,T2,BC1,C4,C5),
  916     cross_prod_bef(C4,C5,C6,BC1), delete(C6,before(T1,T2),C7),
  917     append(C7,BC1,BC2).
  918
  919/*
  920   find_bef_connections(X,Y,TC,C1,C2) creates two lists, C1 and C2,
  921   containing respectively all the time points before X and after
  922   Y according to TC, which is assumed to be transitively closed.
  923*/
  924
  925find_bef_connections(X,Y,[],[X],[Y]).
  926
  927find_bef_connections(X,Y,[before(Z,X)|R],[Z|C1],C2) :-
  928     !, find_bef_connections(X,Y,R,C1,C2).
  929
  930find_bef_connections(X,Y,[before(Y,Z)|R],C1,[Z|C2]) :-
  931     !, find_bef_connections(X,Y,R,C1,C2).
  932
  933find_bef_connections(X,Y,[before(Z1,Z2)|R],C1,C2) :-
  934     find_bef_connections(X,Y,R,C1,C2).
  935
  936/*
  937   find_beq_connections is like find_bef_connections, except that it works
  938   on the transtive closure of happens part of the residue.
  939*/
  940
  941find_beq_connections(X,Y,[],[X],[Y]).
  942
  943find_beq_connections(X,Y,[beq(Z,X)|R],[Z|C1],C2) :-
  944     !, find_beq_connections(X,Y,R,C1,C2).
  945
  946find_beq_connections(X,Y,[beq(Y,Z)|R],C1,[Z|C2]) :-
  947     !, find_beq_connections(X,Y,R,C1,C2).
  948
  949find_beq_connections(X,Y,[beq(Z1,Z2)|R],C1,C2) :-
  950     find_beq_connections(X,Y,R,C1,C2).
  951
  952
  953cross_prod_bef([],C,[],R).
  954
  955cross_prod_bef([X|C1],C2,R3,R) :-
  956     cross_one_bef(X,C2,R1,R), cross_prod_bef(C1,C2,R2,R), append(R1,R2,R3).
  957
  958cross_one_bef(X,[],[],R).
  959
  960cross_one_bef(X,[Y|C],[before(X,Y)|R1],R) :-
  961     \+ member(before(X,Y),R), !, cross_one_bef(X,C,R1,R).
  962
  963cross_one_bef(X,[Y|C],R1,R) :- cross_one_bef(X,C,R1,R).
  964
  965
  966cross_prod_beq([],C,[],R).
  967
  968cross_prod_beq([X|C1],C2,R3,R) :-
  969     cross_one_beq(X,C2,R1,R), cross_prod_beq(C1,C2,R2,R), append(R1,R2,R3).
  970
  971cross_one_beq(X,[],[],R).
  972
  973cross_one_beq(X,[Y|C],[beq(X,Y)|R1],R) :-
  974     \+ member(beq(X,Y),R), !, cross_one_beq(X,C,R1,R).
  975
  976cross_one_beq(X,[Y|C],R1,R) :- cross_one_beq(X,C,R1,R).
  977
  978
  979
  980
  981/* REFINE */
  982
  983
  984/*
  985   refine(R1,N1,Gs,R2,N2) takes the earliest compound action out of the residue
  986   R1 and puts it in the goal list Gs, along with all "before", not(clipped) and
  987   not(declipped) facts that refer to the same time points. These time points
  988   are unskolemised, so that they can be bound to existing time points in the
  989   residue, thus permitting sub-actions to be shared between abstract actions.
  990   This almost restores the state of computation to the state S before the chosen
  991   action was added to the residue in the first place. But not quite, because
  992   some derived before facts will be retained in the transitive closure part
  993   of the before part of the residue that weren't there in state S. This doesn't
  994   matter, however, because these derived facts will need to be there eventually
  995   anyway, when those before facts that have been transferred from residue to goal
  996   list get put back in the residue.
  997
  998   The compound action extracted from the residue is marked for expansion by
  999   inserting it in the goal list in the form expand([happens(A,T1,T2)|Bs]),
 1000   where Bs is the list of "before" facts taken out of the residue, as
 1001   described above. When abdemo comes across a goal of this form, it will
 1002   resolve the "happens" part against program clauses. The reason for
 1003   not doing this resolution here is that we want to backtrack to alternative
 1004   definitions of a compound goal inside the iterative deepening search, not
 1005   outside it. This ensures the desired behaviour for compound actions which
 1006   expand to one series of sub-actions given certain conditions but to another
 1007   series of sub-actions given other conditions. Otherwise the check for these
 1008   conditions, which will be a holds_at goal in the compound action definition,
 1009   is in danger of being treated as a goal to be established instead of just
 1010   checked.
 1011*/
 1012
 1013refine([[HA1,HC1],[BA1,BC1]],N1,Gs,[[HA2,HC2],[BA2,BC2]],N3) :-
 1014     split_happens(HA1,[BA1,BC1],happens(A,T1,T2),HA2),
 1015     split_beqs(HC1,T1,T2,T3,T4,HC3,HC2),
 1016     split_befores(BA1,T1,T2,T3,T4,BA3,BA2),
 1017     split_befores(BC1,T1,T2,T3,T4,BC3,BC2),
 1018     split_nafs(N1,T1,T2,T3,T4,N2,N3),
 1019     append([expand([happens(A,T3,T4)|BA3])],N2,Gs).
 1020
 1021
 1022/*
 1023   split_happens(RH1,RB,H,RH2) holds if H is the earliest non-executable
 1024   (abstract) action in RH1 according to RB. The remainder of RH1 ends up in
 1025   RH2. If there are no non-executable actions, H is the earliest action.
 1026*/
 1027
 1028split_happens([happens(A,T1,T2)],RB,happens(A,T1,T2),[]) :- !.
 1029
 1030split_happens([happens(A1,T1,T2)|RH1],RB,happens(A3,T5,T6),
 1031          [happens(A4,T7,T8)|RH2]) :-
 1032     split_happens(RH1,RB,happens(A2,T3,T4),RH2),
 1033     order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1034          happens(A3,T5,T6),happens(A4,T7,T8)).
 1035
 1036
 1037order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1038          happens(A1,T1,T2),happens(A2,T3,T4)) :-
 1039     \+ executable(A1), executable(A2), !.
 1040
 1041order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1042          happens(A2,T3,T4),happens(A1,T1,T2)) :-
 1043     \+ executable(A2), executable(A1), !.
 1044
 1045order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1046          happens(A1,T1,T2),happens(A2,T3,T4)) :-
 1047     demo_before(T1,T3,[[],RB]), !.
 1048
 1049order(happens(A1,T1,T2),happens(A2,T3,T4),RB,happens(A2,T3,T4),happens(A1,T1,T2)).
 1050
 1051
 1052split_befores([],T1,T2,T3,T4,[],[]).
 1053
 1054split_befores([before(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[before(T1,T2)|Bs3]) :-
 1055     no_match(T1,T2,T3,T4), !, split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1056
 1057split_befores([before(T1,T2)|Bs1],T3,T4,T5,T6,[before(T7,T8)|Bs2],Bs3) :-
 1058     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1059     split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1060
 1061
 1062split_beqs([],T1,T2,T3,T4,[],[]).
 1063
 1064split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[beq(T1,T2)|Bs3]) :-
 1065     no_match(T1,T2,T3,T4), !, split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1066
 1067split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,[beq(T7,T8)|Bs2],Bs3) :-
 1068     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1069     split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1070
 1071
 1072split_nafs([],T1,T2,T3,T4,[],[]).
 1073
 1074split_nafs([[clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,[[clipped(T1,F,T2)]|Bs3]) :-
 1075     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1076
 1077split_nafs([[clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
 1078          [not(clipped(T7,F,T8))|Bs2],Bs3) :-
 1079     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1080     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1081
 1082split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,
 1083          [[declipped(T1,F,T2)]|Bs3]) :-
 1084     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1085
 1086split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
 1087          [not(declipped(T7,F,T8))|Bs2],Bs3) :-
 1088     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1089     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1090
 1091split_nafs([N|Bs1],T3,T4,T5,T6,Bs2,[N|Bs3]) :-
 1092     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1093     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1094
 1095
 1096substitute_time(T1,T1,T2,T3,T4,T3) :- !.
 1097substitute_time(T2,T1,T2,T3,T4,T4) :- !.
 1098substitute_time(T1,T2,T3,T4,T5,T1).
 1099
 1100no_match(T1,T2,T3,T4) :- T1 \= T3, T2 \= T3, T1 \= T4, T2 \= T4.
 1101
 1102
 1103
 1104
 1105/* OTHER BITS AND PIECES */
 1106
 1107
 1108/*
 1109   add_neg(N,Ns1,Ns2) adds goal N to the list of (lists of) negations Ns1,
 1110   giving Ns2. Duplicates are ignored, but N must be fully bound.
 1111*/
 1112
 1113add_neg(N,Ns,Ns) :- member(N,Ns), !.
 1114add_neg(N,Ns,[N|Ns]).
 1115
 1116
 1117/* append_negs is just append, but ignoring duplicates. */
 1118
 1119append_negs([],[],[]).
 1120append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
 1121
 1122
 1123/* delete(X,[],[]).  redundant
 1124   delete(X,[X|L],L) :- !.
 1125   delete(X,[Y|L1],[Y|L2]) :- delete(X,L1,L2).
 1126*/
 1127
 1128% Tail recursive count 
 1129count([],Result, Result). 
 1130count([Head|Tail], Accum, Result) :- 
 1131	IncAccum is Accum+1,
 1132	count(Tail,IncAccum,Result).
 1133
 1134listlength( [Head|Tail], Result ) :-
 1135	count([Head|Tail],0,Result).	
 1136
 1137
 1138/* Skolemisation */
 1139
 1140skolemise(T) :- var(T), gensym(t,T), !.
 1141skolemise(T).
 1142
 1143
 1144opposite(neg(F),F) :- !.
 1145opposite(F,neg(F)).
 1146
 1147trace(off,0).
 1148trace(off,1)