EC Additive Effects Independently
From TAMI
Title: Description of Cumulative Effects with Aggregates in the Event Calculus
Authors: Ankesh Khandelwal
Note: The main proposal here has been submitted to KR 2012 for peer-review.[1]
Abstract
This paper describes an aggregates-based mechanism for handling cumulative effects on real-valued parameters in logic-based approaches to reasoning about action. Specifically, we extend the Event Calculus formalism which can reason about continuously varying parameters and their derivatives. Individual effects, described independently, are summed implicitly (rather than explicitly) to compute the cumulative effect. Domain descriptions can be more general, concise, and elaboration tolerant using this mechanism than it is currently possible.
Introduction
This page will be updated.
Continuously varying parameters are time-varying properties like fluents but, unlike fluents, they are arbitrarily-valued functions of time.[2] Discussion in this paper is relevant only to real-valued functions of time and hence parameters are restricted to those functions.
Cumulative effects on parameters are described by explicitly adding component effects in current logic-based formalisms to reason about action, including Event Calculus, which results in domain descriptions becoming very specific and less elaboration tolerant than they can actually be. Consider for example, a scenario where arbitrary and not-fixed pipes are supposed to fill up some tanks.
Following axiom, not in any specific logical formalism,
(T1') HoldsAt(Tap-on(n), t) → Value(Contribution(n), t) = Rate(n),
where n and t are variables, states that if n is an identifier for a pipe and tap of pipe n is on at any time t, then n fills some tank at the rate at which water is released from pipe n at time t. If the tap is off, it contributes no flow which can be stated by,
(T2') ¬HoldsAt(Tap-on(n), t) → Value(Contribution(n), t) = 0.
Now if the number of pipes contributing to any tank was fixed to 2, following axiom would be sufficient to describe the rate at which any tank will be filled,
(T3') HoldsAt(connects(n1, v), t) ∧ HoldsAt(connects(n2, v), t) ∧ n1 ≠ n2 → Value(Filling(v), t) = Value(Contribution(n1), t) + Value(Contribution(n2), t),
where v is an identifier for a tank and fluent connects(n1, v) holds if pipe n1 is connected to v. However, if the number of pipes ranges between N and M, N < M, then M-N additional axioms of the form,
(T4') HoldsAt(connects(n1, v), t) ∧ ¬∃n2(HoldsAt(connects(n2, v), t) ∧ n1 ≠ n2) → Value(Filling(v), t) = Value(Contribution(n1), t),
are required. Latter axiom checks that no second pipe is connected to tank v, when at-least one but at-most two pipes can contribute to any tank. Note that such a description is scenario-specific and is dependent on the upper bound M.
Next, if the tanks can have one or more water outlets, then the domain axioms describing rate at which any tank v is filling, Value(Filling(v), t), will have to be changed to accommodate contribution of those outlets. Assuming every tank is connected to by exactly two pipes at any time and has one fixed outlet, then (T3') will be replaced by
(T5') HoldsAt(connects(n1, v), t) ∧ HoldsAt(connects(n2, v), t) ∧ n1 ≠ n2 ∧ HoldsAt(Outlet(o1, v), t) → Value(Filling(v), t) = Value(Contribution(n1), t) + Value(Contribution(n2), t) + Value(Contribution-outlet(o1), t),
where contribution of outlet would be zero or non-zero depending on whether its open or not.
A formalism is elaboration tolerant to the extent that it is convenient to modify a set of facts expressed in the formalism to take into account new phenomena or changed circumstances [mccarthy1999]. The simplest kind of elaboration is the addition of new formulas, known as additive elaborations. The last example shows that elaboration with new cumulative effect is not additive (T3' had to be replaced by T5'), even though it may be considered elaboration tolerant.
Additive elaboration (with regards to cumulative effects) seems possible except that its limited by the explicit addition of individual effects. We extend the Event Calculus formalism with aggregates such that only individual effects need be specified and summation is taken care of by underlying semantics of the formalism. We show in Section 2 how axioms described above can be rewritten in the new formalism. The resulting set of axioms are general enough and not limited by values M and N, as above, they are more concise than axioms listed above and elaborations with new cumulative effects are additive.
There are few formalisms for Reasoning about Action which consider continuous change. Miller and Shanahan extended the Event Calculus formalism to reason about continuously varying parameters and its derivatives [miller1996a]. Continuous change can be described using arbitrary systems of differential equations, and their formalism can handle domain constraints, concurrent actions and actions with non-deterministic effects [miller1996a]. Authors also compare their approach with previous works for reasoning about continuously varying parameters, such as [sandewall1989a] and [miller1996b], in [miller1996a]. Furthermore, there are few works that deal with concurrent cumulative effects in Qualitative Reasoning domain, e.g. [belleghem1994], but their approach is very different and does not exploit aggregates for example.
In the sequel, we will be referring to the Event Calculus (EC) formalism proposed in [miller1996a] which will be introduced in the Section 3.
First Order Logic with Aggregates
[lifschitz2008] provides a nice overview of semantics of First Order Logic (FOL). A signature of FOL formula consists of object constants, function constants, propositional constants, and predicate constants. Formulas are constructed using quantifiers ∀ and ∃, and connectives ∧, ∨, ¬ and →.
An interpretation of first order logic (FOL) assigns a denotation to all non-logical constants in that language. Interpretation (or structure) of a signature σ consists of
- a nonempty set |I|, called the universe (or domain) of I,
- for every object constant c of σ, an element cI of |I|,
- for every function constant f of σ of arity n > 0, a function fI from |I|n to |I|,
- for every propositional constant P of σ, an element PI of {FALSE, TRUE},
- for every predicate constant R of σ of arity n > 0, a function RI from |I|n to {FALSE, TRUE}. Alternatively, every predicate symbol R of arity n can be assigned a relation RI over |I|n.
Also, γI can be alternatively represented by I(γ), where γ is a term, formula or sentence.
Signature σI denotes the signature obtained from σ by adding all names ξ* - new symbols for every element ξ of universe |I| - as object constants. The interpretation I is extended to the new signature σI by defining (ξ*)I = ξ for all ξ ∈ |I|.
The semantics of FOL defines, for any sentence F and any interpretation I of a signature σ, the truth value FI that is assigned to F by I.
- tI for any term t of the extended signature that does not contain variables is defined recursively as follows.
- If t is an object constant then tI is part of the interpretation I.
- f(t1, ..., tn)I = fI(t1I, ..., tnI), for all function constants f of arity n > 0.
- FI for any sentence F of the extended signature is defined recursively as follows.
- For any propositional constant PI is part of the interpretation I.
- R(t1, ..., tn)I = RI(t1I, ..., tnI), for all predicate constants R of arity n > 0.
- ⊥I = FALSE, ΤI = TRUE,
- (F ⊙ G)I = ⊙(FI, GI) for every binary connective ⊙, where ⊙(a, b) is evaluation of truth value according to the truth table.
- ∀w F(w)I = TRUE if F(ξ*)Ifor all ξ ∈ |I|, f) ∃w F(w)I = TRUE if F(ξ*)Ifor some ξ ∈ |I|.
- For FO with equality, (t1 = t2)I = TRUE if t1I = t2I.
An interpretation I satisfies a sentence F, or is a model of F, written as I ⊨ F, if FI = TRUE. A sentence F is logically valid if every interpretation satisfies F.
Circumscription
Circumscription is a transformation of predicate formulas proposed by John McCarthy [mccarthy1987] for the purpose of formalizing non-monotonic aspects of a theory. Under circumscription extensions of certain predicates are minimized. Extension of a predicate refers to the tuples that belong to a predicate. Minimization of extensions of some predicates may be given preference over others and it is referred to as prioritized circumscription. When no preference is given, it is referred to as parallel circumscription. Latter is denoted by CIRC[F ; P ; Z ] and former by CIRC[F ; P1 > ... > Pk ; Z ], where F is a FOL formula and P and Pi are tuples of predicates occurring in F such that Pi and Pj, i≠j, are disjoint and their extensions are minimized respectively. Extensions of constants in Z are allowed to vary, but extensions of the rest of the constants are fixed.
If P and Q are n-ary predicates, then P ≤ Q iff extension of P is a subset of the extension of Q, i.e.∀x(P(x) → Q(x)) is true. This can be extended to tuples P = P1, ..., Pm and Q = Q1, ..., Qm of predicates. P ≤ Q iff P1 ≤ Q1 ∧ ... ∧ Pm ≤ Qm. P < Q iff P ≤ Q ∧ ¬(Q < P).
Let P and Q are partitioned into {P1, ..., Pk} and {Q1, ..., Qk}. Then P ≼ Q stands for
- ∧i=1 to k (∧j=1 to i-1(Pj = Qj) ⊃ (Pi ≤ Qi))
P ≺ Q iff (P ≼ Q) ∧ ¬(P ≼ Q).
Then circumscription formulas are second order formulas [lifschitz1994], defined by
CIRC[F ; P ; Z] ≡ F(P, Z) ∧ ¬∃p, z(F(p, z) ∧ p < P)
CIRC[F ; P1 > ... > Pk ; Z] ≡ F(P, Z) ∧ ¬∃p, z(F(p, z) ∧ p ≺ P)
UNA Notation
UNA[f1, ..., fn], where f1, ..., fn are (possibly 0-ary) functions, expresses that f1, ..., fn are injections with disjoint ranges [baker1991] and stands for the axioms:
- fi(x1, ..., xk) ≠ fj(y1, ..., yl)
for i < j where fi has arity k and fj has arity l, and:
fi(x1, ..., xk) = fi(y1, ..., yk) → (x1 = y1 ∧ ... ∧ x2 = y2)
for fi of arity k > 0.
Aggregates
We use interpretation for aggregates from [ferraris2010, bartholomew2011]. [ferraris2010] works with a more general syntax for aggregates than [bartholomew2011], however, we restrict to the latter syntax.
An aggregate function is a partial function from the class of multisets to Num, where Num is Z ∪ {+∞, -∞} and Z is the set of integers. A multiset is defined as a set along with a function assigning a positive integer (and +∞), called the multiplicity, to each of its elements. The aggregate function #sum, for example, maps multiset α to the sum of all non-zero integers from α if there are finitely many of them (otherwise, the sum may be +∞, -∞ or undefined).
If OP is an aggregate function, then OP⟨x.F(x)⟩ is an aggregate expression, where construct x.F(x) is a quantifier binding the members of x. If E is an aggregate expression, t is any term, ≽ is a comparison operator, and f is a function constant, then E ≽ t and f(t) = E, for some t, are aggregate formulas. Aggregate formulas of latter form, intended for use as assignments of aggregate values as function values, are not explicitly stated in [ferraris2010, bartholomew2011].
For any set X of n-tuples (n ≥ 1), msp(X), the multiset projection of X, is the multiset consisting of all ξ1 such that (ξ1, ξ2, ..., ξn) ∈ X for at least one (n-1)-tuple (ξ2, ..., ξn), with the multiplicity equal to the number of such (n-1)-tuples, possibly +∞.
An interpretation I of FOL with aggregates, for signature σI, is defined as:
- (x1...xnF(x1, ..., xn))I is msp({(ξ1, ..., ξn) ∈ |I|n : F(ξ*1, ..., ξ*n)I = TRUE});
- (OP⟨x.F(x)⟩)I = OP((x.F(x))I).
- (OP⟨x.F(x)⟩ ≽ t)I is ≽OP((⟨x.F(x)⟩)I, tI), where comparison operator ≽ is interpreted as itself.
It's expected that Num is a subset of |I| and the comparison operator is interpreted as itself.
Therefore, (#sum⟨x.F(x)⟩)I equals sum of elements in the multiset (x.F(x))I.
Example I: Water Tanks Problem
The Water Tanks Problem discussed in the introduction is more general form of the The Water Tank Example and Many Tanks Problem in [miller1996a] and [shanahan1990], respectively. We'll rewrite the domain axioms (T1') to (T5') using a new predicate symbol Part-value. Part-value is used to collect the individual effects on any parameter.
(T1) HoldsAt(connects(n, v), t) ∧ HoldsAt(Tap-on(n), t) → Part-value(Filling(v), t, ..., Rate(n))
(T2) HoldsAt(connects(n, v), t) ∧ ¬HoldsAt(Tap-on(n), t) → Part-value(Filling(v), t, ..., 0)
(T3) HoldsAt(Outlet(o, v), t) ∧ HoldsAt(Open(o), t) → Part-value(Filling(v), t, ..., -1 × Rate(o))
Value(Filling(v), t) is implicitly computed as:
(T4) Value(Filling(v), t) = #sum⟨w.Part-value(Filling(v), t, ..., w)⟩
Observe that axioms (T1) to (T3) can be used independent of number of pipes connected to a tank or number of outlets from tank v at any time. (T2) need not be explicitly stated (footnote: counterpart of T3 is hence, not stated above). Furthermore, new cumulative effects can be added to the formulas above. For example, effect of evaporation can be added as,
(T5) Part-value(Filling(v), t, ..., -1 × Evaporation-rate(v)).
We have not specified certain arguments of the predicate Part-value(Filling(v), t, ..., w). Consider a scenario for that, where pipes P1 and P2 are connected to tank V, and both the pipes are turned on for some time t. Then predicates Part-value(Filling(V), t, ..., Rate(P1)) and Part-value(Filling(V), t, ..., Rate(P2)) hold, and we would expect that Value(Filling(V), t) = Rate(P1) + Rate(P2) holds as well. However, if Rate(P1) = Rate(P2) = R, then Value(Filling(v), t) would be computed to be equal to R, instead of 2×R, by the semantics of aggregate operation #sum, unless there are other arguments that differentiate the two predicates independent of values of Rate(P1) and Rate(P2).
One possible solution is to have n and o as additional arguments of Part-value. Then, for example, (T1) and (T4) will be of the forms,
HoldsAt(connects(n, v), t) ∧ HoldsAt(Tap-on(n), t) → Part-value(Filling(v), t, n, Rate(n)),
Value(Filling(v), t) = #sum⟨w, z.Part-value(Filling(v), t, z, w)⟩.
This way Value(Filling(v), t) would be computed as 2×R, even when two rates are the same.
DCAs
The additional arguments are referred to as Arguments for Disambiguating Contributions (DCAs). While the DCAs help in disambiguating numerically similar contributions, they must be carefully chosen to avoid counting same contribution from same source but derived from different formulas, twice.
Event Calculus Extended with Aggregates for Cumulative Effects
We recap relevant EC concepts and axioms from [miller1996a] before describing the extension.
| Name of Sort | Symbol | Variables |
|---|---|---|
| Actions | A | a, a1, a2, ... |
| Fluents | F | f, f1, f2, ... |
| Times | T | t, t1, t2, ... |
| Parameters | P | p, p1, p2, ... |
| Reals | R | r, r1, r2, ..., s |
| Domain objects | X | x, x1, x2, ... |
EC is written in sorted predicate calculus, with sorts summarized in the Table 1. T is interpreted as non-negative numbers. Following function symbols, Value : P × T ↦ R, δ : P ↦ P, and Next : T ↦ T, are used. Value(δ(P), T) represents the numerical value of first derivative of parameter P at time T. Next(T) refers to the least time point after T at which an action occurs, if there is such a time point.
Following predicate symbols are used: Happens, HoldsAt, Initiates, Terminates, Releases, InitiallyTrue, InitiallyFalse, LeftContinuous, Continuous, Differentiable, RightLimit, BreaksTo, and Breaks.
The sorting of the predicate symbols in the language can be understood from their arguments in the axioms below. Also, all variables are assumed to be universally quantified with maximum scope unless otherwise stated in the axioms below.
Last six predicates were introduced for reasoning with continuously varying parameters. LeftContinuous(P, T), Continuous(P, T) and Differentiable(P, T) expresses that at time T, the function associated with parameter P is left-hand continuous, continuous, and differentiable respectively. RightLimit(P, T, R) expresses that at time T, the right limit value of function associated with parameter P is R. BreaksTo(A, P, T, R) expresses that at time T, an occurrence of action A will cause parameter P to instantaneously take on value R. Breaks(A, P, T) expresses that at time T, action A potentially causes discontinuity in parameter P.
Mathematical definitions of Continuous, Differentiable, LeftContinuous and RightLimit are axiomatised in (A1)--(A4).
(A1) Continuous(p, t) ≡ ∀r∃t1∀t2[[|t - t2| < t1 ∧ 0 < r] → |Value(p, t) - Value(p, t2)| < r]
(A2) Differentiable(p, t) ≡ ∀r∃t1∀t2[[0 < |t - t2| < t1 ∧ 0 < r] → |(Value(p, t) - Value(p, t2))/(t - t2) - Value(δ(p), t)| < r]
(A3) LeftContinuous(p, t) ≡ ∀r∃t1∀t2[[t2 < t ∧ (t - t2) < t1 ∧ 0 < r] → |Value(p, t) - Value(p, t2)| < r]
(A4) RightLimit(p, t, r) ≡ ∀r1∃t1∀t2[[t < t2 ∧ (t2 - t) < t1 ∧ 0 < r1] → |Value(p, t2) - r| < r1]
Fluents are persistent by default and parameters are continuous by default. Break in the persistence for fluents is described using Initiates or Terminates (or Releases) predicates, whereas change in continuity for parameters is described using BreaksTo and Breaks predicates.
Axioms (EC1) -- (EC4) express the persistence of fluents and effects of Initiates and Terminates, when corresponding actions happen. Axioms (EC8) -- (EC9) express that functions associated with parameters are continuous and differentiable by default.
(EC1) HoldsAt(f, t) ← [InitialisedTrue(f) ∧ ¬Clipped(0, f, t)]
(EC2) ¬HoldsAt(f, t) ← [InitialisedFalse(f) ∧ ¬Declipped(0, f, t)]
(EC3) HoldsAt(f, t2) ← [Happens(a, t1) ∧ Initiates(a, f, t1) ∧ t1 < t2 ∧ ¬Clipped(t1, f, t2)]
(EC4) ¬HoldsAt(f, t2) ← [Happens(a, t1) ∧ Terminates(a, f, t1) ∧ t1 < t2 ∧ ¬Declipped(t1, f, t2)]
(EC5) Clipped(t1, f, t2) ≡def ∃a, t[Happens(a, t) ∧ t1≤t<t2 ∧ [Terminates(a, f, t) ∨ Releases(a, f, t)]]
(EC6) Declipped(t1, f, t2) ≡def ∃a, t[Happens(a, t) ∧ t1≤t<t2 ∧ [Initiates(a, f, t) ∨ Releases(a, f, t)]]
Axiom (EC7) expresses that functions associated with parameters are left-hand continuous at every time-point, including those at which actions occur. In other words, if an action causes a discontinuity it takes effect immediately after the action occurs. Definition of BreaksTo is axiomatized in Axiom (EC10).
(EC7) LeftContinuous(p, t)
(EC8) ¬[Happens(a, t) ∧ Breaks(a, p, t)] → Continuous(p, t)
(EC9) ¬[Happens(a, t) ∧ Breaks(a, δ(p), t)] → Differentiable(p, t)
(EC10) [BreaksTo(a, p, t, r) ∧ Happens(a, t)] → RightLimit(p, t, r)
Axiom (EC11) states the relationship between BreaksTo and Breaks, and Axiom (EC12) states that an action that potentially causes discontinuity in a given parameter also potentially causes discontinuity in its higher derivatives.
(EC11) BreaksTo(a, p, t, r) → Breaks(a, p, t)
(EC12) Breaks(a, p, t) → Breaks(a, δ(p), t)
(EC13)--(EC15) axiomatize the definition of Next(T).
(EC13) t < Next(t)
(EC14) [t < t1 ∧ t1 < Next(t)] → ¬Happens(a, t1)
(EC15) [Happens(a1, t1) ∧ t < t1] → ∃a.Happens(a, Next(t))
The extension
In addition to predicate corresponding to Part-value which was hinted to in Section 2, we also need a predicate for specifying partial discontinuous changes. For example,
(T6) BreaksTo(Scoop(s), Level, t, Value(Level, t) - A) ← Value(Level, t) ≥ A
(T7) BreaksTo(Scoop(s), Level, t, 0) ← Value(Level, t) < A
states that the action of scooping water from the tank instantaneously decreases the level by amount S unless it becomes less than zero. (T6) can be restated to handle effects of multiple concurrent actions of scooping as
(T8) BreaksPartBy(Scoop(s), Level, t, -1 × A) ← Value(Level, t) ≥ A
to express that any unique scoop action reduces the level by amount A. Please note that more than Value(Level, t)/A simultaneous scoops will have an inconsistent outcome and must be disallowed, but is not enforced above. The effects are independent when the number of scoops are less than that value, not otherwise.
The component effects (values) of a cumulative effect (value) are said to be independent if they can be described individually with respective preconditions, and the net effect can be obtained by summing them.
We introduce predicates BreaksPartBy, PartValue, and PartValue", for expressing independent effects and values that are implicitly aggregated every time. BreaksPartBy(A, P, T, R) expresses that if action A occurs at time T, then it discontinuously changes value of parameter P by R. Axiom (EC16p) axiomatizes the definition of BreaksPartBy.[3] Axiom (EC17p), similar to (EC11), states the relationship between BreaksPartBy and Breaks.
(EC16p) ∃a, r.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t)) ∧
s = Value(p, t) + #sum⟨r, a.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))⟩ → RightLimit(p, t, s)
(EC17p) BreaksPartBy(a, p, t, r) → Breaks(a, p, t)
PartValue(P, T, P1, ..., PN, R), N ≥ 0, expresses that R is one of the component values for final values of P, uniquely identified by P1, ..., PN. P1, ..., PN are the DCAs (defined in Section 2). In this work, we assume that DCAs are from the sort P, i.e. they are parameters. In the water tank example N=1 was sufficient, however, that may not always be the case. For example, force applied on a block by a spring connected to it is a function of both the spring constant and displacement of the spring from its equilibrium position.
Note that predicate PartValue is overloaded. Also, as per definition of aggregate expressions, we can not take aggregate of arguments of predicates of different arities in one aggregate expression. Therefore predicate PartValue" is used. PartValue"(P, T, N, R) expresses that R is the sum of all component values, of the final value of P, that are uniquely identified by N DCAs. Axiom (EC19p) axiomatizes the definition of PartValue with help of Axiom (EC18p) that axiomatizes definition of PartValue". Note that (EC18p) is presented in its general form and may be stated separately for every n ≥ 0. [4]
(EC18p) PartValue"(p, t, n, s) ↔ ∃r, p1, ..., pn. PartValue(p, t, p1, ..., pn, r)
∧ s=#sum⟨r, p1, ..., pn. PartValue(p, t, p1, ..., pn, r)⟩
(EC19p) ∃r, n. PartValue"(p, t, n, r) ∧ s=#sum⟨r, n. PartValue"(p, t, n, r)⟩ → Value(p, t) = s.
Value(p; t) must be specified explicitly for all those times when no component values are known for the given parameter p. [5]
Example II: Multiple Blocks Problem
With implicit summation to get the cumulative effect or value, it may be possible that many different scenarios can be modeled via same set of domain axioms. We illustrate one case of that, involving multiple blocks problem in 2D. Multiple blocks are stacked over one other, none of which are on two different blocks and none of them touch sideway. One block may have any number of blocks on it. Coefficient of friction between any two surfaces is given. Axioms (B1), (B2) list some of the afore-mentioned assumptions. Forces may be applied on blocks or blocks with non-zero initial velocities may be placed on top of other blocks. We restrict our goal to finding forces of frictions and accelerations of blocks immediately after any action. Furthermore, horizontal motion is over-ruled. Relationship between (horizontal) velocity and acceleration is described in Axiom (B3). Domain axioms defined below may be extended to account for other things such as movement along the blocks resulting in blocks falling off the edges etc.
(B1) ¬HoldsAt(HorizontalContact(a, b), t)
(B2) HoldsAt(On(a, b), t) ∧ HoldsAt(On(a, c), t) → a = c
(B3) Value(δ(Vel(b)), t) = Value(Acc(b), t)
Following actions are considered, ApplyHorizontalForce(F, B, V) (or AHF(F, B, A)), ApplyVerticalForce(F, B, V) (or AVF(F, B, V)), RemoveHorizontalForce(F, B, V) (or RHF(F, B, V)) and RemoveVerticalForce(F, B, V) (or RVF(F, B, V)) and PlaceOn(B1, B2, V), where F is identifier for force, B refers to blocks, Bi refers to a block or Ground, and V is the value of force or velocity. Act PlaceOn(B1, B2, V) places block B1 having velocity V on B2. Ground is treated as a special block with fixed zero velocity and acceleration and infinite weight (Axiom (B4)). Axiom (B5) expresses effects of actions on fluents (AppliedHorizontalForce(f, b, v) or AHF(f, b, v), AppliedVerticalForce(f, b, v) or AVF(f, b, v)), where as Axiom (B6) expresses that velocity of block b1 is v when it is placed on b2.
(B4) Value(Acc(Ground), t) = Value(Vel(Ground), t) = 0 ∧ Value(Wt(Ground), t) = +∞
(B5) Initiates(ApplyHF(f, b, v), AHF(f, b, v), t) ∧ Initiates(ApplyVF(f, b, v), AVF(f, b, v), t)
∧ Terminates(RemoveHF(f, b, v), AHF(f, b, v), t) ∧ Terminates(RemoveVF(f, b, v), AVF(f, b, v), t)
∧ Initiates(PlaceOn(b1, b2, v), On(b1, b2), t)
(B6) BreaksTo(PlaceOn(b1, b2, v), Vel(b1), t, v)
IndirectlyOn(b1, b2) (or IndOn(b1, b2)), Connected(b1, b2) (or Conn(b1, b2)), PotMobile(b), SlidingRight(b1, b2) (or SR(b1, b2)) and SlidingLeft(b1, b2) (or SL(b1, b2)) are secondary fluents. Secondary fluents are fluents that are not directly affected by any actions and have no default persistence (Axiom (B7)).
(B7) ReleasedAt(IndOn(b1, b2), t) ∧ ReleasedAt(Conn(b1, b2), t) ∧ ReleasedAt(PotMobile(b), t)
∧ ReleasedAt(SR(a, b), t) ∧ ReleasedAt(SL(a, b), t)
Block b1 is indirectly on b2 if it is transitively on b2 (Axiom (B8)). Observe that constraint in Axiom (B10) holds. Further, block b1 is connected to b2 if they are either transitively on each other or transitively on same block (Axiom (B9)).
(B8) HoldsAt(IndOn(b1, b3), t) ↔ HoldsAt(On(b1, b3), t) ∨ HoldsAt(On(b1, b2), t) ∧ HoldsAt(IndOn(b2, b3), t))
(B9) HoldsAt(On(b1, b2), t) → b1 ≠ b2 ∧ ¬HoldsAt(IndOn(b2, b1), t)
(B10) HoldsAt(Conn(b1, b2), t) ↔ b1 ≠ Ground ∧ b2 ≠ Ground
∧ ((HoldsAt(IndOn(b1, b3), t) ∧ HoldsAt(IndOn(b2, b3), t) ∧ b3 &neq; Ground)
∨ HoldsAt(IndOn(b1, b2), t) ∨ HoldsAt(IndOn(b2, b1), t)) [6]
Unlike Axioms (B8) and (B10) which define necessary and sufficient conditions, axioms (B11) -- (B13) describe necessary conditions, involving different velocities, for block b1 to be sliding right and left respectively, over b2. CKF(b1, b2) and CSF(b1, b2) are the coeffecients of kinetic and static friction between surfaces and Friction(b1, b2) (or Fr(b1, b2)) is the friction force on b1 by b2. ForceByBlockAbove(b1, b2) (or FbBA(b1, b2)) is the force applied on b1 by b2 from above. The positive horizontal and vertical directions are to the right and upwards, respectively.
(B11) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) = Value(Vel(b2), t) ∧ HoldsAt(SR(b1, b2), t)
→ Value(Fr(b1, b2), t) = -1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t)
∧ Value(Acc(b1), t) - Value(Acc(b2), t) > 0 ∧ ¬HoldsAt(SL(b1, b2), t)
(B12) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) = Value(Velocity(b2), t) ∧ HoldsAt(SL(b1, b2), t)
→ Value(Fr(b1, b2), t) = +1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t)
∧ Value(Acc(b1), t) - Value(Acc(b2), t) < 0 ∧ ¬HoldsAt(SR(b1, b2), t)
(B13) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) = Value(Vel(b2), t) ∧ ¬HoldsAt(SR(b1, b2), t)
∧ ¬HoldsAt(SL(b1, b2), t) → Value(Acc(b1), t) = Value(Acc(b2), t)
∧ |Value(Fr(b1, b2), t)| ≤ Value(CSF(b1, b2), t) × Value(FbBA(b2, b1), t)
For each of the three cases, sliding left, right, or not, we get an equation, e.g. Value(Fr(b1, b2), t) = -1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t) and Value(Acc(b1), t) = Value(Acc(b2), t), and a constraint, e.g. Value(Acc(b1), t) - Value(Acc(b2), t) > 0 and |Value(Fr(b1, b2), t)| ≤ Value(CSF(b1, b2), t) × Value(FbBA(b2, b1), t). |V| denotes the absolute value of V.
(B14)--(B15) express friction values and directions when velocities of blocks in contact are unequal.
(B14) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) > Value(Vel(b2), t)
→ Value(Fr(b1, b2), t) = -1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t)
(B15) HoldsAt(On(b1, b2), t) ∧ Value(Vel(b1), t) < Value(Vel(b2), t)
→ Value(Fr(b1, b2), t) = +1 × Value(CKF(b1, b2), t) × Value(FbBA(b2, b1), t)
Axiom (B16) states that blocks apply equal and opposite friction forces on each other, and (B17) follows from the Newton's Second Law of Motion.
(B16) HoldsAt(On(b1, b2), t) → Value(Fr(b1, b2), t) = -1 × Value(Fr(b2, b1), t)
(B17) Value(Acc(b)) = Value(NHF(b), t) / Value(mass(b), t)
Axioms (B18) -- (B24) describe component values for parameters NetAppliedHorizontalForce(b) (or NAHF(b)), NetAppliedVerticalForce(b) (or NAVF(b)), ForceByBlockAbove(b1, b2) (or FbBA(b1, b2)), and NetHorizontalForce(b) (or NHF(b)). Axioms (B18) and (B19) express that the individual forces on a block can be added to get the net force in each direction. Axioms (B20) and (B21) express that if no force is applied then the net applied force is 0. DCAs are implicit here, they are discussed in following subsection.
(B18) HoldsAt(AHF(f, b, v), t) → PartValue(NAHF(b), t, ..., v)
(B19) HoldsAt(AVF(f, b, v), t) → PartValue(NAVF(b), t, ..., v)
(B20) ¬∃ n, v. PartValue"(NAHF(b), t, n, v) → Value(NAHF(b), t) = 0
(B21) ¬∃ n, v. PartValue"(NAVF(b), t, n, v) → Value(NAVF(b), t) = 0
Axioms (B22) and (B23) express that weight of, and vertical force on, block b2 and any block transitively on b2 contribute to the Force applied by block b2 on b1.
(B22) HoldsAt(On(b2, b1), t) → PartValue(FbBA(b1, b2), t, ..., Value(Wt(b2))) ∧ PartValue(FbBA(b1, b2), t, ..., Value(NAVF(b2)))
(B23) HoldsAt(IndOn(b3, b2), t) ∧ HoldsAt(On(b2, b1), t)
→ PartValue(FbBA(b1, b2), t, ..., Value(Wt(b3))) ∧ PartValue(FbBA(b1, b2), t, ..., Value(NAVF(b3)))
Axiom (B24) expresses that a block can move if it is connected to some block that has non-zero velocity or non-zero net applied force.
(B24) HoldsAt(PotMobile(b1), t) ↔ (Value(Vel(b), t) ≠ 0 ∨ Value(NAHF(b), t) ≠ 0) ∧ HoldsAt(Conn(b, b1), t)
Axiom (B25) incorporates value of net applied horizontal forces in value of the net horizontal force. If a block can potentially be mobile and is on top of another body then friction forces will come into play and would contribute to the net horizontal force (Axiom (B26)). Axiom (B27) expresses that if no applied horizontal force or friction force is active, then the net horizontal force on the block is 0.
(B25) PartValue(NHF(b), t, ..., Value(NAHF(b)))
(B26) HoldsAt(On(b1, b2), t) ∧ HoldsAt(PotMobile(b1), t)
→ PartValue(NHF(b1), t, ..., Value(Fr(b1, b2), t)) ∧ PartValue(NHF(b2), t, ..., Value(Fr(b2, b1), t))
(B27) ¬∃ n, v. PartValue"(NHF(b), t, n, v) → Value(NHF(b), t) = 0
Axioms (B28) -- (B34) express discontinuities, in parameters, caused by actions.
(B28) (a = ApplyHF(f, b, v) ∨ a = RemoveHF(f, b, v)) ∧ p = NAHF(b) → Breaks(a, p, t)
(B29) (a = ApplyVF(f, b, v) ∨ a = RemoveVF(f, b, v)) ∧ p = NAVF(b) → Breaks(a, p, t)
(B30) (a = ApplyVF(f, b1, v) ∨ a = RemoveVF(f, b1, v)) ∧ HoldsAt(IndOn(b1, b2), t) ∧ p = FbBA(b3, b2) → Breaks(a, p, t)
(B31) (a = ApplyHF(f, b1, v) ∨ a = RemoveHF(f, b1, v)) ∧ HoldsAt(Conn(b1, b2), t)
∧ (p = NHF(b2) ∨ p = Vel(b2) ∨ p = Acc(b2)) → Breaks(a, p, t)
(B32) (a = ApplyVF(f, b1, v) ∨ a = RemoveVF(f, b1, v)) ∧ HoldsAt(PotMobile(b1), t) ∧ HoldsAt(Conn(b1, b2), t)
∧ (p = NHF(b2) ∨ p = Vel(b2) ∨ p = Acc(b2)) → Breaks(a, p, t)
(B33) a = PlaceOn(b3, b1, v) ∧ HoldsAt(Conn(b1, b2), t) ∧ (p = NHF(b2) ∨ p = Vel(b2) ∨ p = Acc(b2)) → Breaks(a, p, t)
(B34) [(a = ApplyHF(f, b1, v) ∨ a = RemoveHF(f, b1, v))
∨ ((a = ApplyVF(f, b1, v) ∨ a = RemoveVF(f, b1, v)) ∧ HoldsAt(PotMobile(b1), t)) ∨ a = PlaceOn(b4, b1, v)]
∧ HoldsAt(Conn(b1, b2), t) ∧ HoldsAt(On(b2, b3), t) ∧ (p = Fr(b1, b2) ∨ p = Fr(b1, b2)) → Breaks(a, p, t)
Finally axiom (B35) contains uniqueness of names axioms.
(B35) UNA[ApplyHF, ApplyVF, RemoveHF, RemoveVF, PlaceOn]
∧ UNA[On, IndOn, Conn, PotMobile, SR, SL, HorizontalContact]
∧ UNA[NAHF, NAVF, FbBA, NHF, Fr, CKF, CSF, Mass, Wt, Vel, Acc, δ]
DCAs
DCAs were not specified in the axioms above. In the definitions in Section 3.1, DCAs were assumed to be parameters. Below we list DCAs axiom-wise and we consider alternatives too.
(B18) : AHFpar(f, b) or just f. (B19) : AVFpar(f, b) or just f. (B22)--(B23) : 1. Wt(b) 2. NAVF(b) (B25) : 1. NAHF(b) (B26) : 1. Fr(b1, b2) or b
where, AHFpar(f, b), AVFpar(f, b) are new parameters corresponding to the (functional) fluents AHF(f, b, v), AVF(f, b, v). (Value(AHFpar(f, b)) can be thought to be v.)
In this case one DCA is enough for every PartValue predicate. However, it is not known if one is enough in all cases.
Validity of Domain-specific Axioms
Consider any scenario of n blocks that are connected to each other. At any given time, axiom (B17) gives n equations (one for each block). If one or more external forces are applied to one or more blocks or a block is kept over one of the other n-1 blocks, then friction forces will come into play (or they would remain in play). Then those n equations contain 3×n unknowns (acceleration of each block and friction forces between surfaces in contact). We get n more equations from axiom (B16).
When velocities of two surfaces in contact are different then axioms (B14) and (B15) give the direction and magnitude of friction forces. If the velocities are the same then one of the three things is possible, block above will slide to the left or to the right or will not slide. In any possibility, axiom (B11), (B12) or (B13) gives one equation. In the worst case there are 3n possibilities of blocks sliding to left, right, or not. In each case, we get 3×n equations (from axioms (B11)-(B17)) with 3×n unknowns. Axioms (B11)-(B13) also impose certain constraints that must be satisfied by any solution to the equations.
We haven't been able to prove (or disprove) that in any scenario, of the 3n possibilities only one will be consistent, and the consistent solution will also be physically possible.[7] However, we conjecture the following.[8]
Conjecture 1 For any scenario, there is at least one consistent solution satisfying the formula (B11) ∧ ... ∧ (B17) which is also physically possible.
Conjecture 2 For scenarios where all forces are applied in one direction or all forces are applied only on one block, there is only one consistent solution satisfying the formula (B11) ∧ ... ∧ (B17).
Conjecture 3 For any scenario, there is only one consistent solution satisfying the formula (B11) ∧ ... ∧ (B17).
PDPs and Dependencies
If f is a function and f(x) is a parameter then f will be referred to as parameter type. f may be a function symbol or composition of multiple δs with a function symbol, e.g. δ(f'), δ(δ(f')), etc. We'll often refer parameter types just as parameters, but correct meaning may be understood from the context. When arity of f is zero, then parameter and parameter type are one and the same thing.
Parameter types that appear as the first argument of some PartValue argument, i.e. types for parameters whose final value is computed by summing the part values, are called as Parameter (types) Defined in Parts (PDPs). In the multiple blocks example, NAHF, NAVF, FbBA, and NHF are PDPs.
We say that a parameter type p depends on other parameter type q if any of the conditions are true in any of the axioms containing p and q
- p is the first argument of PartValue predicate and q appears in some other argument of the same predicate. E.g. NetHorizontalForce depends on NetAppliedHorizontalForce by axiom (B25).
- p is the first argument of PartValue predicate and q appears in the antecedent.
- p is on the consequent side, but not in any PartValue predicate and q is a PDP or q is used in a constraint in the antecedent. E.g. Friction depends on ForceByBlockAbove and Vel by axiom (B14).
Further, the depends is a transitive relationship. Any two non-PDP parameter types p, q that do not depend on each other can mutually depend (mut-depend) on one other if p and q have a mathematical relationship. E.g. Fr mut-depends on CKF, and vice-versa, by axiom (B14).
Finally, we extend the binary and transitive depends relationship with recursive definition.
- depends ο (mut-depends)n ο depends,
where n≥0, ο is used in the sense of composition and (mut-depends)n represents composition of n mut-depends relationships.
We can infer following direct dependencies in the multiple blocks example:
- Acc on NHF by axiom (B17)
- NHF on NAHF by axiom (B25), and FR by axiom (B26)
- FR on FbBA (and Vel) by axioms (B11)--(B15)
- FbBA on NAVF (and Wt) by axioms (B22)--(B23)
The Circumscription Policy CIRCCECA
In addition to domain independent and dependent axioms, a default reasoning mechanism is used to model default assumptions like by default a given action does not occur at a given time point and by default a given action occurrence does not result in a discontinuity for a given parameter. Circumscription of conjunction of domain dependent axioms is used to model default assumptions. Furthermore, extensions of predicates are minimized separately in different parts (of the conjunction). Latter is often referred to by forced separation strategy [shanahan1997], which is based on the idea of filter preferential entailment [sandewall1989]. We extend the circumscription policies of CIRCCEC considered in [miller1996a] and incorporate the new predicates.
BreaksPartBy and PartValue provide partial partial discontinuous changes or partial values for parameters which are aggregated to compute cumulative value for parameters. For carrying out summations, only the minimal extensions of BreaksPartBy and PartValue are considered. That is by default partial discontinuous changes and partial values are zero (or non-existent). Besides, the default assumption that by default a given action occurrence does not result in a discontinuity for a given parameter is valid even after addition of effects of BreaksPartBy.
Let D denote collection of domain dependent axioms, e.g. (B1)--(B35). The circumscription policy, CIRCCECA is[9]:
CIRC[Nar(D); Happens] ∧ CIRC[Eff(D); Initiates, Terminates, Releases] ∧ CIRC[Inst(D) ∧ (EC11) ∧ (EC12) ∧ (EC17p); Breaks; BreaksTo] ∧ CIRC[InstP(D); BreaksPartBy] ∧ ICIRC[ConP(D) ∧ (EC18p); PartValue; 1; Par1 > ... > Parm; PartValue"] ∧ [Con(D) ∧ (EC19p)] ∧ Rem(D) ∧ Una(D) ∧ [(EC1) ∧ ... ∧ (EC15) ∧ (EC16p)]
(EC18p) is emphasized to denote set of axioms generated from general representation in (EC18p). Pari, 1 ≤ i ≤ m, are tuples of parameter types. ICIRC[ConP(D) ∧ (EC18p); PartValue; 1; Par1 > ... > Parm; PartValue"] states that the formula PVA = [ConP(D) ∧ (EC18p)] is circumscribed to minimize extensions of PartValue such that subset of extensions of PartValue providing partial values for parameters of types in Pari are minimized preferably over that for parameters of type in Parj, for any 1 ≤ i < j ≤ m. Section 6.1 provides further details. ICIRC can be defined in terms of CIRC after transformation.
Nar(D), Eff(D), Inst(D), Con(D) and Una(D) stand for axioms describing, respectively, the narrative (Happens facts and statements about the initial values of fluents or parameters), the effects of actions on fluents (using Initiates, Terminates and Releases), the instantaneous effects of actions on parameters (using Breaks and BreaksTo), the mathematical constraints between parameters during different circumstances, and the uniqueness-of-names [miller1996a].
InstP(D) and ConP(D) stand for axioms describing, respectively, the partial instantaneous effects of actions on parameters (using BreaksPartBy) and the partial values for parameters during different circumstances. Rem(D) stand for axioms that are not covered in any other categories. Axioms about secondary fluents are part of Rem(D) for example.
Axiom (EC19p) is not included in PVA, however, value obtained by summation of partial values is explicitly accounted for by ESI-rewrite of axioms expressing partial values.
Definition 1. Explicit Summation Inclusion Rewrite (ESI-rewrite) for axioms with PartValue predicate in the consequent is defined as follows. Every unique Value(p, t) reference, where p is PDP, is replaced by a fresh variable z and for each such case following condition is conjuncted with the antecedent: ((∃r, n.PartValue"(p, t, n, r) ∧ z = #sum⟨r,n.PartValue"(p, t, n, r)⟩) ∨ (¬∃r, n.PartValue(p, t, n, r) ∧ z = Value(p, t)).
For example, ESI-rewrite of (B25) gives
((∃r, n.PartValue"(NAHF(b), t, n, r) ∧ z = #sum⟨r,n.PartValue"(NAHF(b), t, n, r)⟩) ∨ (¬∃r, n.PartValue(NAHF(b), t, n, r) ∧ z = Value(NAHF(b), t)) → PartValue(NHF(b), t, ..., z)
If DM refers to (B1)--(B35) then
Eff(DM) = [(B5)] Inst(DM) = [(B6) ∧ (B28) ∧ ... ∧ (B34)] Con(DM) = [(B3) ∧ (B4) ∧ (B11) ∧ ... ∧ (B17) ∧ (B20) ∧ (B21) ∧ (B27)][10] ConP(DM) = [(B18) ∧ (B19) ∧ (B22) ∧ (B23) ∧ (B25) ∧ (B26)], after ESI-rewrite Una(DM) = [(B35)] Rem(DM) = [(B1) ∧ (B2) ∧ (B7) ∧ ... ∧ (B10) ∧ (B24)]
No specific instance of multiple blocks is described in (B1)--(B25). However to illustrate, couple of forces can be applied on a block. Then, Happens(ApplyVerticalForce(F1, B, 10)) ∧ Happens(ApplyHorizontalForce(F2, B, 12)) will be part of some Nar(D). Also axiom (T8) will be part of some InstP(D).
When Nar(D), Eff(D), Inst(D), InstP(D) and ConP(D) are of a certain form their circumscription is a FO formula. We'll show some forms for each when the circumscription is a FO formula. In all the results we assume that all axioms in D (but not in Rem(D) and Con(D)) are syntactically transformed to following form ∀ x ( ρ( x ) ← Δ(x ) ) , one per unique predicate symbol ρ.
For example, axiom (B6) is rewritten as
BreaksTo(a, p, t, r) ← ∃v. (a = PlaceOn(b1, b2, v) ∧ p = Vel(b1) ∧ r = v)
Also, axioms (B28)-(B34) are of the form Breaks(a, p, t) ← φi(a, p, t), 1 ≤ i ≤ 7, and can be rewritten as single axiom Breaks(a, p, t) ← φ1(a, p, t) ∨ ... ∨ φ7(a, p, t)
Definition 2. If a FOL formula F can be written as ∧i=1 to n∀x(ρi(x) ← Δ(x)), for some n > 0, where each ρi is unique predicate and Δ(x) may contain negation but no implication (← or →), then Comp(F) refers to ∧i=1 to n∀x(ρi(x) ↔ Δ(x)). [11]
Proposition 1. Let Nar(D) = [Happens(a, t) ← Δ(a, t)]. If Δ(a, t) does not mention the predicate Happens then CIRC[Nar(D); Happens] ≡ Comp(Nar(D)).
Proof: The proposition follows directly from Proposition 2 in [lifschitz1994]. ∎
Proposition 2. Let Eff(D) = [(Initiates(a, f, t) ← Δ1(a, f, t)) ∧ (Terminates(a, f, t) ← Δ2(a, f, t)) ∧ (Releases(a, f, t) ← Δ3(a, f, t))]. If none of the Δi(a, t), 1≤i≤3, mention the predicates Initiates, Terminates or Releases then CIRC[Eff(D); Initiates, Terminates, Releases] ≡ Comp(Eff(D)).
Proof: The proposition follows directly from Propositions 2 and 14 in [lifschitz1994]. ∎
Proposition 3. Let Inst(D) = [(Breaks(a, p, t) ← Δ1(a, p, t)) ∧ (BreaksTo(a, p, t, r) ← Δ2(a, p, t, r))]. If none of Δ1(a, p, t) and Δ2(a, p, t, r) mention Breaks, BreaksTo or BreaksPartBy then CIRC[Inst(D) ∧ (EC11) ∧ (EC12) ∧ (EC17p); Breaks; BreaksTo] entails following sentence :
Breaks(a, p, t) ↔ [∃p1[p=δ(p1) ∧ Breaks(a, p1, t)] ∨ Δ1(a, p, t) ∨ ∃r[Δ2(a, p, t, r) ∨ BreaksPartBy(a, p, t, r)]].
Proof: [(Breaks(a, p, t) ← Δ1(a, p, t)) ∧ (Breaks(a, p, t) ← BreaksPartBy(a, p, t, r))] = [(Breaks(a, p, t) ← Δ1'(a, p, t))] where Δ1'(a, p, t)) = [Δ1(a, p, t) ∨ ∃r.BreaksPartBy(a, p, t, r)].
As Δ1'(a, p, t) and Δ2(a, p, t, r)) do not mention Breaks or BreaksTo result follows from Proposition 1 in [miller1996a]. ∎
Propositions 1, 2 and 3 (mostly) have been covered in [miller1996a]. Propositions in the sequel are new.
Proposition 4. Let InstP(D) = [(BreaksPartBy(a, p, t, r) ← Δ(a, p, t, r))]. If Δ(a, p, t, r) does not mention the predicate BreaksPartBy then CIRC[InstP(D); BreaksPartBy] ≡ Comp(InstP(D)).
Proof: The proposition follows directly from Proposition 2 in [lifschitz1994]. ∎
Circumscription with Intra-predicate priorities
Circumscription is defined for minimization of extensions of certain predicates. Further, inter-predicate priorities are given for prioritized circumscription. We'll extend that notion to intra-predicate priorities, based on first argument in particular. Before we define that, consider following observation.
Observation 1. If P and Q are overloaded predicates, i.e. they are used in different relation types, then P < Q can be understood in terms of P < Q, where P = [P1, ..., Pk] and Q = [Q1, ..., Qk] and Pi and Qi are P and Q restricted to specific relation type. Each Pi (and Qi) corresponds to unique relation that P (and Q) is used for.
Definition 3. Intra-predicate prioritized circumscription is denoted as ICIRC[F ; P; n; f1 > ... > fm; Z], where circumscription of formula F is sought to minimize the extensions of P such that minimization of subset of extensions of P with n-th argument g1(x), g1 ∈ fi, is given priority over that with argument g2(x), g2 ∈ fj, for any g1, g2 and 1 ≤ i < j ≤ m, while extensions of Z may vary.
Definition 4. Let Ω = Par1 ∪ ... ∪ Parm = Set of PDPs in D. Let PVA = ConP(D) ∧ (EC18p), such that axioms in (EC18p) are instantiated separately for every parameter type in PDPs. Further, let P = {PartValue} and Z = {PartValue"}.
Instantiation of (EC18p) for parameter type NHF, for example, will give axiom
∃r. PartValue(NHF(b), t, ..., r) ∧ s=#sum⟨r. PartValue(NHF(b), t, ..., r)⟩ ↔ PartValue"(NHF(b), t, n, s).
Definition 5. If UNA[Ω][12] and if in all occurrences of PartValue and PartValue" predicates in PVA, the 1st argument is of the form g(x), for some g ∈ Ω then every occurrence PartValue(g(x), ...) and PartValue"(g(x), ...) can be replaced by PartValueg(x, ...) and PartValue"g(x, ...). The resulting formula is denoted by PVAΩ. It has similar signature to F except that constants in P and Z are replaced by PΩ and ZΩ, respectively, where PΩ = PΩ1 ∪ ... ∪ PΩm and PΩi = {PartValueg|g ∈ Pari}. PΩ is similarly defined.
Lemma 1 establishes relationship between Intra-predicate prioritized circumscription, ICIRC, and Prioritized circumscription, CIRC, in the special circumstance considered in Definition 5. Equivalence is defined more formally in Definition A3 in the Appendix. Lemma A4 gives a stronger result on equivalence - between PVA and PVAΩ, not just their circumscriptions - using an observation in Lemma A3.
Lemma 1. ICIRC[PVA ; P; 1; Par1 > ... > Parm; Z] can be equivalently computed from CIRC[PVAΩ ; PΩ1 > ... > PΩm; ZΩ].
Proof sketch. If extension of P in PVA are minimized (varying Z) then the first arguments in that extension should be of the form g(...), for some g ∈ Ω. Also, interpretation of constants in Ω are not affected by the circumscriptions (as P and Z are disjoint from Ω). Since UNA[Ω] there exists one to one mapping from minimal extensions of P (and corresponding extensions of Z) to that of PΩ (and corresponding ZΩ). ∎
Next we discuss how partitioning of PDPs may be determined based on dependencies between PDPs (depends relation was defined in the Section 5).
Definition 6. If PDPs have no cyclic dependencies then we can partition Ω into {Par1, ..., Parm}, for some m, such that if g ∈ Pari depends on h ∈ Parj then j > i. Such a partition will be referred to as PDP-partitioning.
If PDP-partitioning is possible then PVAΩ becomes pseudo-hierarchical type 1 formula, that we define next (starting with hierarchical formula). In that special case its circumscription is equivalent to the completion.
Definition 7. Let F be a FO formula which is a conjunction of axioms of the form φ(x) → ρ(x) where ρ is a predicate symbol and φ(x) is a FO formula without any implications and x as the only free variables. F is said to be hierarchical if there exists an assignment of ordinal levels to predicates such that for each axiom any predicate appearing in the antecedent, including in an aggregate expression, is of strictly lower level than the predicate in the consequent. Using the assignment, predicates in F, PF, can be partitioned into {P0, P1, ..., Pn}, such that predicates in Pi have ordinal levels i. All predicates that do not appear in consequent of any of the axioms are assumed to be in P0, and may not be mentioned explicitly. Such a partitioning is referred to as stratification. Further F can be partitioned as F1 ∧ ... ∧ Fn, such that axioms with ordinal level i for consequent predicate are in Fi. This partitioning is referred to by F-partition. [13].
Lemma 2. If F is hierarchical with stratification {P1, ... , Pn} and F-partition {F1, ..., &Fn} then CIRC[F; P1 > ... > Pn] = Comp(F).
Proof. By proposition 15 of [lifschitz1994], CIRC[F; P1 > ... > Pn] = ∧i=1 to n CIRC[F; Pi; Pi+1, ..., Pn].
CIRC[F1 ∧ ... ∧ Fn; Pi; Pi+1, ..., Pn] = CIRC[F1 ∧ ... ∧ Fi; Pi] ∧ Fi+1 ∧ ... ∧ Fn, by theorem 9.4.6 from [shanahan1997] because by Lemma A1 in the Appendix, model for Fi+1 ∧ ... ∧ Fn can be created from model for CIRC[F1; ∧ ... ∧ Fi; Pi; Pi+1, ..., Pn] and F1 ∧ ... ∧ Fi does not contain any predicate from Pi+1, ..., Pn. (See Lemma A2 in Appendix for proof from [shanahan1997])
CIRC[F1 ∧ ... ∧ Fi; Pi] = F1 ∧ ... ∧ Fi-1 ∧ CIRC[Fi; Pi], because F1 ∧ ... ∧ Fi-1 do not contain predicates from Pi.
By propositions 2 and 14 in [lifschitz1994], CIRC[Fi; Pi] = Comp(Fi).
Therefore, ∧i=1 to n CIRC[F; Pi; Pi+1, ..., Pn] = ∧i=1 to n(Comp(Fi) ∧ Fi) = ∧i=1 to n Comp(Fi) = Comp(F). ∎
Definition 8. Let F be a hierarchical formula with stratification {P1, ... , P2*m} and F-partition {F1, ... , F2*m}. Consider a new formula F' which we call pseudo-hierarchical of type 1, defined as, F' = F1 ∧ Comp(F2) ∧ ... ∧ F2*m-1 ∧ Comp(F2*m). Stratification of F is split into {P'1, ... , P'm} and {Z'1, ... , Z'm}, such that P'i = P2*i-1 and Z'i = P2*i. F' = F'1 ∧ F'2 ∧ ... ∧ F'2*m-1 ∧ F'2*m, where F'2*i-1 = F2*i-1 and F'2*i = Comp(F2*i).
Lemma 3. If F is hierarchical with stratification {P1, ... , P2*m} and F' constructed as per Definition 8 then CIRC[F'; P'1 > ... > P'm; Z'1, ... , Z'm] = Comp(F') = Comp(F).
Proof. By proposition 15 of [lifschitz1994], CIRC[F'; P'1 > ... > P'm; Z'1, ... , Z'm] = ∧i=1 to m CIRC[F'; P'i; P'i+1, ..., P'm, Z'1, ... , Z'm].
CIRC[F'1 ∧ ... ∧ F'2*m; P'i; P'i+1, ..., P'm, Z'1, ... , Z'm] = CIRC[F'1 ∧ ... ∧ F'2*i-1; P'i; Z'1, ... , Z'i-1] ∧ F'2*i ∧ ... ∧ F2*m, by theorem 9.4.6 from [shanahan1997] because model for F'2*i ∧ ... ∧ F'2*m can be created from model for CIRC[F'1 ∧ ... ∧ F'2*i-1; P'i; Z'1, ... , Z'm] and F'1 ∧ ... ∧ F'2*i-1 does not contain any predicate from P'i+1, ..., P'm, Z'i, ... , Z'm.
CIRC[F'1 ∧ ... ∧ F'2*i-1; P'i; Z'1, ... , Z'i-1] = F'1 ∧ ... ∧ F'2*i-2 ∧ CIRC[F'2*i-1; Pi], because F'1 ∧ ... ∧ F'2*i-2 do not contain predicates from Pi.
By propositions 2 and 14 in [lifschitz1994], CIRC[F'2*i-1; Pi] = Comp(F'2*i-1).
Therefore, ∧i=1 to m CIRC[F'; P'i; P'i+1, ..., P'm, Z'1, ... , Z'm] = ∧i=1 to m(Comp(F'2*i-1) ∧ F'2*i-1 ∧ F'2*i) = ∧i=1 to m(Comp(F'2*i-1) ∧ F'2*i) = Comp(F'), because F'2*i = Comp(F'2*i). ∎
Lemma 4. If PDP-partitioning of Ω is possible and {Par1, ..., Parm} is the PDP-partition then CIRC[PVAΩ ; PΩ1 > ... > PΩm; ZΩ] = Comp(PVAΩ).
Proof. (B18p) is a set of bidirectional axioms. Let (B18p)f be unidirectional sub-formuala such that PartValue" appears in the consequent. Then PVAH = [ConP(D) ∧ (EC18p)f] is a hierarchical formula. PVAΩ is corresponding pseudo-hierarchical of type 1 and PΩi and ZΩi correspond, respectively, with P'i and Z'i in Definition 8. Result follows from Lemma 3. ∎
Proposition 5. If UNA[PDPs] and PDPs have acyclic dependencies over one another, and {Par1, ..., Parm} is their PDP-partition, then ICIRC[PVA ; P; 1; Par1 > ... > Parm; Z] = Comp(PVA).
Proof. Follows from Lemmas 1 and 4. ∎
The requirement that every axiom in ConP(D) is about a specific parameter type will usually satisfy. The important conditions in Proposition 5 are that of uniqueness and acyclic dependencies within PDPs. Since PDP-partition can be computed automatically, priorities may not be specified - ICIRC[PVA; P; 1; _; Z] - in such cases.16
Lemma 5. ICIRC[ConP(DM) ∧ (EC18p); PartValue; 1; _ ; PartValue"] = Comp(ConP(DM)) ∧ (EC18p).
Proof. Ω = {NAHF, NAVF, FbBA, NHF} and with following dependencies: i) NHF depends on NAHF, ii) NHF depends on Fr that depends on FbBA, iii) FbBA depends on NAVF. There is no cyclical dependency and {[NAHF, NAVF], FbBA, NHF} is a PDP-partition. And, UNA[Ω] by axiom (B35). Therefore, ICIRC[ConP(DM) ∧ (EC18p); PartValue; 1; _ ; PartValue"] = ICIRC[ConP(DM) ∧ (EC18p); PartValue; 1; NAHF;NAV F > FbBA > NHF ; PartValue"]. Result follows from Proposition 5. ∎
Comparisons with other variants of circumscriptions
Difference from parallel and prioritized circumscriptions [mccarthy1987] is straight-forward, because in ICIRC we consider intra-predicate priorities. There are several variants of circumscriptions namely pointwise circumscription [lifschitz1987], nested abnormality theories [lifschitz1995], autocircumscription [perlis1988] and value minimization [baral1996].
Pointwise Circumscription
Pointwise circumscription of predicate P denoted by CP(A(P, Z)) is described by the formula
A(P, Z) ∧ ∀x z[P(x) ∧ A(λy.(P(y) ∧ x≠y), z)]
Instead of single minimality condition for predicate minimization, minimality of predicate at every point is considered through infinite conjunctions of local minimality conditions, where the local minimality condition is that it is impossible to change the value of the predicate from true to false at one point.
ICIRC is not quite point-wise minimization as it takes into account minimization in terms of subset relationships between extensions (like CIRC). Its just that the extensions are divided by values of a given arguments and minimizations of subsets with certain given values are prioritized over subsets with certain other given values.
Note. We didn't take into account prioritized pointwise circumscription as difference is evident without it.
Nested Abnormality Theories
In nested abnormality theories axioms have nested structure, with each level corresponding to another application of the circumscription operator. This approach is much less elaboration tolerant.
Axioms are described in nested blocks and block is of the form {C1, ..., Cm : A1, ..., An} where Ci are function and/or predicate constants and Ai are blocks or formulas. A nested abnormality theory (NAT) is a (possibly infinitely many) set of blocks. The semantics of NATs is characterized by function φ, which is defined recursively as
φ{C1, ..., Cm : A1, ..., An} = ∃ ab.CIRC[φAsub>1</sub> ∧ ..., φAn; Ab; C1, ..., Cm].
NAT is a good alternative for prioritization. If PVA (defined earlier) are all about specific parameter types and UNA[PDPs] then nesting of axioms in PVA can be decided based on PDP-partition. At each level of nesting predicate PartValue can be minimized. However, notion of intra-predicate prioritization will still have to be introduced to model ICIRC-style circumscription.
Autocircumscription
Autocircumscription is another way of looking at parallel circumscription where roughly speaking P < Q is interpreted as ∀x(¬Q(x) → ¬P(x)) instead of ∀x(P(x) → Q(x)).
Value minimization.
In this circumscription value of a function is minimized relative to an ordering of its range. Whereas with ICIRC we intend to minimize predicates.
Discussion
Choice of DCAs
In Section 4.1 we saw that parameters Wt(b) and NAVF(b) are more apt in axioms (B22)--(B23), whereas identifier f is enough for (B18)--(B19). We assumed that DCAs to be parameters in Section 3.1, however, apt sorts for DCAs and number of DCAs required per predicate must be investigated in detail.
UNA[PDPs, δ] is too strict
We may want to say Acc(b) = δ(Vel(b)) but that would violate the uniqueness requirement of Proposition 5. We can at-least express that Value(Acc(b)) = Value(δ(Vel(b))). However, that works fine for non-PDPs (and Acc(b) and Vel(b) are non-PDPs). Assume for now that Acc and Vel are PDPs. The partial values of Acc(b) and δ(Vel(b)) will not be added as expected unless we can state Acc(b) = δ(Vel(b)).[14]. We need a mechanism to be able to state equivalences between PDPs. To start with, we can allow explicit equivalences to be asserted but none to be inferred (i.e. allow no mechanism to infer equivalences). Construction of PVAΩ in Definition 5 and PDP-partitioning in Definition 6 can take that into account with small modifications.
Independence of components of cumulative effect
Components can be described individually (and aggregated implicitly) only if they are independent. In other words the preconditions for components must be independent for components to be specified independently. We saw in the tank example that empty tank condition limits ability to specify contributions of each scoop independently. Its a future work to investigate how some of the benefits of our approach (more general, concise and elaboration tolerant domain descriptions) can be extended to scenarios such as scooping water from tank where the components of cumulative effect can reach a point where they seize to be independent. Independence may be more critical in discontinuous changes such as by scoops, because continuous changes happen in very small amount and preconditions can be effectively set. For instance in case of multiple pipes filling a tank the overflow condition can be readily accounted for (by adding precondition for every component contribution).
Applying prioritized circumscription
We use prioritized circumscription, of a special kind, to perform closed world reasoning for partial effects. Its use may be considered for other predicates as well. For example, in the multiple blocks example we had specified that AHF breaks continuity of NAHF and potentially, NHF on connected blocks. However, latter depends on former and break in latter may be inferred automatically, which while can be encoded as a FO formula but that formula, we believe, may not be circumscribed to a FO formula with only parallel circumscription.
ICIRC is an over-kill at times
Axiom (B23) expresses that when b2 is on b1 vertical force on any block above b2 contributes to FbBA(b1, b2). It uses a derived fluent indirectly-on to capture transitive on relationships between blocks. However, an equivalent axiomatic description without indirectly-on is possible:
HoldsAt(On(b3, b2), t) ∧ HoldsAt(On(b2, b1), t)
→ PartValue(FbBA(b1, b2), t, ..., Value(FbBA(b2, b3)))
Since the On relationship is asymmetric and irreflexive (as expressed in axiom (B9)) extensions of PartValue(FbBA(b1, b2), t, ..., v) would be minimized as expected by the completion of axiom above. However, that's not possible under ICIRC.
Implementation
Many Prolog based systems such as XSB [15] support aggregate functions, including aggregate sum. Any Logic Program based implementation of Event Calculus can be extended to support the version of EC proposed in this paper, except for use of derivatives. As such we are not aware of any decently mature work in combining logic reasoning with numerical reasoning over ODEs in Constraint Logic Programming or other domains. Some hints were provided by authors in [miller1996]. Any such work must be extended with semantics for aggregates summation. This is worth investigation in the future.
Summary
We have proposed a new version of Event Calculus that extends the version by Miller and Shanahan to reason with continuously varying parameters. We observe that explicit summation of component effects for knowing the cumulative effects tends to make domain descriptions very scenario-specific and less elaboration tolerant. Some of these components are independent, in the sense of their preconditions being independent, and they can be specified individually and summed implicitly. We introduce two new predicates for specifying component effects, one for discontinuous change and other for continuous relationships between parameters, which are interpreted using the semantics of aggregate summation. We have discussed the default assumptions associated with the new predicates and defined corresponding circumscription policies. When there is no cyclical dependency between partially defined parameter values, circumscribed formula is shown to be first order and, in fact, it is equivalent to the completion of the formula. As a result domain descriptions can be more general and concise than its possible by existing formalisms. Furthermore, elaboration with new (independent) cumulative effects becomes additive.
Appendix
Lemmas
Definition A1. Let φ(x) is some formula with x the only free variables and μ is a variable mapping from x. Then μ(φ(x)) refers to the formula obtained after substitution of variables x in φ(x) according to μ.
Definition A2. If M1 and M2 are two models with interpretations for different constants, then M = M1 + M2 represents interpretation for union of the constants such that M[C], for any constant symbol C, equals M1[C] if C belongs to M1, equals M2[C] if C belongs to M2 and M1[C] = M2[C] if C belongs to both M1 and M2.
Lemma A1. If F is a hierarchical formula with stratification {P1, ..., Pn} and F-partition {F1, ..., Fn} then given a model M of F1 ∧ ... ∧ Fi, with interpretation for all constants but that in Pi+1, ..., Pn, a mapping G exists from interpretations of F1 ∧ ... ∧ Fi to interpretations of Fi+1 ∧ ... ∧ Fn such that, M+G(M) is a model of F1 ∧ ... ∧ Fn.
Proof. We prove by induction and show one of possibly many methods of creating G(M). Given M, we extend it to a model M+Mi+1 for F1 ∧ ... ∧ Fi+1 as follows.
Let Q ∈ Pi+1 and Q ⊆ S1 × ... × Sm where Si is the sort of i-th argument. Let FQ ⊆ Fi+1 be the formula containing all axioms with predicate Q in the consequent. We assume without loss of generality that all axioms in FQ have same arguments all of which are variable symbols. Further, they can be combined by taking disjunction of the antecedent and rewritten in one axiom such as Δ(x) → Q(x). Then, Mi+1[P] = {(a1, ..., am) | (a1, ..., am) ∈ S1 × ... × Sm and ∃μ.(μ(x) = (a1, ..., am) and M ⊨ μ(Δ(x)))}.[16]
It is easy to verify that M+Mi+1 is a model of F1 ∧ ... ∧ Fi+1. Likewise, we can construct a model M+Mi+1+Mi+2 for F1 ∧ ... ∧ Fi+2 from M+Mi+1.
M+Mi+1+...+Mn will be a model for F1 ∧ ... ∧ Fn. Now letting G(M) = Mi+1+...+Mn, we have constructed a model for F1 ∧ ... ∧ Fn from a model M for F1 ∧ ... ∧ Fi. ∎
Lemma A2 plainly restates proof of theorem 9.4.6 from [shanahan1997], only for our specific requirements.
Lemma A2. If F is a hierarchical formula with stratification {P1, ..., Pn} and F-partition {F1, ..., Fn}, CIRC[F1 ∧ ... ∧ Fn; Pi; Pi+1, ..., Pn] = CIRC[F1 ∧ ... ∧ Fi; Pi] ∧ Fi+1 ∧ ... ∧ Fn.
Proof. Let M be a model of CIRC[F1 ∧ ... ∧ Fn; Pi; Pi+1, ..., Pn]. Then M is also a model of F1 ∧ ... ∧ Fi and Fi+1 ∧ ... ∧ Fn. Assume that M is not a model of CIRC[F1 ∧ ... ∧ Fi; Pi], i.e. M is not a minimal model of F1 ∧ ... ∧ Fi with respect to Pi. So there exists a model M' of F1 ∧ ... ∧ Fi such that a) M'[Q] = M[Q] for all constants not in P and all constants in P0, ..., Pi-1, b) M'[Q] ⊆ M[Q] for all Q ∈ Pi and c) M'[Q] ⊂ M[Q] for some Q ∈ Pi. From lemma A1, there exists a model M'+G(M') for F1 ∧ ... ∧ Fn. But then M'+G(M') < M (in the context of CIRC[F1 ∧ ... ∧ Fn; Pi; Pi+1, ..., Pn]) which is a contradiction.
To prove the other half, let M be a model of CIRC[F1 ∧ ... ∧ Fi; Pi] ∧ Fi+1 ∧ ... ∧ Fn. Then M is also a model of F1 ∧ ... ∧ Fn. Assume that M is not a model of CIRC[F1 ∧ ... ∧ Fn; Pi; Pi+1, ..., Pn], i.e. M is not a minimal model of F1 ∧ ... ∧ Fn w.r.t. Pi. So there exists a model M' of F1 ∧ ... ∧ Fn such that a) M'[Q] = M[Q] for all constants not in P and all constants in P0, ..., Pi-1, b) M'[Q] ⊆ M[Q] for all Q ∈ Pi and c) M'[Q] ⊂ M[Q] for some Q ∈ Pi. M' is also a model of F1 ∧ ... ∧ Fi. But then M' < M (in the context of CIRC[F1 ∧ ... ∧ Fi; Pi]) which is again a contradiction. ∎
PVA and PVAΩ introduced in Definitions 4 and 5 are reused below. Recollect that UNA[Ω] is one of the conditions imposed in Definition 5.
Definition A3. Let φ is a FO formula such that in all occurrences of PartValue and PartValue" predicates, the first argument is of the form C(x) for some C ∈ Ω. Let φΩ be the formula obtained from φ by replacing every occurrence of PartValue(C(x), ...) and PartValue"(C(x), ...) with PartValueC(x, ...) and PartValue"C(x, ...). PVA is said to be equivalent to PVAΩ only if for any φ, PVA ⊨ φ iff PVAΩ ⊨ φΩ.
Let I be an interpretation of PVA, then I(PartValue) ⊆ P × T × ... × R and I(PartValue") ⊆ P × T × ... × R. Lemma A3 says that if a model of PVA has in its extension a tuple such that first argument is a parameter but not mapped to by any parameter types in Ω then that tuple is useless because there exists another exact model just without it. And in FOL any formula is satisfied only if it is satisfied in every model.
Lemma A3. For every model M1 of PVA with interpretation I1 such that I1(PartValue) contains a tuple (P, T, ..., R) and ¬∃ C, x (C ∈ Ω ∧ C(x) = P), there exists a model M2 of PVA with interpretation I2 such that I2(PartValue) = I1(PartValue) \ (P, T, ..., R) and I2(C) = I1(C) for every other constant. Same holds for PartValue".
Proof. Given for every occurrence of PartValue predicate in PVA the first argument is of the form C(x) for some C ∈ Ω and that ¬∃ C, x (C ∈ Ω ∧ C(x) = P), formula PartValue(P, T, ..., R) cannot be resolved with any PartValue(y) in PVA. Therefore, PartValue(P, T, ..., R) or ¬PartValue(P, T, ..., R) is inconsequential to I1 being a model of PVA. The way I2 is constructed from I1 only change is that in I2 ¬PartValue(P, T, ..., R) holds whereas in I1 PartValue(P, T, ..., R) holds. If I1 is a model of PVA then so is I2. ∎
Lemma A4. PVA is equivalent to PVAΩ.
Proof. Recall that P, T and R are parameter, time and reals sorts.
Let I be an interpretation of PVA. I(PartValue) ⊆ P × T × ... × R and I(PartValue") ⊆ P × T × ... × R. Constructions below are shown only with predicate constant PartValue but they apply just as is to PartValue".
For any C ∈ Ω, let I(PartValue)C = {(p, t, ..., r) | (p, t, ..., r) ∈ I(PartValue) and ∃x(I(C(x)) = p)}. Since range of I(C), C∈Ω, are disjoint, any tuple in I(PartValue) is mapped to single I(PartValue)C.
By Lemma A3, we can restrict ourselves to only those models where {I(PartValue)C | C∈Ω} is also a partition of I(PartValue), i.e. I(PartValue) = ∪C∈Ω I(PartValue)C.
Notice that this condition is automatically satisfied when PVA is circumscribed w.r.t. PartValue (and PartValue" is varied) in Lemma 1.
Let I(PartValue)ΩC = {(x, t, ..., r) | (p, t, ..., r) ∈ I(PartValue)C and I(C(x)) = p}. Since I(C) is also a one to one function the inverse mapping from p to x is unique.
Let IΩ be an interpretation of PVAΩ. For any C∈Ω, let MC: S1 × ... × Sm ↦ P be a one to one function such that ranges of MC, C∈Ω are disjoint. Si are sorts of the arguments of function C. If C ∈Ω is a function constant in PVAΩ then MC = IΩ(C).
For any C∈Ω, let IΩ(PartValue)(MC, C) = {(p, t, ..., r) | (x, t, ..., r) ∈ IΩ and p = MC(C(x))}
Given a model of PVA with interpretation I we can construct a model for PVAΩ with interpretation IΩ as follows:
- IΩ(C) = I(C) for any C different from PartValue, PartValue".
- IΩ(PartValueC) = I(PartValue)ΩC, C ∈ Ω.
- IΩ(PartValue"C) = I(PartValue")ΩC, C ∈ Ω.
It can be verified that IΩ is a model of PVAΩ.
For any model of PVA there exists a unique model of PVAΩ (because IΩ(PartValueC) and IΩ(PartValue"C) are created uniquely).
Likewise, given a model of PVAΩ with interpretation IΩ we can construct a model for PVA with interpretation I as follows:
- I(C) = IΩ(C) for any C different from PartValueD, PartValue"D, D∈Ω, and C ∉ Ω
- I(C) = any MC mapping, for C∈Ω
- I(PartValue) = ∪C∈ΩIΩ(PartValue)(I(C), C).
- I(PartValue") = ∪C∈ΩIΩ(PartValue")(I(C), C).
It can be verified that I is a model of PVA.
For any model of PVAΩ, there exists a unique model of PVA per interpretation of constants C∈Ω. Some constants in Ω may not be function constants in PVAΩ and many MC mappings are possible in such case.
The fact that new interpretations are models in the two cases just described can be verified easily.
Let φ and φΩ be FO formula as defined in Definition A3.
If PVA ⊭ φ then there exists a model M with interpretation I of PVA such that M does not satisfy φ. We can construct IΩ (and model MΩ) from I (and M) as shown above. Then MΩ also doesn't satisfy φΩ. That is PVAΩ ⊭ φΩ.
Therefore, PVA ⊭ φ iff FΩ ⊭ φΩ. From that we can infer that F ⊨ φ iff FΩ ⊨ φΩ. ∎
More Event Calculus
EC is written in a sorted predicate calculus with equality. Following notes are mainly from [miller2002] and [miller1996]. [17]
This section covers functions, predicates and axioms not covered in main section.
Table 2 lists predicates, their relation types and a description.
| Predicate | Relation Type | Description |
|---|---|---|
| Happens | A × T | Happens(A, T): action A occurs at time T |
| HoldsAt | F × T | HoldsAt(F, T): fluent F is true at time T |
| Initiates | A × F × T | Initiates(A, F, T): if A occurs at T it will initiate the fluent F |
| Terminates | A × F × T | Terminates(A, F, T): if A occurs at T it will terminate the fluent F |
| Releases | A × F × T | Releases(A, F, T): if A occurs at T it will disable the fluents innate persistence. |
| InitiallyTrue | F | InitiallyTrue(F): fluent F is true initially |
| InitiallyFalse | F | InitiallyFalse(F): fluent F is false initially |
| Clipped | T × F × T | Clipped(T1, F, T2): fluent F is terminated between times T1 and T2 |
| Declipped | T × F × T | Declipped(T1, F, T2): fluent F is initiated between times T1 and T2 |
| Trajectory | F × T × P × T × X | Trajectory(F, T1, P, T2, X): fluent F is initiated at time T1 and continues to hold until time T1+T2, this results in parameter P having a value of X at time T1+T2 |
| AntiTrajectory | F × T × P × T × X | AntiTrajectory(F, T1, P, T2, X): fluent F is terminated at time T1 and continues not to hold until time T1+T2, this results in parameter P having a value of X at time T1+T2 |
| BreaksTo | A × P × T × R | BreaksTo(A, P, T, R): at time T, an occurrence of action A will cause parameter P to instantaneously take on value R |
| Breaks | A × P × T | Breaks(A, P, T): at time T, action A potentially causes discontinuity in parameter P |
| LeftContinuous | P × T | LeftContinuous(P, T): at time T, the function associated with parameter P is left-hand continuous |
| RightLimit | P × T × R | RightLimit(P, T, R): at time T, the right limit value of function associated with parameter P is R |
| Continuous | P × T | Continuous(P, T): at time T, the function associated with parameter P is continuous |
| Differentiable | P × T | Differentiable(P, T): at time T, the function associated with parameter P is differentiable |
| < | T × T | the standard order relation for time |
Function ValueAt is used with the Trajectory and AntiTrajectory predicates. ValueAt: P × T ↦ X. ValueAt(P, T) is the value of parameter P at time T.
Definitions of Trajectory and AntiTrajectory predicates are axiomatized below.
(EC20) ValueAt(p, t1+t2)=x ← [Happens(a, t1) ∧ Initiates(a, f, t1)\\ ∧ 0<t2 ∧ Trajectory(f, t1, p, t2, x) ∧ ¬Clipped(t, f, t1+t2)]
(EC21) ValueAt(p, t1+t2)=x ← [Happens(a, t1) ∧ Terminates(a, f, t1)\\ ∧ 0<t2 ∧ AntiTrajectory(f, t1, p, t2, x) ∧ ¬Declipped(t, f, t1+t2)]
ValueAt function along with Trajectory and AntiTrajectory predicates is used to represent trajectories, delayed actions and gradual changes.
More Extensions for Partial Values
| Predicate | Relation Type | Description |
|---|---|---|
| BreaksPartTo | A × P × T × R | BreaksPartTo(A, P, T, R): if action A occurs at time T, then it contributes discontinuous change of value R to value of parameter P. (The exact definition is given by (EC23p)). |
| BreaksPartBy | A × P × T × R | BreaksPartBy(A, P, T, R): if action A occurs at time T, then it discontinuously changes value of parameter P by value of R. (The exact definition is given by (EC23p)). |
| PartValue | P × T × Pn × R | PartValue(P, T, P1, ..., Pn, R): A part value of parameter P depends on parameters P1, ..., Pn, where n≥0, and equals R. |
| PartValue" | P × T × N × R | PartValue"(P, T, N, R): Net part value of parameter P that depends on exactly N parameters. (The exact definition is given by (EC24p)). |
BreaksPartBy introduced earlier accounted for relative discontinuous change. For absolute, but partial, changes we introduce BreaksPartTo predicate. (EC16p) and (EC17p) are modified to account for the new predicate.
(EC16p') (∃a, r.(BreaksPartTo(a, p, t, r) ∧ Happens(a, t)) ∧ ∃a, r.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))
∧ s1=#sum⟨r, a.(BreaksPartTo(a, p, t, r) ∧ Happens(a, t))⟩
∧ s2= Value(p, t) + #sum⟨r, a.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))⟩
∧ s = s1 + s2)
∨ (∃a, r.(BreaksPartTo(a, p, t, r) ∧ Happens(a, t)) ∧ ¬∃a, r.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))
∧ s=#sum⟨r, a.(BreaksPartTo(a, p, t, r) ∧ Happens(a, t))⟩)
∨ (¬∃a, r.(BreaksPartTo(a, p, t, r) ∧ Happens(a, t)) ∧ ∃a, r.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))
∧ s= Value(p, t) + #sum⟨r, a.(BreaksPartBy(a, p, t, r) ∧ Happens(a, t))⟩)
→ RightLimit(p, t, s)
(EC17p') BreaksPartTo(a, p, t, r) ∨ BreaksPartBy(a, p, t, r) → Breaks(a, p, t)
Circumscription
Models of Circumscription
A structure M for a one sorted (for simplicity) language is determined by its universe |M| and by the interpretations of M[C] of all individual, function and predicate constants C in the language.
By proposition 1 in [lifschitz1994], A structure M (of A) is a model of CIRC[A; P; Z] if and only if < is minimal relative to ≤P;Z.
For two structures M1, M2, M1 ≤P;Z M2 if
- |M1| = |M2|,
- M1[C] = M2[C] for every constant C which is different from P and does not belong to Z,
- M1[P] ⊂ M2[P]
i.e. M1 and M2 differ only in how they interpret P and Z, and the extent of P in M1 is a subset of its extent in M2.
Computing Circumscription (in Restricted Formulas)
Definitions
Occurence of a predicate symbol in a formula - where ⊃ and ≡ have been eliminated in favor of other connectives such as ∨ - is positive, if it is in the range of an even number of negations, and negative otherwise.
A formula is positive relative to a predicate if all occurrences of P in it are positive, and negative if all occurrences of P are negative. A formula which does not contain P at all is both positive and negative.
A formula is definite in the predicates Pi ... Pn if it is the conjunction of implications of the form F(P1 ... Pn) ⊃ Pi(t1 ... tk), where t1 ... tk are terms and F(P1 ... Pn) is a formula positive relative to each of P1 ... Pn.
Two languages of many-sorted first-order predicate calculus (MSFOPC) are disjoint if their sets of constant symbols, function symbols and predicate symbols are all disjoint.
Propositions and Theorems
1. Proposition 2 from [lifschitz1994], on equivalence with predicate completion.
If F(x) does not contain P, then the circumscription CIRC[∀x(F(x) ⊃ P(x)); P] is equivalent to ∀x(F(x) ≡ P(x)).
Note that if there are several such formula, ∀x(F1(x) ⊃ P(x)), ..., ∀x(Fn(x) ⊃ P(x)), then they can be replaced by one such formula: ∀x[F1(x) ∨ ... ∨ Fk(x)) ⊃ P(x)].
Let P be a tuple of predicate constants.
2. From [lifschitz1994],
For any sentence B not containing P, Z, CIRC[A(P, Z) ∧ B; P; Z] ≡ CIRC[A(P, Z); P; Z] ∧ B.
3. Proposition 4 from [lifschitz1994], on separation of positive and negative formula.
If B(P) is negative, then the circumscription CIRC[A(P) ∧ B(P); P] is equivalent to CIRC[A(P); P] ∧ B(P).
4. Proposition 5 from [lifschitz1994], on circumscription of positive formula.
If A(P, Z) is positive relative to P, then teh circumscription CIRC[A(P, Z); P; Z] is equivalent to A(P, Z) ∧ ¬∃xz[P(x) ∧ A(λy(P(y) ∧ x ≠ y), z)].
where predicate expression λx1...xnF(x1 ... xn) is used for predicate F(x1 ... xn).
5. Proposition 8 from [lifschitz1994],
If A(P1...Pn; P1; P1...Pn) is the universal closure of a formula definite in P1...Pn, the circumscription CIRC[A(P1...Pn); P1; P2...Pn] is equivalent to A(P1...Pn) ∧ ∀x[P1(x) ≡ ∀p1...pn(A(p1...pn) ⊃ p1(x))].
6. Proposition 14 from [lifschitz1994],
If A(P, Z) is positive relative to each member Pi of P, then the parallel circumscription CIRC[A(P, Z); P; Z] is equivalent to ∧iCIRC[A(P, Z); Pi; Z].
7. By proposition 15 of [lifschitz1994], prioritized circumscription is equivalent to conjunction of parallel circumscriptions.
- CIRC(A; P1 > ... > Pk; z) = ∧i=1 to k CIRC(A; Pi; Pi+1, ..., Pk, Z)
8. Theorem 9.4.6 from [shanahan1997],
If there exists a mapping F from interpretations of L1 to interpretations of L2 such that, for any interpretation M of L1 that satisfies Σ , M+F(M) is a model of Δ, then CIRC[Σ ∧ Δ; ρ*; σ*] is equivalent to CIRC[Σ; ρ*; σ*] ∧ Δ.
where L1 and L2 are disjoint and compatible languages of MSFOPC, Σ is a formula of L1, Δ is a formula of L1 + L2, ρ* is a tuple of predicate symbols from L1, and σ* is a tuple of predicate, function and constant symbols from L1 + L2 that includes every predicate, function and constant symbol in L2.
9. Theorem 9.4.7 from [shanahan1997],
If there exists a mapping G from interpretations of L1 to interpretations of L2 such that, for any interpretation M of L1 that satisfies Σ, M+G(M) is a model of CIRC[Δ; ρ2*; σ2*], then, CIRC[Σ ∧ Δ; ρ1*, ρ2*; σ1*, σ2*] is equivalent to CIRC[Σ; ρ1*; σ1*] ∧ CIRC[Δ; ρ2*; σ2*].
where L1 and L2 are disjoint and compatible languages of MSFOPC, Σ is a formula of L1, Δ is a formula of L1 + L2, ρ1* and ρ2* are tuples of predicate symbols from L1 and L2 respectively, σ1* is a tuple of predicate, function and constant symbols from L1, and σ2* is a tuple comprising every predicate, function and constant symbol in L2 not in ρ2*.
10. Theorem 6.6 from [przymusinski1989],
Suppose that P is a stratified program and {S1, ..., Sn} is a stratification of P. A model of P is perfect if and only if it is a model of prioritized circumscription CIRC(P; S1 > ... > Sn).
Example: Difference in parallel and prioritized circumscriptions
The example below shows difference in models of parallel-ly and prioritized-ly circumscribed formulas.
Consider formula F
∀x(P1(A, x) → P2(A, x)) ∧ ∀x,y(P1(x, y) ∧ ¬P2(x, y) → P3(x, y)) ∧ P1(a, b) ∧ P1(b, c) ∧ P1(c, d) ∧ a≠b≠c
Models of CIRC[P; P1, P2, P3]
1. Model 1
- P1 = {(a, b), (b, c), (c, d)}
- P2 = {(a, b)}
- P3 = {(b, c), (c, d)}
2. Model 2
- P1 = {(a, b), (b, c), (c, d)}
- P2 = {(a, b), (b, c)}
- P3 = {(c, d)}
3. Model 2
- P1 = {(a, b), (b, c), (c, d)}
- P2 = {(a, b), (b, c), (c, d)}
- P3 = {}
Instead Models of CIRC[P; P1 > P2 > P3]
Only Model 1 is also a model of CIRC[P; P1 > P2 > P3], because extension of P2 is minimised over that of P3.
1. Model 1
- P1 = {(a, b), (b, c), (c, d)}
- P2 = {(a, b)}
- P3 = {(b, c), (c, d)}
Clark's completion
Clark's completion comp(P) of a program P gives a declarative semantics of logic programs [clark1978]. Clark's completion of P is obtained by rewriting every clause in P of the form q(K1, ..., Kn) ← L1, ..., Lm, as a clause q(T1, ..., Tn) ← ∃x1, ..., xk(T1 = K1 ∧ ... ∧ Tn = Kn ∧ L1 ∧ ... ∧ Lm), where K1, ..., Kn are terms containing variables x1, ..., xk, and then replacing, for every predicate symbol q in the alphabet, the (possibly empty) set of all clauses
- q(K11, ..., Kn1) ← F1
- .
- .
- .
- q(K1s, ..., Kns) ← Fs
with q appearing in the head, by a single universally quantified logical equivalence q(T1, ..., Tn) ↔ (F1 ∨ ... ∨ Fs).
Toy Examples
Tank problem
The tank problem as described in [shanahan1990] involves many tanks discharging liquid into another tank. Each tank has an associated tap which can be turned on or off and which discharges liquid at a given rate. Upto two tanks fill the same tank at any time. The figure shows an example of the two tanks (with tap) case.
Following set of axioms are used for the N tanks problem. We express those axioms in syntax used in the paper and also differentiate fluents from parameters.
Actions Tap-on(N) and Tap-off(N) denote the act of turning tap N on and off respectively. Parameters Filling(V) and Emptying(V) denote the property of rate of filling and emptying of tank V respectively. Parameter Rate(N) denotes the rate at which tap N is discharging liquid. Parameter Level(V) denotes the level of tank V and δ(Level(V)) denotes its first derivative. Parameter Rim(V) denotes the rim of tank valve. (Note that the parameters Filling(V) and Emptying(V) are associated with disjoint tanks.)
1st Approach
Value(Filling(v), 0) = Value(Emptying(v), 0) = Value(δ(Level(v)), 0)) = 0
Value(Level(v1), 0) = L1 etc.
BreaksTo(Tap-on(n), Filling(v2), t, r1+r2) ← connects(n, v1, v2) ∧ r1 = Value(Rate(n), t) ∧ r2 = Value(Filling(v2), t)
BreaksTo(Tap-off(n), Filling(v2), t, r2-r1) ← connects(n, v1, v2) ∧ r1 = Value(Rate(n), t) ∧ r2 = Value(Filling(v2), t)
BreaksTo(Tap-on(n), Emptying(v1), t, r) ← connects(n, v1, v2) ∧ r = Value(Rate(n), t)
BreaksTo(Tap-off(n), Emptying(v1), t, 0) ← connects(n, v1, v2)
Value(δ(Level(v2))) = Value(Filling(v2)) ← connects(n, v1, v2) ∧ Value(Level(v2)) < Value(Rim(v2))
Value(δ(Level(v1))) = -1 × Value(Emptying(v1)) ← connects(n, v1, v2) ∧ Value(Level(v1)) > 0
Breaks(Tap-on(n), δ(Level(v1)), t) ∧ Breaks(Tap-on(n), δ(Level(v2)), t) ∧ Breaks(Tap-off(n), δ(Level(v1)), t) ∧ Breaks(Tap-off(n), δ(Level(v2)), t) ∧ Breaks(Tap-on(n), Level(v1), t) ∧ Breaks(Tap-on(n), Level(v2), t) ∧ Breaks(Tap-off(n), Level(v1), t) ∧ Breaks(Tap-off(n), Level(v2), t) ← connects(n, v1, v2)
However, the above formalization can be used only if taps are turned on and off sequentially, i.e. not concurrently, as also noted in [shanahan1990]. We rework the set of axioms for the two tank problems to allow concurrent actions.
2nd Approach
In this approach we will not differentiate between Filling and Emptying and plainly refer to those notions by change in Level, i.e. δ(Level(v)). Further we introduce new fluents Tap-is-on(n) and Tap-is-off(n) to denote that the taps are on and off.
InitiallyFalse(Tap-is-on(n))
Value(δ(Level(v)), 0) = 0
Initializations of Value(Level(v), 0) for all tanks.
Initiates(Tap-on(n), Tap-is-on(n), t)
Terminates(Tap-off(n), Tap-is-on(n), t)
Value(δ(Level(v2)), t) = Value(Rate(n1), t) + Value(Rate(n2), t) ← connects(n1, v11, v2) ∧ connects(n2, v12, v2) ∧ n1≠n2 ∧ HoldsAt(Tap-is-on(n1), t) ∧ HoldsAt(Tap-is-on(n2), t) ∧ 0 < Value(Level(v2)) < Value(Rim(v2), t) ∧ Value(Level(v11), t) > 0 ∧ Value(Level(v12), t) > 0.
Value(δ(Level(v2)), t) = Value(Rate(n1), t) + Value(Rate(n2), t) ← connects(n1, v11, v2) ∧ connects(n2, v12, v2) ∧ n1≠n2 ∧ HoldsAt(Tap-is-on(n1), t) ∧ HoldsAt(Tap-is-on(n2), t) ∧ 0 < Value(Level(v2)) < Value(Rim(v2), t) ∧ Value(Level(v11), t) > 0 ∧ Value(Level(v12), t) > 0.
Value(δ(Level(v2)), t) = Value(Rate(n1)) ← connects(n1, v11, v2) ∧ connects(n2, v12, v2) ∧ n1≠n2 ∧ HoldsAt(Tap-is-on(n1), t) ∧ ¬ HoldsAt(Tap-is-on(n2), t) ∧ 0 < Value(Level(v2)) < Value(Rim(v2), t) ∧ Value(Level(v11), t) > 0
Value(δ(Level(v2)), t) = Value(Rate(n2), t) ← connects(n1, v11, v2) ∧ connects(n2, v12, v2) ∧ n1≠n2 ∧ ¬HoldsAt(Tap-is-on(n1), t) ∧ HoldsAt(Tap-is-on(n2), t) ∧ 0 < Value(Level(v2)) < Value(Rim(v2), t) ∧ Value(Level(v12), t) > 0
Value(δ(Level(v2)), t) = 0 ← connects(n1, v11, v2) ∧ connects(n2, v12, v2) ∧ n1≠n2 ∧ ¬HoldsAt(Tap-is-on(n1), t) ∧ ¬HoldsAt(Tap-is-on(n2), t)
Value(δ(Level(v1)), t) = -1*Value(Rate(n), t) ← connects(n, v1, v2) ∧ HoldsAt(Tap-is-on(n), t) ∧ Value(Level(v1), t) > 0
Value(δ(Level(v1)), t) = 0 ← connects(n, v1, v2) ∧ ¬HoldsAt(Tap-is-on(n), t)
Breaks(Tap-on(n), δ(Level(v1)), t) ∧ Breaks(Tap-on(n), δ(Level(v2)), t) ∧ Breaks(Tap-off(n), δ(Level(v1)), t) ∧ Breaks(Tap-off(n), δ(Level(v2)), t) ∧ Breaks(Tap-on(n), Level(v1), t) ∧ Breaks(Tap-on(n), Level(v2), t) ∧ Breaks(Tap-off(n), Level(v1), t) ∧ Breaks(Tap-off(n), Level(v2), t) ← connects(n, v1, v2)
If we were to extend the above description to the three tanks problem, i.e. pipes from three tanks could fill up any container, we would have to rewrite the axioms above and also the size of description would increase exponentially, as there would be 23 possible on and off-states instead of 22.
3nd Approach
We will use the same set of fluents and parameters as in the last approach.
InitiallyFalse(Tap-is-on(n))
Value(δ(Level(v)), 0) = 0
Initializations of Value(Level(v), 0), for all tanks.
Initiates(Tap-on(n), Tap-is-on(n), t)
Terminates(Tap-off(n), Tap-is-on(n), t)
PartValue(δ(Level(v2)), t, ..., Value(Rate(n)) ← HoldsAt(Tap-is-on(n1), t) ∧ connects(n1, v1, v2) ∧ 0 < Value(Level(v2)) < Value(Rim(v2), t) ∧ Value(Level(v1), t) > 0 .
¬∃r.PartValue(δ(Level(v)), t, ..., r) → Value(δ(Level(v)), t) = 0
Value(δ(Level(v1)), t) = Value(Rate(n), t) ← connects(n, v1, v2) ∧ HoldsAt(Tap-is-on(n), t) ∧ Value(Level(v1), t) > 0
Value(δ(Level(v1)), t) = 0 ← connects(n, v1, v2) ∧ ¬HoldsAt(Tap-is-on(n), t)
Breaks(Tap-on(n), δ(Level(v1)), t) ∧ Breaks(Tap-on(n), δ(Level(v2)), t) ∧ Breaks(Tap-off(n), δ(Level(v1)), t) ∧ Breaks(Tap-off(n), δ(Level(v2)), t) ∧ Breaks(Tap-on(n), Level(v1), t) ∧ Breaks(Tap-on(n), Level(v2), t) ∧ Breaks(Tap-off(n), Level(v1), t) ∧ Breaks(Tap-off(n), Level(v2), t) ← connects(n, v1, v2)
Multiple Blocks Problem
References
The references may be found here.
Notes
- ↑ Here is a link to the submitted version.
- ↑ Parameters have (some) similarities with functional fluents in Situation Calculus
- ↑ BreaksPartBy is used to express relative discontinuous change. We have introduced a new predicate BreaksPartTo to express non-relative discontinuous change. Please see tech report for details.
- ↑ An arbitrary finite upper limit may be set on n in the implementation.
- ↑ Sum of an empty multiset may be assumed to be zero but Value(p, t) may not be zero every time no component value (r, in PartValue(p, t, ..., r)) is specified.
- ↑ Any block is connected to itself
- ↑ One of the reasons for getting consistent but physically impossible solutions could be lack of enough constraints.
- ↑ We feel confident of proving conjectures 1 and 2, but less so for 3.
- ↑ A in CECA indicates use of aggregates in the axioms
- ↑ Axioms (B11) -- (B17) contain some constraints in the consequence which must be separated and put in Rem(DM)
- ↑ Comp(F) is similar in notion to Clark's completion of programs [clark1978], hence the name.
- ↑ UNA[Ω] = UNA[g1, ..., gk], where &Omega = {g1, ..., gk}
- ↑ Note similarity with definitions of stratified (and hierarchical) programs [przymusinski1989]
- ↑ Value(Acc(b)) = Value(δ(Vel(b))) will require individual summations to be same!
- ↑ http://xsb.sourceforge.net/
- ↑ Formula μ(Δ(x)) may contain existentially quantified variables.
- ↑ Individual action occurrences are often referred to as "events", so that "actions" are "event types".
