1%
    2%  sitcalc.pl:   domain-independent sitcalc predicates.
    3%
    4%  Copyright 2008, Ryan Kelly
    5%
    6
    7:- multifile(adp_fluent/3).    8:- index(adp_fluent(1,1,0)).    9:- multifile(constraint/1).   10:- multifile(initially/1).   11:- multifile(holds0/1).   12:- multifile(knows0/1).   13
   14:- discontiguous(causes_true/3).   15:- discontiguous(causes_false/3).   16
   17%
   18%  action_with_vars(A,Vs)  -  get an action term with variable arguments
   19%
   20%  This predicate binds A to an action term with all arguments set to
   21%  variables, and Vs to a matching variable list.
   22%
   23action_with_vars(A,Vs) :-
   24    prim_action(At),
   25    At =.. [F|ArgTypes],
   26    awv_collect(ArgTypes,Args,Vs),
   27    A =.. [F|Args].
   28
   29awv_collect([],[],[]).
   30awv_collect([T|Ts],[Y|Ys],[Y:T|Vs]) :-
   31    awv_collect(Ts,Ys,Vs).
   32
   33
   34%
   35%  Specify domain-independent constraints, and some things we can safely
   36%  assume will hold in any initial situation.
   37%
   38%constraint(true).
   39%constraint(~false).
   40initially(~knows(Agt,false)) :-
   41    agent(Agt).
   42
   43%
   44%  Perform reasoning relative to the domain axioms.
   45%
   46domain_axioms(Ax) :-
   47   findall(C,constraint(C),Ax1),
   48    maplist(make_cknows_fml,Ax1,Ax).
   49domain_falsehood(Fml) :-
   50    domain_axioms(Axs),
   51    entails(Axs,~Fml).
   52domain_tautology(Fml) :-
   53    domain_axioms(Axs),
   54    entails(Axs,Fml).
   55
   56make_cknows_fml(F,CK) :-
   57    setof(A,agent(A),Agts),
   58    joinlist('|',Agts,E),
   59    CK = pknows0((E*),F).
   60
   61%
   62%  adp_fluent(F,A,C)  -  C is the defn for ADP fluent F applied to action A
   63%
   64%  The specific ADP fluent definitions are given in domain.pl, but we give
   65%  a default implementation for the case when A is a variable, which simply
   66%  enumerates each possible action and conjoins the individual definitions.
   67%
   68adp_fluent(F,A,C) :-
   69    var(A), !,
   70    (bagof(Ft,adp_fluent_bagof(F,A,Ft),Fts) ->
   71        joinlist(('|'),Fts,Ftmp),
   72        simplify(Ftmp,C)
   73    ;
   74        C=F
   75    ).
   76
   77adp_fluent_bagof(F,A,F1) :-
   78    action_with_vars(A1,V),
   79    adp_fluent(F,A1,F1t),
   80    F1 = ?(V : (F1t & (A=A1))).
   81
   82%
   83%  Useful ADPs that can be defined in terms of other, simpler ADPs
   84%
   85
   86adp_fluent(pbu(Agt),A,C) :-
   87    adp_fluent(poss,A,C1),
   88    adp_fluent(canObs(Agt),A,C2),
   89    C = C1 & ~C2.
   90
   91adp_fluent(obs(Agt,O),A,C) :-
   92    ( adp_fluent(canObs(Agt),A,CO) -> true ; CO=false),
   93    ( adp_fluent(canSense(Agt),A,CS) -> true ; CS=false),
   94    ( adp_fluent(sr(R),A,CR) -> true ; CR=(R=nil)),
   95    C = ((~CO & (O=nil)) | (CO & ~CS & (O=A)) | (CO & CS & ?([R:result]: CR & (O=pair(A,R))))).
   96
   97
   98%
   99%  regression(+F,+A,-Fr) - Fr is the regression of F over action A
  100%
  101%  This predicate calculates the regression of a fluent F with respect to
  102%  an action A, yielding a new fluent Fr.  If A is free, will consider all
  103%  types of action that could affect the fluent.
  104%
  105
  106%  If A is non-free, regression1 will succeed only once.
  107regression(F,A,Fr) :-
  108    nonvar(A), !,
  109    regression1(F,A,Frt),
  110    simplify(Frt,Fr).
  111
  112%  If A is free, find all actions which could affect F.
  113regression(F,A,Fr) :-
  114    var(A),
  115    (bagof(Ft,B^regression_bagof(F,A,B,Ft),Fts) ->
  116        joinlist(('|'),Fts,Ftmp),
  117        simplify((Ftmp | ((A=nil) & F)),Fr)
  118    ;
  119        Fr=F
  120    ).
  121
  122regression_bagof(F,A,B,Ft) :-
  123    action_with_vars(B,V),
  124    regression1(F,B,Ftr),
  125    Ft = ?(V : (Ftr & (A=B))).
  126
  127
  128% Regression base case, a primitive fluent.
  129% Build successor state axiom from causes_true/cases_false
  130regression1(F,A,Fr) :-
  131    is_atom(F), F \= (_ = _), F \= (_ \= _),
  132    (causes_true(F,A,Ep) -> true ; Ep = false),
  133    (causes_false(F,A,En) -> true ; En = false),
  134    simplify(Ep | (F & ~En),Fr).
  135
  136% No functional fluents, so equality is rigid
  137regression1(T1=T2,_,T1=T2).
  138regression1(T1\=T2,_,T1\=T2).
  139
  140% Regression is pushed inside the logical operators
  141regression1(!(X : P),A,!(X : R)) :-
  142    regression1(P,A,R).
  143regression1(?(X : P),A,?(X : R)) :-
  144    regression1(P,A,R).
  145regression1(~P,A,~R) :-
  146    regression1(P,A,R).
  147regression1((P & Q),A,(R & S)) :-
  148    regression1(P,A,R),
  149    regression1(Q,A,S).
  150regression1((P | Q),A,(R | S)) :-
  151    regression1(P,A,R),
  152    regression1(Q,A,S).
  153regression1((P => Q),A,(R => S)) :-
  154    regression1(P,A,R),
  155    regression1(Q,A,S).
  156regression1((P <=> Q),A,(R <=> S)) :-
  157    regression1(P,A,R),
  158    regression1(Q,A,S).
  159
  160% Regression of a knowledge expression.
  161%
  162% Since we're defining obs() in terms of canObs() and canSense(), we
  163% can make the following simplifications:
  164%
  165%    * replace obs()=nil with CanObs
  166%    * avoid quantifying over actions inside knows(), since only A
  167%      can ever match the observations for A
  168%
  169regression1(knows(Agt,P),A,Fr) :-
  170    Fr = ?([O:observation]: (ObsDefn & (~CanObs => knows(Agt,P)) & (CanObs => KR))),
  171    KR = knows(Agt,((Poss & ObsDefn2) => Ppr)),
  172    pcond(P,pbu(Agt),Pp),
  173    regression(Pp,A,Ppr),
  174    adp_fluent(obs(Agt,O),A,ObsDefn),
  175    adp_fluent(obs(Agt,O),A,ObsDefn2),
  176    adp_fluent(canObs(Agt),A,CanObs),
  177    adp_fluent(poss,A,Poss).
  178
  179%  Regression of pknows0 using epistemic path regressor
  180%
  181regression1(pknows0(E,P),A,Fr) :-
  182    regression(P,A2,Pr),
  183    regress_epath(E,A,A2,Er),
  184    Fr = !([A2:action] : pknows0(Er,Pr)).
  185
  186%  Regression of pknows as a fixpoint of pknows0
  187%
  188regression1(pknows(E,P),A,Fr) :-
  189    regression1_pknows_fixpoint(pknows0(E,P),FP),
  190    regression1(FP,A,FPr),
  191    regression1_pknows_rename(FPr,Fr).
  192regression1_pknows_fixpoint(PKn,FP) :-
  193    regression1(PKn,nil,PKn1),
  194    ( domain_tautology(PKn => PKn1) ->
  195        FP = PKn
  196    ;
  197        regression1_pknows_fixpoint(PKn1,FP)
  198    ).
  199regression1_pknows_rename(!(V : PK),!(V : PKr)) :-
  200    regression1_pknows_rename(PK,PKr).
  201regression1_pknows_rename(pknows0(E,P),pknows(E,P)).
  202
  203
  204%  Knowledge fluents need an extra regression step once we reach the
  205%  initial situation.
  206%
  207regression_s0(F,F) :-
  208    is_atom(F).
  209regression_s0(!(X : P),!(X : R)) :-
  210    regression_s0(P,R).
  211regression_s0(?(X : P),?(X : R)) :-
  212    regression_s0(P,R).
  213regression_s0(~P,~R) :-
  214    regression_s0(P,R).
  215regression_s0((P & Q),(R & S)) :-
  216    regression_s0(P,R),
  217    regression_s0(Q,S).
  218regression_s0((P | Q),(R | S)) :-
  219    regression_s0(P,R),
  220    regression_s0(Q,S).
  221regression_s0((P => Q),(R => S)) :-
  222    regression_s0(P,R),
  223    regression_s0(Q,S).
  224regression_s0((P <=> Q),(R <=> S)) :-
  225    regression_s0(P,R),
  226    regression_s0(Q,S).
  227regression_s0(knows(Agt,P),knows(Agt,Pp)) :-
  228    pcond(P,pbu(Agt),Pp).
  229regression_s0(pknows0(E,P),pknows0(E,P)).
  230regression_s0(pknows(E,P),FPr) :-
  231    regression1_pknows_fixpoint(pknows0(E,P),FPr).
  232
  233
  234%  Definition of the epistemic path regressor.
  235%
  236regress_epath(P,C1,C2,POut) :-
  237  regress_epath_a(P,X,Pa),
  238  POut = (!(X:action) ; ?(X=C1) ; Pa ; ?(X=C2)).
  239
  240regress_epath_a(A,X,P) :-
  241    atom(A),
  242    P = (!(Z:observation) ; ?(ObsDefn) ; A ; !(X:action) ; ?(PossDefn & ObsDefn)),
  243    adp_fluent(obs(A,Z),X,ObsDefn1),
  244    adp_fluent(poss,X,PossDefn1),
  245    simplify(ObsDefn1 | ((Z=nil) & (X=nil)),ObsDefn),
  246    simplify(PossDefn1 | (X=nil),PossDefn).
  247regress_epath_a(?(F),X,P) :-
  248    regression(F,X,Fr),
  249    P = ?(Fr).
  250regress_epath_a(!(Y:T),_,!(Y:T)).
  251regress_epath_a(P1 ; P2,X,P1a ; P2a) :-
  252    regress_epath_a(P1,X,P1a),
  253    regress_epath_a(P2,X,P2a).
  254regress_epath_a(P1 | P2,X,P1a | P2a) :-
  255    regress_epath_a(P1,X,P1a),
  256    regress_epath_a(P2,X,P2a).
  257regress_epath_a((P*),X,(Pa*)) :-
  258    regress_epath_a(P,X,Pa).
  259
  260
  261%
  262%  holds(+F,+S) - fluent F holds in situation S
  263%
  264%  This predicate is true whenever the fluent F holds in situation S.
  265%
  266holds(F,do(A,S)) :-
  267    regression(F,A,Fr),
  268    holds(Fr,S).
  269holds(F,s0) :-
  270    regression_s0(F,Fr),
  271    bagof(Ax,initially(Ax),Ax0s),
  272    joinlist('&',Ax0s,Ax0),
  273    domain_tautology(Ax0 => Fr).
  274
  275%
  276%  pcond_d1(F,C,P1)  -  depth 1 persistence condition for fluent F
  277%
  278%    The basic meaning of this pedicate is: if fluent F holds in situation
  279%    s, then it will continue to hold in all C-successors of s as long
  280%    as P1 is true in s.
  281% 
  282pcond_d1(F,C,P1) :-
  283    ( bagof(Cn,pcond_d1_bagof(F,C,Cn),Cns) ->
  284        joinlist('&',Cns,P1t),
  285        simplify(P1t,P1)
  286    ;
  287        P1=true
  288    ).
  289
  290pcond_d1_bagof(F,C,Cnt) :-
  291    action_with_vars(A,Vs),
  292    regression(F,A,R),
  293    adp_fluent(C,A,Ec),
  294    Cnt = !(Vs : (R | ~Ec)).
  295
  296%
  297%  pcond(F,C,P)  -  persistence condition for F under C
  298%
  299pcond(F,C,P) :-
  300    (domain_falsehood(F) ->
  301        P = false
  302    ; domain_tautology(F) ->
  303        P = true
  304    ; 
  305        pcond_acc([F],C,P)
  306    ).
  307
  308pcond_acc([F|Fs],C,P) :-
  309    pcond_d1(F,C,P1),
  310    (domain_falsehood(P1) ->
  311        P = false
  312    ; domain_tautology(P1) ->
  313        joinlist('&',[F|Fs],P)
  314    ; 
  315      joinlist('&',[F|Fs],Ff),
  316      (domain_tautology(Ff=>P1) ->
  317        P = Ff
  318      ;
  319        pcond_acc([P1,F|Fs],C,P)
  320      )
  321    ).
  322
  323
  324%
  325%  enumerate_vars(Vs)  -  bind each variable V in the list to a member
  326%                         of its corresponding type T, backtracking to
  327%                         enumerate all possible values.
  328%
  329enumerate_vars([]).
  330enumerate_vars([V:T|Vs]) :-
  331    call(T,V), enumerate_vars(Vs).
  332
  333
  334%
  335%  guess_var_types(Vs,Fml,VTs)  -  guess the types of each variable in the
  336%                                  list Vs, by looking at how the var is
  337%                                  used in the formula Fml.  Returns a list
  338%                                  of (V:T) pairs.
  339%
  340guess_var_types([],_,[]).
  341guess_var_types([V|Vs],P,[V:T|Ts]) :-
  342    guess_var_type(V,P,T),
  343    guess_var_types(Vs,P,Ts).
  344
  345guess_var_type(V,P,T) :-
  346    (guess_var_type_(V,P,T2) -> T=T2 ; T=object), !.
  347
  348guess_var_type_(V,P,T) :-
  349    is_atom(P), P \= (_=_), P \= (_\=_),
  350    contains_var(P,V:T),
  351    P =.. [F|FArgs], length(FArgs,NumArgs),
  352    length(FTypes,NumArgs), P2 =.. [F|FTypes],
  353    prim_fluent(P2),
  354    guess_var_type_list(V,FArgs,FTypes,T).
  355guess_var_type_(V,P1 & P2,T) :-
  356    guess_var_type_(V,P1,T) ; guess_var_type_(V,P2,T).
  357guess_var_type_(V,P1 | P2,T) :-
  358    guess_var_type_(V,P1,T) ; guess_var_type_(V,P2,T).
  359guess_var_type_(V,P1 => P2,T) :-
  360    guess_var_type_(V,P1,T) ; guess_var_type_(V,P2,T).
  361guess_var_type_(V,P1 <=> P2,T) :-
  362    guess_var_type_(V,P1,T) ; guess_var_type_(V,P2,T).
  363guess_var_type_(V,~P,T) :-
  364    guess_var_type_(V,P,T).
  365guess_var_type_(V,?(_:P),T) :-
  366    guess_var_type_(V,P,T).
  367guess_var_type_(V,!(_:P),T) :-
  368    guess_var_type_(V,P,T).
  369guess_var_type_(V,knows(_,P),T) :-
  370    guess_var_type_(V,P,T).
  371guess_var_type_(V,pknows(_,P),T) :-
  372    guess_var_type_(V,P,T).
  373
  374guess_var_type_list(_,[],[],_) :- fail.
  375guess_var_type_list(V,[Ah|At],[Th|Tt],T) :-
  376    ( V == Ah ->
  377        T = Th
  378    ;
  379        guess_var_type_list(V,At,Tt,T)
  380    )