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
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
40initially(~knows(Agt,false)) :-
41 agent(Agt).
42
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
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
105
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
137regression1(T1=T2,_,T1=T2).
138regression1(T1\=T2,_,T1\=T2).
139
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
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
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
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
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
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
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
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
329enumerate_vars([]).
330enumerate_vars([V:T|Vs]) :-
331 call(T,V), enumerate_vars(Vs).
332
333
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 )