1%
    2%  Domain-specific definitions.
    3%
    4%  Copyright 2008, Ryan Kelly
    5%
    6%  This axiomatisation is for the "party invitation" domain from the
    7%  paper "Common Knowledge, Hidden Actions, and the Frame Problem", as
    8%  well as Ryan's thesis "Asynchronous Multi-Agent Reasoning in the
    9%  Situation Calculus".
   10%
   11
   12:- discontiguous(causes_true/3).   13:- discontiguous(causes_false/3).   14
   15% Enumerate the values of the various types in the domain
   16agent(ann).
   17agent(bob).
   18
   19location(c).
   20location(d).
   21
   22result(R) :-
   23  location(R).
   24
   25action(nil).
   26action(A) :-
   27    action_with_vars(A,Vs),
   28    enumerate_vars(Vs).
   29
   30observation(nil).
   31observation(A) :-
   32    action_with_vars(A,Vs),
   33    enumerate_vars(Vs).
   34observation(pair(A,R)) :-
   35    A = read(Agt), agent(Agt), location(R).
   36
   37object(O) :-
   38    agent(O) ; location(O) ; result(O) ; observation(O).
   39
   40% Enumerates primitive actions, and the types of their arguments.
   41prim_action(read(agent)).
   42prim_action(leave(agent)).
   43prim_action(enter(agent)).
   44
   45% Enumerates primitive fluents, and types of arguments
   46prim_fluent(loc(location)).
   47prim_fluent(inroom(agent)).
   48
   49% Definitions for action description predicate fluents
   50adp_fluent(poss,read(Agt),inroom(Agt)).
   51adp_fluent(poss,enter(Agt),~inroom(Agt)).
   52adp_fluent(poss,leave(Agt),inroom(Agt)).
   53
   54adp_fluent(canObs(Agt),read(_),inroom(Agt)).
   55adp_fluent(canObs(_),leave(_),true).
   56adp_fluent(canObs(_),enter(_),true).
   57
   58adp_fluent(canSense(Agt),read(Agt2),Agt=Agt2).
   59adp_fluent(canSense(_),leave(_),false).
   60adp_fluent(canSense(_),enter(_),false).
   61
   62adp_fluent(sr(R),read(_),loc(R)).
   63adp_fluent(sr(ok),leave(_),true).
   64adp_fluent(sr(ok),enter(_),true).
   65
   66% Causal rules for each fluent/action combo
   67causes_true(inroom(Agt),enter(Agt2),(Agt=Agt2)).
   68causes_false(inroom(Agt),leave(Agt2),(Agt=Agt2)).
   69
   70%  Specify what holds in the initial situation.
   71initially(loc(c)).
   72initially(~loc(d)).
   73initially(inroom(ann)).
   74initially(inroom(bob)).
   75
   76% Specify what is common knowledge in the initial situation
   77initially(pknows0((ann | bob)*,P)) :-
   78    P = inroom(ann) ; P = inroom(bob)
   79    ; P = (loc(c) <=> ~loc(d))
   80    ; P = ~knows(ann,loc(c)) ; P = ~knows(bob,loc(c))
   81    ; P = ~knows(ann,loc(d)) ; P = ~knows(bob,loc(d)).
   82
   83
   84%
   85%  And now for the unit tests...
   86%
   87
   88:- begin_tests(domain,[sto(rational_trees)]).   89
   90test(reg1) :-
   91    regression(inroom(ann),read(bob),inroom(ann)).
   92test(reg2) :-
   93    regression(inroom(ann),enter(bob),inroom(ann)).
   94test(reg3) :-
   95    regression(inroom(ann),leave(bob),inroom(ann)).
   96test(reg4) :-
   97    regression(inroom(ann),enter(ann),true).
   98test(reg5) :-
   99    regression(inroom(ann),leave(ann),false).
  100
  101
  102test(adp1) :-
  103    adp_fluent(canObs(ann),read(ann),inroom(ann)).
  104test(adp2) :-
  105    adp_fluent(canObs(ann),read(bob),inroom(ann)).
  106
  107test(holds1) :-
  108    holds(inroom(ann),s0), !.
  109test(holds2,fail) :-
  110    holds(~inroom(ann),s0).
  111test(holds3) :-
  112    holds(~inroom(ann),do(leave(ann),s0)), !.
  113test(holds4) :-
  114    holds(inroom(ann),do(leave(bob),s0)), !.
  115test(holds5) :-
  116    holds(?([X:agent] : inroom(X)),do(leave(bob),s0)), !.
  117test(holds6) :-
  118    holds(!([X:agent] : inroom(X)),s0), !.
  119test(holds7) :-
  120    \+ holds(!([X:agent] : inroom(X)),do(leave(bob),s0)).
  121test(holds8) :-
  122    holds(loc(c),s0), !.
  123
  124
  125test(knows1) :-
  126    holds(knows(ann,inroom(ann)),s0), !.
  127test(knows2) :-
  128    holds(knows(ann,inroom(bob)),s0), !.
  129test(knows3) :-
  130    holds(knows(bob,~inroom(ann)),do(leave(ann),s0)), !.
  131test(knows4) :-
  132    holds(~knows(bob,inroom(ann)),do(leave(ann),s0)), !.
  133test(knows5) :-
  134    holds(~knows(bob,loc(c)),s0), !.
  135test(knows6) :-
  136    \+ holds(knows(bob,loc(c)),s0).
  137
  138test(path1) :-
  139    domain_tautology(pknows0(ann | bob,loc(c)) <=> (knows(ann,loc(c)) & knows(bob,loc(c)))).
  140test(path2) :-
  141    domain_tautology(pknows0(!(X:agent) ; ?(inroom(X)),loc(c)) <=> ((inroom(ann) | inroom(bob)) => loc(c))).
  142test(path3) :-
  143    P = pknows0(ann,loc(c)),
  144    regression(P,nil,R),
  145    domain_tautology(R => P), !.
  146%test(path4) :-
  147%    P = pknows0(ann*,loc(c)),
  148%    regression(P,nil,R),
  149%    domain_tautology(R => P), !.
  150
  151test(pknows1) :-
  152    holds(pknows(ann,inroom(ann)),s0), !.
  153test(pknows2) :-
  154    holds(pknows(bob,~inroom(ann)),do(leave(ann),s0)), !.
  155test(pknows3) :-
  156    holds(pknows((ann | bob)*,inroom(ann)),s0), !.
  157
  158%
  159%  Examples from the thesis
  160%
  161test(example1) :-
  162    holds(~ ?([L:location]:knows(ann,loc(L))),s0), !.
  163test(example2) :-
  164    holds(knows(bob,loc(c)),do(read(bob),s0)), !.
  165test(example3) :-
  166    holds(knows(bob,~knows(ann,loc(c))),s0).
  167test(example4) :-
  168    holds(~ knows(bob,~ knows(ann,loc(c))),do(leave(bob),s0)), !.
  169
  170%test(example5) :-
  171%    holds(pknows((ann | bob)*,~knows(ann,loc(c))),s0), !.
  172%test(example6) :-
  173%    holds(~pknows((ann | bob)*,loc(c)),do(read(bob),s0)), !.
  174%test(example7) :-
  175%    holds(pknows((ann | bob)*,?([X:location] : knows(bob,loc(X)))),do(read(bob),s0)), !.
  176%test(example8) :-
  177%    holds(pknows((ann | bob)*,loc(c)),do(read(ann),do(read(bob),s0))), !.
  178
  179:- end_tests(domain).