% This is an alternative ASP encoding of the domain independent % axioms of the Epistemic Functional Event Calculus (EFEC) % See http://www.ucl.ac.uk/infostudies/efec/ % Last update: 16 May 2013 % -- List of domain predicates -- % % fluent(F). % possVal(F, V). % action(A). % % causesValue(A,F,V,T). % possVal(F,v). % -- Domain independent rules -- world(1..maxworld). instant(0..maxinstant). % FEC1 valueCaused(F, V, T) :- happens(A, T), causesValue(A, F, V, T). hasPossCausedValue(F, T) :- valueCaused(F, V, T). % The two rules below are implementing the following: % % 1 { valueChangedTo(F, V, T) : valueCaused(F, V, T) } 1 :- % hasPossCausedValue(F, T). % % Since ASP does not allow non-domain predicate 'possCausedValue' to be used as a % condition inside an aggregation literal (i.e., the head of the rule in this case), % we have to use the domain predicate 'possValue' as the condition and break the axiom % down into two rules. 1 { valueChangedTo(F, V, T) : possVal(F, V) } 1 :- hasPossCausedValue(F, T). :- valueChangedTo(F, V, T), not valueCaused(F, V, T). -valueChangedTo(F, V, T) :- possVal(F, V), time(T), not valueChangedTo(F, V, T). % FEC2 otherValCausedBetween(F, V, T1, T2) :- possVal(F, V), valueChangedTo(F, Vp, T), lessThanEqualTo(T1, T), lessThan(T, T2), V != Vp. -otherValCausedBetween(F, V, T1, T2) :- possVal(F, V), lessThan(T1, T2), not otherValCausedBetween(F, V, T1, T2). % FEC3 valueOf(F, T2, V) :- valueOf(F, T1, V), lessThan(T1, T2), not otherValCausedBetween(F, V, T1, T2). valueOf(F, T2, V) :- valueChangedTo(F, V, T1), lessThan(T1, T2), not otherValCausedBetween(F, V, T1, T2). % FEC4 valueCausedBetween(F, V, T1, T2) :- valueChangedTo(F, V, T), lessThanEqualTo(T1, T), lessThan(T, T2). -valueCausedBetween(F, V, T1, T2) :- lessThan(T1, T2), possVal(F, V), not valueCausedBetween(F, V, T1, T2). -valueOf(F, T2, V) :- possVal(F, V), lessThan(T1, T2), valueChangedTo(F, Vp, T1), Vp != V, not valueCausedBetween(F, V, T1, T2). % FEC5 % ic(fec5) :- valueOf(F, T, V), not possVal(F, V). % EFEC1 time((W, I)) :- world(W), instant(I). % EFEC2 equal((W, I), (W, I)) :- world(W), instant(I). % EFEC3 lessThan((W,I), (W,Ip)) :- world(W), instant(I), instant(Ip), I < Ip. lessThanEqualTo((W,I), (W,Ip)) :- world(W), instant(I), instant(Ip), I <= Ip. % EFEC4 possVal(k(W), true) :- world(W). possVal(k(W), false) :- world(W). % EFEC5 valueOf(k(W), (W, I), true) :- world(W), instant(I). % EFEC6 valueOf(k(W), (Wp, I), true) :- valueOf(k(Wp), (W, I), true). valueOf(k(W), (Wp, I), false) :- valueOf(k(Wp), (W, I), false). % EFEC7 valueOf(k(W3), (W1, I), true) :- valueOf(k(W2), (W1, I), true), valueOf(k(W3), (W2, I), true). % EFEC8 causesValue(sense(F), k(Wp), false, (W, I)) :- valueOf(F, (W,I), V), valueOf(F, (Wp,I), Vp), V != Vp. % EFEC9 epistemic_fluent(k(W)) :- world(W). fluent(EF) :- epistemic_fluent(EF). someWorldValueIs((W, I), F, Ip, V) :- valueOf(k(Wp), (W, I), true), valueOf(F, (Wp, Ip), V), not epistemic_fluent(F). knowsValueIsNot((W, I), F, Ip, V) :- time((W, I)), instant(Ip), possVal(F, V), not epistemic_fluent(F), not someWorldValueIs((W, I), F, Ip, V). -knowsValueIsNot((W, I), F, Ip, V) :- time((W, I)), instant(Ip), possVal(F, V), not epistemic_fluent(F), not knowsValueIsNot((W, I), F, Ip, V). % EFEC10 someOtherValueNotKnownIsNot((W, I), F, Ip, V) :- time((W, I)), instant(Ip), possVal(F, V), not epistemic_fluent(F), possVal(F, Vp), Vp != V, not knowsValueIsNot((W, I), F, Ip, Vp). knowsValueIs((W, I), F, Ip, V) :- time((W, I)), instant(Ip), possVal(F, V), not epistemic_fluent(F), not someOtherValueNotKnownIsNot((W, I), F, Ip, V). -knowsValueIs((W, I), F, Ip, V) :- time((W, I)), instant(Ip), possVal(F, V), not epistemic_fluent(F), not knowsValueIs((W, I), F, Ip, V). % EFEC11 knowsValue(T, F, Ip) :- knowsValueIs(T, F, Ip, V). -knowsValue(T, F, Ip) :- time(T), instant(Ip), possVal(F, V), not epistemic_fluent(F), not knowsValue(T, F, Ip). % EFEC12 someWorldNotHappens((W, I), A, Ip) :- action(A), instant(Ip), valueOf(k(Wp), (W,I), true), not happens(A, (Wp, Ip)). knowsHappens((W, I), A, Ip) :- time((W, I)), action(A), instant(Ip), not someWorldNotHappens((W, I), A, Ip). -knowsHappens(T, A, Ip) :- time(T), action(A), instant(Ip), not knowsHappens(T, A, Ip). % EFEC13 someWorldHappens((W, I), A, Ip) :- valueOf(k(Wp), (W, I), true), happens(A, (Wp, Ip)). knowsNotHappens((W, I), A, Ip) :- time((W, I)), action(A), instant(Ip), not someWorldHappens((W, I), A, Ip). -knowsNotHappens(T, A, Ip) :- time(T), action(A), instant(Ip), not knowsNotHappens(T, A, Ip). % EFEC14 knowsIfHappens(T, A, Ip) :- knowsHappens(T, A, Ip). knowsIfHappens(T, A, Ip) :- knowsNotHappens(T, A, Ip). -knowsIfHappens(T, A, Ip) :- time(T), action(A), instant(Ip), not knowsIfHappens(T, A, Ip). % EFEC15 happens(A, (W, I)) :- perform(A, I), world(W). % EFEC16 happens(A, (W, I)) :- performIfValueKnownIs(A, F, V, I), knowsValueIs((W, I), F, I, V). -happens(A, (W, I)) :- performIfValueKnownIs(A, F, V, I), -knowsValueIs((W, I), F, I, V). % EFEC17 happens(A, T) :- triggered(A, T). % EFEC18 performIfValueKnown(A, I) :- performIfValueKnownIs(A, F, V, I). % ic(efec18) :- happens(A, (W, I)), not performIfValueKnown(A, I), not perform(A, I), not triggered(A, (W, I)). % EFEC19 otherNonEpistemicFluentInitiallyDiffer(W1, W2, F) :- world(W1), world(W2), fluent(F), not epistemic_fluent(F), fluent(Fp), not epistemic_fluent(Fp), Fp != F, valueOf(Fp, (W1, 0), Vp1), valueOf(Fp, (W2, 0), Vp2), Vp1 != Vp2. initiallyDifferAtMostBy(W1, W2, F) :- world(W1), world(W2), fluent(F), not epistemic_fluent(F), not otherNonEpistemicFluentInitiallyDiffer(W1, W2, F). -initiallyDifferAtMostBy(W1, W2, F) :- world(W1), world(W2), fluent(F), not epistemic_fluent(F), not initiallyDifferAtMostBy(W1, W2, F). % EFEC20 someWorldInitiallyDifferAtMostBy(Wa, W, F, V) :- world(Wa), world(W), valueOf(k(Wp), (Wa, 0), true), valueOf(F, (Wp, 0), V), initiallyDifferAtMostBy(W, Wp, F). %ic(efec20) :- world(Wa), possVal(F, V), not epistemic_fluent(F), not knowsValueIsNot((Wa, 0), F, 0, V), valueOf(k(W), (Wa, 0), true), not someWorldInitiallyDifferAtMostBy(Wa, W, F, V). % EFEC21 % EFEC22 % EFEC23 happensBetween(T1, T2) :- lessThan(T1, T), lessThan(T, T2), happens(A, T). next(T, Tnext) :- lessThan(T, Tnext), happens(A, Tnext), not happensBetween(T, Tnext). next((W, I), (W, maxinstant)) :- lessThan((W, I), (W, maxinstant)), not happensBetween((W, I), (W, maxinstant)). % EFEC24 otherNonEpistemicFluentDifferAfter(W1, W2, I, F) :- world(W1), world(W2), instant(I), fluent(F), not epistemic_fluent(F), fluent(Fp), not epistemic_fluent(Fp), Fp != F, next((W1, I), Tnext1), next((W2, I), Tnext2), valueOf(Fp, Tnext1, Vp1), valueOf(Fp, Tnext2, Vp2), Vp1 != Vp2. differAfterAtMostBy(W1, W2, I, F) :- world(W1), world(W2), instant(I), fluent(F), not epistemic_fluent(F), not otherNonEpistemicFluentDifferAfter(W1, W2, I, F). -differAfterAtMostBy(W1, W2, I, F) :- world(W1), world(W2), instant(I), fluent(F), not epistemic_fluent(F), not differAfterAtMostBy(W1, W2, I, F). % EFEC25 someNonEpistemicFluentDifferUpTo(W1, W2, I) :- world(W1), world(W2), instant(I), instant(Ip), Ip <= I, fluent(F), not epistemic_fluent(F), valueOf(F, (W1, Ip), V1), valueOf(F, (W2, Ip), V2), V1 != V2. equalUpTo(W1, W2, I) :- world(W1), world(W2), instant(I), not someNonEpistemicFluentDifferUpTo(W1, W2, I). -equalUpTo(W1, W2, I) :- world(W1), world(W2), instant(I), not equalUpTo(W1, W2, I). % EFEC26 someWorldDifferAfterAtMostBy(Wa, F, V, I) :- world(Wa), next((Wa, I), TaNext), valueOf(k(Wp), TaNext, true), next((Wp, I), TpNext), valueOf(F, TpNext, V), equalUpTo(Wa, Wp, I), differAfterAtMostBy(Wa, Wp, I, F). %ic(efec26) :- world(Wa), valueCaused(F, V, (Wa, I)), not epistemic_fluent(F), next((Wa, I), Tnext), not someWorldDifferAfterAtMostBy(Wa, F, V, I). % AUX1 % initially in any world every non epistemic fluent must have one but % only one value 1 { valueOf(F, (W, 0), V) : possVal(F, V) } 1 :- fluent(F), not epistemic_fluent(F), world(W). % AUX2 % ensures that "knowsValueIsNot((W, 0), F, 0, V) iff initiallyKnowsValueIsNot((W, 0), F, 0, V)". % :- initiallyKnowsValueIsNot((W, 0), F, 0, V), not knowsValueIsNot((W, 0), F, 0, V). :- knowsValueIsNot((W, 0), F, 0, V), not initiallyKnowsValueIsNot((W, 0), F, 0, V). % AUX3 % initially every world is accessible by any world. valueOf(k(W), (Wa, 0), true) :- world(Wa), world(W). % AUX4 % make sure valueOf is a function. %ic(aux4) :- fluent(F), time(T), not 1 { valueOf(F, T, V) : possVal(F, V) } 1. % AUX5 % disallows duplicate worlds. %ic(aux5) :- world(W1), world(W2), W1 != W2, equalUpTo(W1, W2, maxinstant).