Basic Types of Event Calculus : 

deductive tasks:

“what happens when” and “what actions do” are given and “what’s true when” is required.

Deductive tasks include temporal projection or prediction, where the outcome of a known sequence of actions is sought.

abductive tasks: 

“what actions do” and “what’s true when” are supplied, and “what happens when” is required. In other words, a sequence of actions is sought that leads to a given outcome. Examples of such tasks include temporal explanation or postdiction, certain kinds of diagnosis, and planning.

inductive tasks:

“what’s true when” and “what happens when” are supplied, but “what actions do” is required. In this case, we’re seeking a set of general rules, a theory of the effects of actions, that accounts for observed data. Inductive tasks include certain kinds of learning, scientific discovery, and theory formation.

Event Calculus is key to solving The Egg Cracking Problem.
For More information see Commonsense Reasoning by Erik Mueller!

Event calculus

From Wikipedia, the free encyclopedia

Jump to navigationJump to search

The event calculus is a logical language for representing and reasoning about events and their effects first presented by Robert Kowalski and Marek Sergot in 1986.[1] It was extended by Murray Shanahan and Rob Miller in the 1990s.[2] Similar to other languages for reasoning about change, the event calculus represents the effects of actions on fluents. However, events can also be external to the system. In the event calculus, one can specify the value of fluents at some given time points, the events that take place at given time points, and their effects.

Fluents and events

In the event calculus, fluents are reified. This means that they are not formalized by means of predicates but by means of functions. A separate predicate HoldsAt is used to tell which fluents hold at a given time point. For example, {\displaystyle {\mathit {HoldsAt}}(on(box,table),t)}{\displaystyle {\mathit {HoldsAt}}(on(box,table),t)} means that the box is on the table at time t; in this formula, HoldsAt is a predicate while on is a function.

Events are also represented as terms. The effects of events are given using the predicates Initiates and Terminates. In particular, {\displaystyle {\mathit {Initiates}}(e,f,t)}{\displaystyle {\mathit {Initiates}}(e,f,t)} means that, if the event represented by the term e is executed at time t, then the fluent f will be true after t. The Terminates predicate has a similar meaning, with the only difference being that f will be false and not true after t.

Domain-independent axioms

Like other languages for representing actions, the event calculus formalizes the correct evolution of the fluent via formulae telling the value of each fluent after an arbitrary action has been performed. The event calculus solves the frame problem in a way that is similar to the successor state axioms of the situation calculus: a fluent is true at time t if and only if it has been made true in the past and has not been made false in the meantime.

{\displaystyle {\mathit {HoldsAt}}(f,t)\leftarrow [{\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})\wedge (t_{1}<t)\wedge \neg {\mathit {Clipped}}(t_{1},f,t)]}{\displaystyle {\mathit {HoldsAt}}(f,t)\leftarrow [{\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})\wedge (t_{1}<t)\wedge \neg {\mathit {Clipped}}(t_{1},f,t)]}

This formula means that the fluent represented by the term f is true at time t if:

  1. an event e has taken place: {\displaystyle {\mathit {Happens}}(e,t_{1})}{\displaystyle {\mathit {Happens}}(e,t_{1})};
  2. this took place in the past: {\displaystyle {\mathit {t}}_{1}<t}{\displaystyle {\mathit {t}}_{1}<t};
  3. this event has the fluent f as an effect: {\displaystyle {\mathit {Initiates}}(e,f,t_{1})}{\displaystyle {\mathit {Initiates}}(e,f,t_{1})};
  4. the fluent has not been made false in the meantime: {\displaystyle {\mathit {Clipped}}(t_{1},f,t)}{\displaystyle {\mathit {Clipped}}(t_{1},f,t)}

A similar formula is used to formalize the opposite case in which a fluent is false at a given time. Other formulae are also needed for correctly formalizing fluents before they have been effects of an event. These formulae are similar to the above, but {\displaystyle {\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})}{\displaystyle {\mathit {Happens}}(e,t_{1})\wedge {\mathit {Initiates}}(e,f,t_{1})} is replaced by {\displaystyle {\mathit {HoldsAt}}(f,t_{1})}{\displaystyle {\mathit {HoldsAt}}(f,t_{1})}.

The Clipped predicate, stating that a fluent has been made false during an interval, can be axiomatized, or simply taken as a shorthand, as follows:

{\displaystyle {\mathit {Clipped}}(t_{1},f,t_{2})\equiv \exists e,t[{\mathit {Happens}}(e,t)\wedge (t_{1}\leq t<t_{2})\wedge {\mathit {Terminates}}(e,f,t)]}{\displaystyle {\mathit {Clipped}}(t_{1},f,t_{2})\equiv \exists e,t[{\mathit {Happens}}(e,t)\wedge (t_{1}\leq t<t_{2})\wedge {\mathit {Terminates}}(e,f,t)]}

Domain-dependent axioms

The axioms above relate the value of the predicates HoldsAt, Initiates and Terminates, but do not specify which fluents are known to be true and which events actually make fluents true or false. This is done by using a set of domain-dependent axioms. The known values of fluents are stated as simple literals {\displaystyle {\mathit {HoldsAt}}(f,t)}{\displaystyle {\mathit {HoldsAt}}(f,t)}. The effects of events are stated by formulae relating the effects of events with their preconditions. For example, if the event open makes the fluent isopen true, but only if haskey is currently true, the corresponding formula in the event calculus is:

{\displaystyle {\mathit {Initiates}}(e,f,t)\equiv [e=open\wedge f=isopen\wedge {\mathit {HoldsAt}}(haskey,t)]\vee \cdots }{\displaystyle {\mathit {Initiates}}(e,f,t)\equiv [e=open\wedge f=isopen\wedge {\mathit {HoldsAt}}(haskey,t)]\vee \cdots }

The right-hand expression of this equivalence is composed of a disjunction: for each event and fluent that can be made true by the event, there is a disjunct saying that e is actually that event, that f is actually that fluent, and that the precondition of the event is met.

The formula above specifies the truth value of {\displaystyle {\mathit {Initiates}}(e,f,t)}{\displaystyle {\mathit {Initiates}}(e,f,t)} for every possible event and fluent. As a result, all effects of all events have to be combined in a single formulae. This is a problem, because the addition of a new event requires modifying an existing formula rather than adding new ones. This problem can be solved by the application of circumscription to a set of formulae each specifying one effect of one event:

{\displaystyle {\mathit {Initiates}}(open,isopen,t)\leftarrow {\mathit {HoldsAt}}(haskey,t)}{\displaystyle {\mathit {Initiates}}(open,isopen,t)\leftarrow {\mathit {HoldsAt}}(haskey,t)}
{\displaystyle {\mathit {Initiates}}(break,isopen,t)\leftarrow {\mathit {HoldsAt}}(hashammer,t)}{\displaystyle {\mathit {Initiates}}(break,isopen,t)\leftarrow {\mathit {HoldsAt}}(hashammer,t)}
{\displaystyle {\mathit {Initiates}}(break,broken,t)\leftarrow {\mathit {HoldsAt}}(hashammer,t)}{\displaystyle {\mathit {Initiates}}(break,broken,t)\leftarrow {\mathit {HoldsAt}}(hashammer,t)}

These formulae are simpler than the formula above, because each effect of each event can be specified separately. The single formula telling which events e and fluents f make {\displaystyle {\mathit {Initiates}}(e,f,t)}{\displaystyle {\mathit {Initiates}}(e,f,t)} true has been replaced by a set of smaller formulae, each one telling the effect of an event on a fluent.

However, these formulae are not equivalent to the formula above. Indeed, they only specify sufficient conditions for {\displaystyle {\mathit {Initiates}}(e,f,t)}{\displaystyle {\mathit {Initiates}}(e,f,t)} to be true, which should be completed by the fact that Initiates is false in all other cases. This fact can be formalized by simply circumscribing the predicate Initiates in the formula above. It is important to note that this circumscription is done only on the formulae specifying Initiates and not on the domain-independent axioms. The predicate Terminates can be specified in the same way Initiates is.

A similar approach can be taken for the Happens predicate. The evaluation of this predicate can be enforced by formulae specifying not only when it is true and when it is false:

{\displaystyle {\mathit {Happens}}(e,t)\equiv (e=open\wedge t=0)\vee (e=exit\wedge t=1)\vee \cdots }{\displaystyle {\mathit {Happens}}(e,t)\equiv (e=open\wedge t=0)\vee (e=exit\wedge t=1)\vee \cdots }

Circumscription can simplify this specification, as only necessary conditions can be specified:

{\displaystyle {\mathit {Happens}}(open,0)}{\displaystyle {\mathit {Happens}}(open,0)}
{\displaystyle {\mathit {Happens}}(exit,1)}{\displaystyle {\mathit {Happens}}(exit,1)}

Circumscribing the predicate Happens, this predicate will be false at all points in which it is not explicitly specified to be true. This circumscription has to be done separately from the circumscription of the other formulae. In other words, if F is the set of formulae of the kind {\displaystyle {\mathit {Initiates}}(e,f,t)\leftarrow \cdots }{\displaystyle {\mathit {Initiates}}(e,f,t)\leftarrow \cdots }, G is the set of formulae {\displaystyle {\mathit {Happens}}(e,t)}{\displaystyle {\mathit {Happens}}(e,t)}, and H are the domain independent axioms, the correct formulation of the domain is:

{\displaystyle {\mathit {Circ}}(F;{\mathit {Initiates}},{\mathit {Terminates}})\wedge Circ(G;Happens)\wedge H}{\displaystyle {\mathit {Circ}}(F;{\mathit {Initiates}},{\mathit {Terminates}})\wedge Circ(G;Happens)\wedge H}

The event calculus as a logic program

The event calculus was originally formulated as a set of Horn clauses augmented with negation as failure and could be run as a Prolog program. In fact, circumscription is one of the several semantics that can be given to negation as failure, and is closely related to the completion semantics (in which "if" is interpreted as "if and only if" — see logic programming).

Extensions and applications

The original event calculus paper of Kowalski and Sergot focused on applications to database updates and narratives.[3] Extensions of the event calculus can also formalize non-deterministic actions, concurrent actions, actions with delayed effects, gradual changes, actions with duration, continuous change, and non-inertial fluents.

Kave Eshghi showed how the event calculus can be used for planning,[4] using abduction to generate hypothetical events in abductive logic programming. Van Lambalgen and Hamm showed how the event calculus can also be used to give an algorithmic semantics to tense and aspect in natural language[5] using constraint logic programming.

Other notable extensions of the Event Calculus include probabilistic dialects. For instance, Artikis et al. introduced Markov Logic Networks-based[6] and probabilistic[7] variants of the EC.

Reasoning tools

In addition to Prolog and its variants, several other tools for reasoning using the event calculus are also available:

See also

Chapter 17 - Event Calculus  Erik T. Mueller

17.1 Introduction

The event calculus [45, 66, 74, 98, 100] is a formalism for reasoning about action and change. Like the situation calculus, the event calculus has actions, which are called events, and time-varying properties or fluents. In the situation calculus, performing an action in a situation gives rise to a successor situation. Situation calculus actions are hypothetical, and time is tree-like. In the event calculus, there is a single time line on which actual events occur.

narrative is a possibly incomplete specification of a set of actual event occurrences [63, 98]. The event calculus is narrative-based, unlike the standard situation calculus in which an exact sequence of hypothetical actions is represented.

Like the situation calculus, the event calculus supports context-sensitive effects of events, indirect effects, action preconditions, and the commonsense law of inertia. Certain phenomena are addressed more naturally in the event calculus, including concurrent events, continuous time, continuous change, events with duration, nondeterministic effects, partially ordered events, and triggered events.

We use a simple example to illustrate what the event calculus does. Suppose we wish to reason about turning on and off a light. We start by representing general knowledge about the effects of events:

If a light’s switch is flipped up, then the light will be on.

If a light’s switch is flipped down, then the light will be off.

We then represent a specific scenario:

The light was off at time 0.

Then the light’s switch was flipped up at time 5.

Then the light’s switch was flipped down at time 8.

We use the event calculus to conclude the following:

At time 3, the light was off.

At time 7, the light was on.

At time 10, the light was off.

Table 17.1. Original event calculus (OEC) predicates and functions (e,e1,e2 = event occurrences, f,f1,f= fluents, p = time period)

Predicate/function

Meaning

Holds(p)

p holds

Start(p,e)

e starts p

End(p,e)

e ends p

Initiates(e,f)

e initiates f

Terminates(e,f)

e terminates f

e1 < e2

e1 precedes e2

Broken(e1,f,e2)

f is broken between e1 and e2

Incompatible(f1,f2)

f1 and f2 are incompatible

After(e,f)

time period after e in which f holds

Before(e,f)

time period before e in which f holds

In this chapter, we discuss several versions of the event calculus, the use of circumscription in the event calculus, methods of knowledge representation using the event calculus, automated event calculus reasoning, and applications of the event calculus. We use languages of classical many-sorted predicate logic with equality.

17.2 Versions of the Event Calculus

The event calculus has evolved considerably from its original version. In this section, we trace the development of the event calculus and present its important versions.

17.2.1 Original Event Calculus (OEC)

The original event calculus (OEC) was introduced in 1986 by Kowalski and Sergot [45]. OEC has sorts for event occurrences, fluents, and time periods. The predicates and functions of the original event calculus are shown in Table 17.1. The axioms of the original event calculus are as follows.

OEC1. Initiates(e,f) ≡ Holds(After(e,f)).

OEC2. Terminates(e,f) ≡ Holds(Before(e,f)).

OEC3. Start(After(e,f),e).

OEC4. End(Before(e,f),e).

OEC5. After(e1,f) = Before(e2,f) ⊃ Start(Before(e2,f),e1).

OEC6. After(e1,f) = Before(e2,f) ⊃ End(After(e1,f),e2).

OEC7. Holds(After(e1,f)) ∧ Holds(Before(e2,f)) ∧ e< e∧ ¬Broken(e1, f,e2) ⊃ After(e1,f) = Before(e2,f).

OEC8. Broken(e1,f,e2) ≡ ∃e,f

% style="font-size: 11pt; font-variant: normal; white-space: pre-wrap; font-family: "Times New Roman"; color: rgb(0, 0, 0); font-weight: 400; font-style: italic; text-decoration: none" %)Holds(After(e,f1))∨Holds(Before(e,f1)))∧ Incompatible(f,f1) ∧ e< e < e2).

Let OEC be the conjunction of OEC1 through OEC8.

Example 17.1. Consider the example of turning on and off a light. We have an event occurrence E1, which precedes event occurrence E2:

E< E(17.1)

Eturns on the light and Eturns it off:

Initiates(e,f) ≡ (e = E∧ f = On) ∨ (e = E∧ f = Off) (17.2)

Terminates(e,f) ≡ (e = E∧ f = Off) ∨ (e = E∧ f = On) (17.3)

The light cannot be both on and off:

Incompatible(f1,f2) ≡ (fOn ∧ fOff) ∨ (fOff ∧ fOn)

(17.4) We also assume the following:

E= E2

(17.5)

On Off

(17.6)

¬(e < e)

(17.7)

We can then prove that the time period after Ein which the light is on equals the time period before Ein which the light is on. Let Σ be the conjunction of (17.1) through (17.7).

Proposition 17.1. Σ ∧ OEC |= After(E1,On) = Before(E2,On).

Proof. From (17.2), (17.3), OEC1, and OEC2, we have

Holds(After(e,f)) ≡ (e = E∧ f = On) ∨ (e = E∧ f = Off) (17.8)

Holds(Before(e,f)) ≡ (e = E∧ f = Off) ∨ (e = E∧ f = On) (17.9)

From (17.8), (17.9), (17.4), (17.6), (17.7), and OEC8, we get ¬Broken(E1,On,E2). From this, Holds(After(E1,On) (which follows from (17.8)), Holds(Before(E2,On) (which follows from (17.9)), (17.1), and OEC7, we have After(E1,On) = Before(E2,

On).

We can also prove that Estarts the time period before Ein which On holds and that Eends the time period after Ein which On holds.

Proposition 17.2. Σ∧OEC |= Start(Before(E2,On),E1)∧End(After(E1,On),E2).

Table 17.2. Simplified event calculus (SEC) predicates (e = event, f = fluent, t,t1,t= timepoints)

Predicate

Meaning

Initially(f)

f is true at timepoint 0

HoldsAt(f,t)

f is true at t

Happens(e,t)

e occurs at t

Initiates(e,f,t)

if e occurs at t, then f is true after t

Terminates(e,f,t)

if e occurs at t, then f is false after t

StoppedIn(t1,f,t2)

f is stopped between t1 and t2

Proof. This follows from Proposition 17.1, OEC5, and OEC6.

Pinto and Reiter [82] argue that the Holds predicate of the original event calculus is problematic, because it represents that “time periods hold”. They point out some undesirable consequences of axioms OEC3 and OEC4. In our light example, Start(After(E1,Off),E1) follows from OEC3. But what is the time period After(E1,Off)? Whatever it is, it does not hold. From (17.5), (17.6), and (17.8), we have ¬Holds(After(E1,Off)). Similarly, from OEC3, we get Start(After(E2,On),E2) and from OEC4, we get End(Before(E2,Off),E2). Sadri and Kowalski [88] suggest modifying OEC3 to Holds(After(e,f)) ⊃ Start(After(e,f),e) and OEC4 to Holds(Before(e,f)) ⊃ End(Before(e,f),e).

17.2.2 Simplified Event Calculus (SEC)

The simplified event calculus (SEC) was proposed in 1986 by Kowalski [40, p. 25] (see also [41]) and developed by Sadri [87, pp. 137–139], Eshghi [17], and Shanahan [93, 94, 98]. It differs from the original event calculus in the following ways: • It replaces time periods with timepoints, which are either nonnegative integers or nonnegative real numbers.

  • It replaces event occurrences or tokens with event types. The predicate Happens(e,t) represents that event (type) e occurs at timepoint t.
  • It eliminates the notion of incompatible fluents.
  • It adds a predicate Initially(f), which represents that fluent f is initially true [95, p. 254] (see also [12] and [98, p. 253]).

The predicates of the simplified event calculus are shown in Table 17.2. The axioms of the simplified event calculus are as follows.

SEC1. 

% style="font-size: 11pt; font-variant: normal; white-space: pre-wrap; font-family: "Times New Roman"; color: rgb(0, 0, 0); font-weight: 400; font-style: italic; text-decoration: none" %)Initially(f) ∧ ¬StoppedIn(0,f,t)) ∨ ∃e,t(Happens(e,t1) ∧ Initiates(e,f,t1) ∧ t< t ∧ ¬StoppedIn(t1,f,t))) ≡ HoldsAt(f,t).

SEC2. StoppedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t

Terminates(e,f,t)).

Let SEC be the conjunction of SEC1 and SEC2.

SEC1 represents that (1) a fluent that is initially true remains true until it is terminated, and (2) a fluent that is initiated remains true until it is terminated. Thus fluents are subject to the commonsense law of inertia [48, 49, 98], which states that a fluent’s truth value persists unless the fluent is affected by an event.

Example 17.2. Consider again the example of turning on and off a light. If a light is turned on, it will be on, and if a light is turned off, it will no longer be on:

Initiates(e,f,t) ≡ (e = TurnOn ∧ f = On) (17.10)

Terminates(e,f,t) ≡ (e = TurnOff ∧ f = On) (17.11)

Initially, the light is off:

¬Initially(On) (17.12)

The light is turned on at timepoint 2 and turned off at timepoint 4:

Happens(e,t) ≡ (e = TurnOn ∧ t = 2) ∨ (e = TurnOff ∧ t = 4) (17.13)

We further assume the following:

TurnOn TurnOff (17.14)

We can then show that the light will be off at timepoint 1, on at timepoint 3, and off again at timepoint 5. Let Σ be the conjunction of (17.10) through (17.14).

Proposition 17.3. Σ ∧ SEC |= ¬HoldsAt(On,1).

Proof. From (17.13), we have ¬∃e,t(Happens(e,t1)∧Initiates(e,On,t1)∧t< 1∧ ¬StoppedIn(t1,On,1)). From this, (17.12), and SEC1, we have ¬HoldsAt(On,1).  Proposition 17.4. Σ ∧ SEC |= HoldsAt(On,3).

Proof. From (17.13) and SEC2, we have ¬StoppedIn(2,On,3). From this, Happens(TurnOn,2) (which follows from (17.13)), Initiates(TurnOn,On,2) (which follows from (17.10)), 2 < 3, and SEC1, we have HoldsAt(On,3).  Proposition 17.5. Σ ∧ SEC |= ¬HoldsAt(On,5).

Proof. From Happens(TurnOff,4) (which follows from (17.13)), 2 < 4 < 5, Terminates(TurnOff,On,4) (which follows from (17.11)), and SEC2, we have StoppedIn(2,On,5)). From this, (17.13), and (17.10), we have ¬∃e,t(Happens(e,t1) ∧Initiates(e,On,t1)∧t< 5∧¬StoppedIn(t1,On,5)). From this, (17.12), and SEC1, we have ¬HoldsAt(On,5).

Table 17.3. Basic event calculus (BEC) predicates (e = event, f,f1,f= fluents, t,t1,t= timepoints)

Predicate

Meaning

InitiallyN(f)

f is false at timepoint 0

InitiallyP(f)

f is true at timepoint 0

HoldsAt(f,t)

f is true at t

Happens(e,t)

e occurs at t

Initiates(e,f,t)

if e occurs at t, then f is true and not

released from the commonsense law

of inertia after t

Terminates(e,f,t)

if e occurs at t, then f is false and not

released from the commonsense law

of inertia after t

Releases(e,f,t)

if e occurs at t, then f is released from the commonsense law of inertia after t

StoppedIn(t1,f,t2)

f is stopped between t1 and t2

StartedIn(t1,f,t2)

f is started between t1 and t2

Trajectory(f1,t1,f2,t2)

if f1 is initiated by an event that occurs at t1, then f2 is true at t1 + t2

17.2.3 Basic Event Calculus (BEC)

Shanahan [94–96, 98] extended the simplified event calculus by allowing fluents to be released from the commonsense law of inertia via the Releases predicate, and adding the ability to represent continuous change via the Trajectory predicate. The Initially predicate is broken into two predicates InitiallyP and InitiallyN. We call this version of the event calculus the basic event calculus (BEC).

Releases(e,f,t) represents that, if event e occurs at timepoint t, then fluent f will be released from the commonsense law of inertia after t. In SEC, a fluent that is initiated remains true until it is terminated, and a fluent that is terminated remains false until it is initiated. In BEC, a fluent that is initiated remains true until it is terminated or released, and a fluent that is terminated remains false until it is initiated or released. After a fluent is released, its truth value is not determined by BEC and is permitted to vary. Thus there are models in which the fluent is true, and models in which the fluent is false.

This opens up several possibilities. First, releasing a fluent frees it up so that other axioms in the domain description can be used to determine its truth value. This allows us to represent continuous change using Trajectory, as discussed in Section 17.5.7, and indirect effects, as discussed in Section 17.5.9. Second, released fluents can be used to represent nondeterministic effects of events, as discussed in Section 17.5.8.

Trajectory(f1,t1,f2,t2) represents that, if fluent fis initiated by an event that occurs at timepoint t1, then fluent fwill be true at timepoint t+ t2. This can be used to represent fluents that change as a function of time. The domain description is usually written so that the fluent fis released by the events that initiate f1.

The predicates of the basic event calculus are shown in Table 17.3. The axioms of the basic event calculus are as follows.

BEC1. StoppedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t∧ (Terminates(e,f,t) ∨ Releases(e,f,t))).

BEC2. StartedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t)∧t< t < t2∧(Initiates(e,f,t) ∨ Releases(e,f,t))).

BEC3. Happens(e,t1) ∧ Initiates(e,f1,t1) ∧ 0 < t∧ Trajectory(f1,t1,f2,t2) ∧ ¬StoppedIn(t1,f1,t+ t2) ⊃ HoldsAt(f2,t+ t2).

BEC4. InitiallyP(f) ∧ ¬StoppedIn(0,f,t) ⊃ HoldsAt(f,t).

BEC5. InitiallyN(f) ∧ ¬StartedIn(0,f,t) ⊃ ¬HoldsAt(f,t).

BEC6. Happens(e,t1) ∧ Initiates(e,f,t1) ∧ t< t∧ ¬StoppedIn(t1,f,t2) ⊃ HoldsAt(f,t2).

BEC7. Happens(e,t1) ∧ Terminates(e,f,t1) ∧ t< t∧ ¬StartedIn(t1,f,t2) ⊃ ¬HoldsAt(f,t2).

Let BEC be the conjunction of BEC1 through BEC7.

Example 17.3. Consider once again the example of turning on and off a light. We replace (17.12) with the following:

InitiallyN(On) We add the following:

(17.15)

¬Releases(e,f,t)

(17.16)

Let Σ be the conjunction of (17.10), (17.11), (17.13), (17.14), (17.15), and (17.16). We then have the same results as for SEC.

Proposition 17.6. Σ ∧ BEC |= ¬HoldsAt(On,1).

Proof. From (17.13) and BEC2, we have ¬StartedIn(0,On,1). From this, (17.15), and BEC5, we have ¬HoldsAt(On,1).

Proposition 17.7. Σ ∧ BEC |= HoldsAt(On,3).

Proof. From (17.13) and BEC1, we have ¬StoppedIn(2,On,3). From this, Happens(TurnOn,2) (which follows from (17.13)), Initiates(TurnOn,On,2) (which follows from (17.10)), 2 < 3, and BEC6, we have HoldsAt(On,3).  Proposition 17.8. Σ ∧ BEC |= ¬HoldsAt(On,5).

Proof. From (17.13) and BEC2, we have ¬StartedIn(4,On,5). From this, Happens(TurnOff,4) (which follows from (17.13)), Terminates(TurnOff,On,4) (which follows from (17.11)), 4 < 5, and BEC7, we have ¬HoldsAt(On,5). 

Example 17.4. We can use Releases and Trajectory to represent a light that alternately emits red and green when it is turned on. If a light is turned on, it will be on:

Initiates(e,f,t) ≡ (e = TurnOn ∧ f = On) (17.17)

If a light is turned on, whether it is red or green will be released from the commonsense law of inertia:

Releases(e,f,t) ≡ (e = TurnOn ∧ (f = Red ∨ f = Green)) (17.18)

If a light is turned off, it will not be on, red, or green:

Terminates(e,f,t) ≡ (e = TurnOff ∧ (f = On ∨ f = Red ∨ f = Green))

(17.19)

After a light is turned on, it will alternately emit red for two seconds and green for two seconds:

(tmod 4) < 2 ⊃ Trajectory(On,t1,Red,t2) (17.20) https://lh6.googleusercontent.com/nsG_raAArEpiIorOCRBOwIjym7KMGh5F0ejR1rgaf59KwH5qqYhBBtdFS_ND_lqJgRRtE8upBGbg-aE3se47G0FeqlEeOgPCPDvNKLFk3Z77ZXGzorOmCTOokCMCxNzdTWpO3C0Trajectory(On,t1,Green,t2) (17.21)

The light is not simultaneously red and green:

 

¬HoldsAt(Red,t) ∨ ¬HoldsAt(Green,t)

The light is turned on at timepoint 2:

(17.22)

Happens(e,t) ≡ (e = TurnOn ∧ t = 2)

We also assume

(17.23)

TurnOn TurnOff

(17.24)

We can then show that the light will be red at timepoint 3, green at timepoint 5, red at timepoint 7, and so on. Let Σ be the conjunction of (17.17) through (17.24).

Proposition 17.9. Σ ∧ BEC |= HoldsAt(Red,3).

Proof. From (17.20) by universal instantiation, we have

Trajectory(On,2,Red,1) (17.25)

From (17.23) and BEC1, we have ¬StoppedIn(2,On,3). From this, Happens(TurnOn, 2) (which follows from (17.23)), Initiates(TurnOn,On,2) (which follows from (17.17)), 0 < 1, (17.25), and BEC3, we have HoldsAt(Red,3). 

Proposition 17.10. Σ ∧ BEC |= HoldsAt(Green,5).

Proof. From (17.21) by universal instantiation, we have

Trajectory(On,2,Green,3) (17.26)

From (17.23) and BEC1, we have ¬StoppedIn(2,On,5). From this, Happens(TurnOn, 2) (which follows from (17.23)), Initiates(TurnOn,On,2) (which follows from (17.17)), 0 < 3, (17.26), and BEC3, we have HoldsAt(Green,5). 

Proposition 17.11. Σ ∧ BEC |= HoldsAt(Red,7).

Table 17.4. EC and DEC predicates (= event, f,f1,f= fluents, t,t1,t= timepoints)

Predicate

Meaning

HoldsAt(f,t)

f is true at t

Happens(e,t)

e occurs at t

ReleasedAt(f,t)

f is released from the commonsense law of inertia at t

Initiates(e,f,t)

if e occurs at t, then f is true and not

released from the commonsense law

of inertia after t

Terminates(e,f,t)

if e occurs at t, then f is false and not

released from the commonsense law

of inertia after t

Releases(e,f,t)

if e occurs at t, then f is released from the commonsense law of inertia after t

Trajectory(f1,t1,f2,t2)

if f1 is initiated by an event that

AntiTrajectory(f1,t1,f2,t2)

occurs at t1, then f2 is true at t1 + t2 if f1 is terminated by an event that occurs at t1, then f2 is true at t1 + t2

Proof. From (17.20) by universal instantiation, we have

Trajectory(On,2,Red,5) (17.27)

From (17.23) and BEC1, we have ¬StoppedIn(2,On,7). From this, Happens(TurnOn, 2) (which follows from (17.23)), Initiates(TurnOn,On,2) (which follows from (17.17)), 0 < 5, (17.27), and BEC3, we have HoldsAt(Red,7). 

17.2.4 Event Calculus (EC)

Miller and Shanahan [65, 66] introduced several alternative formulations of the basic event calculus. A number of their axioms can be combined [70] to produce what we call EC, which differs from the basic event calculus in the following ways:

  • It allows negative time. Timepoints are either integers or real numbers.
  • It eliminates the InitiallyN and InitiallyP predicates. • It explicitly represents that a fluent is released from the commonsense law of inertia using the ReleasedAt predicate.
  • It adds AntiTrajectory.
  • It treats StoppedIn and StartedIn as abbreviations rather than predicates, and introduces other abbreviations.

ReleasedAt(f,t) represents that fluent f is released from the commonsense law of inertia at timepoint t. AntiTrajectory(f1,t1,f2,t2) represents that, if fluent fis terminated by an event that occurs at timepoint t1, then fluent fwill be true at timepoint t+ t2.

The predicates of EC are shown in Table 17.4. The axioms and definitions of EC are as follows.

def

EC1. Clipped(t1,f,t2) ≡ ∃e,t (Happens(e,t) Terminates(e,f,t)).https://lh5.googleusercontent.com/JjVvWXJq5udqTEF0krK-Se4wwOu7XkkJGaAL3H-QqyLgZo-6_GrjlbG6Co71jZdIxXJ2RVqFDKhKbB_jKrmffQGao59ekBeElq0LFKQ1v7imrMcrzBIubFvHEk3ID9Wr4y0Igrc

def

EC2. Declipped(t1,f,t2) ≡ ∃e,t (Happens(e,t)https://lh6.googleusercontent.com/pjXbOCRnlbmB3Cs7zIih56KAzdMb43DjWrb_IMThlSp3_Rt1k18J_w8AqCRdfcR71bsXpTdee5vvK3fm5v2FuH-j7Hlny6ZRDaVtu3lXVOsmoosPajss4IG_yWjKar8EPXt_l7g

Initiates(e,f,t)).

def

EC3. StoppedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t

Terminates(e,f,t)).

def

EC4. StartedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t

Initiates(e,f,t)).

EC5. Happens(e,t1) ∧ Initiates(e,f1,t1) ∧ 0 < t∧ Trajectory(f1,t1,f2,t2) ∧ ¬StoppedIn(t1,f1,t+ t2) ⊃ HoldsAt(f2,t+ t2).

EC6. Happens(e,t1) ∧ Terminates(e,f1,t1) ∧ 0 < t∧ AntiTrajectory(f1,t1, f2,t2) ∧ ¬StartedIn(t1,f1,t+ t2) ⊃ HoldsAt(f2,t+ t2).

def

EC7. PersistsBetween(t1,f,t2) ≡ ¬∃t (ReleasedAt(f,t) .https://lh6.googleusercontent.com/meb7GdNonlCdKE_kbt6povMtKjOmKkzm2f8oMBO7tTYMD5n34PD7IF9ytKDtTuR8nu5snCpld7wExPH_kloHStkyjHPiUjTa05b55TaDoaF5hWaqCM28WS9Z9ieKXEB4AwJjYdg

def

EC8. ReleasedBetween(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t t < t

Releases(e,f,t)).

EC9. HoldsAt(f,t1) ∧ t< t∧ PersistsBetween(t1,f,t2) ∧ ¬Clipped(t1,f,t2) ⊃ HoldsAt(f,t2).

EC10. ¬HoldsAt(f,t1) ∧ t< t∧ PersistsBetween(t1,f,t2) ∧ ¬Declipped(t1,f,t2) ⊃ ¬HoldsAt(f,t2).

EC11. ReleasedAt(f,t1)∧t< t∧¬Clipped(t1,f,t2)∧¬Declipped(t1,f,t2) ⊃ ReleasedAt(f,t2).

EC12. ¬ReleasedAt(f,t1) ∧ t< t∧ ¬ReleasedBetween(t1,f,t2) ⊃ ¬ReleasedAt(f,t2).

def

EC13. ReleasedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t

Releases(e,f,t)).

EC14. Happens(e,t1) ∧ Initiates(e,f,t1) ∧ t< t∧ ¬StoppedIn(t1,f,t2) ∧ ¬ReleasedIn(t1,f,t2) ⊃ HoldsAt(f,t2).

EC15. Happens(e,t1) ∧ Terminates(e,f,t1) ∧ t< t∧ ¬StartedIn(t1,f,t2) ∧ ¬ReleasedIn(t1,f,t2) ⊃ ¬HoldsAt(f,t2).

EC16. Happens(e,t1) ∧ Releases(e,f,t1) ∧ t< t∧ ¬StoppedIn(t1,f,t2) ∧ ¬StartedIn(t1,f,t2) ⊃ ReleasedAt(f,t2).

EC17. Happens(e,t1) ∧ (Initiates(e,f,t1) ∨ Terminates(e,f,t1)) ∧ t< t∧ ¬ReleasedIn(t1,f,t2) ⊃ ¬ReleasedAt(f,t2).

Let EC be the formula generated by conjoining axioms EC5, EC6, EC9, EC10, EC11, EC12, EC14, EC15, EC16, and EC17 and then expanding the predicates ClippedDeclippedStoppedInStartedInPersistsBetweenReleasedBetween, and ReleasedIn using definitions EC1, EC2, EC3, EC4, EC7, EC8, and EC13.

Example 17.5. Consider again the light example. We replace (17.15) with the following:

¬HoldsAt(On,0)

We add the following:

(17.28)

¬ReleasedAt(f,t)

(17.29)

Let Σ be the conjunction of (17.10), (17.11), (17.13), (17.14), (17.16), (17.28), and (17.29). Again, we get the same results.

Proposition 17.12. Σ ∧ EC |= ¬HoldsAt(On,1).

Proof. From (17.13) and EC2, we have ¬Declipped(0,On,1). From this, (17.28), 0 < 1, PersistsBetween(0,On,1) (which follows from (17.29) and EC7), and EC10, we have ¬HoldsAt(On,1).

Proposition 17.13. Σ ∧ EC |= HoldsAt(On,3).

Proof. From (17.13) and EC3, we have ¬StoppedIn(2,On,3). From this, Happens(TurnOn,2) (which follows from (17.13)), Initiates(TurnOn,On,2) (which follows from (17.10)), 2 < 3, ¬ReleasedIn(2,On,3) (which follows from (17.13) and

EC13), and EC14, we have HoldsAt(On,3).

Proposition 17.14. Σ ∧ EC |= ¬HoldsAt(On,5).

Proof. From (17.13) and EC4, we have ¬StartedIn(4,On,5). From this, Happens(TurnOff,4) (which follows from (17.13)), Terminates(TurnOff,On,4) (which follows from (17.11)), 4 < 5, ¬ReleasedIn(4,On,5) (which follows from (17.13) and EC13), and EC15, we have ¬HoldsAt(On,5). 

17.2.5 Discrete Event Calculus (DEC)

Mueller [70, 74] developed the discrete event calculus (DEC) to improve the efficiency of automated reasoning in the event calculus. DEC improves efficiency by limiting time to the integers, and eliminating triply quantified time from many of the axioms.

The predicates of DEC are the same as those of EC, as shown in Table 17.4. The axioms and definitions of DEC are as follows.

def

DEC1. StoppedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t

Terminates(e,f,t)).

def

DEC2. StartedIn(t1,f,t2) ≡ ∃e,t (Happens(e,t) ∧ t< t < t∧ Initiates(e,f,t)).

DEC3. Happens(e,t1)∧Initiates(e,f1,t1)∧0 < tTrajectory(f1,t1,f2,t2)∧ ¬StoppedIn(t1,f1,t+ t2) ⊃ HoldsAt(f2,t+ t2).

DEC4. Happens(e,t1) ∧ Terminates(e,f1,t1) ∧ 0 < t∧ AntiTrajectory(f1,t1, f2,t2) ∧ ¬StartedIn(t1,f1,t+ t2) ⊃ HoldsAt(f2,t+ t2).

DEC5. HoldsAt(f,t) ∧ ¬ReleasedAt(f,t + 1) ∧ ¬∃e(Happens(e,t) ∧ Terminates(e,f,t)) ⊃ HoldsAt(f,t + 1).

DEC6. ¬HoldsAt(f,t) ∧ ¬ReleasedAt(f,t + 1) ∧ ¬∃e(Happens(e,t) ∧ Initiates(e,f,t)) ⊃ ¬HoldsAt(f,t + 1).

DEC7. ReleasedAt(f,t) ∧ ¬∃e(Happens(e,t) ∧ (Initiates(e,f,t) ∨ Terminates(e,f,t))) ⊃ ReleasedAt(f,t + 1).

DEC8. ¬ReleasedAt(f,t) ∧ ¬∃e(Happens(e,t) ∧ Releases(e,f,t)) ⊃ ¬ReleasedAt(f,t + 1).

DEC9. Happens(e,t) ∧ Initiates(e,f,t) ⊃ HoldsAt(f,t + 1).

DEC10. Happens(e,t) ∧ Terminates(e,f,t) ⊃ ¬HoldsAt(f,t + 1). DEC11. Happens(e,t) ∧ Releases(e,f,t) ⊃ ReleasedAt(f,t + 1).

DEC12. Happens(e,t) ∧ (Initiates(e,f,t) ∨ Terminates(e,f,t)) ⊃ ¬ReleasedAt(f,t + 1).

Let DEC be the formula generated by conjoining axioms DEC3 through DEC12 and then expanding the predicates StoppedIn and StartedIn using definitions DEC1 and DEC2.

The difference between EC and DEC is that EC operates over spans of timepoints, whereas DEC operates timepoint by timepoint. For example, EC14 states that a fluent that is initiated remains true until it is terminated or released. This corresponds to several DEC axioms. DEC9 states that a fluent that is initiated is true at the next timepoint. DEC5 states that a fluent that is true, not released from the commonsense law of inertia, and not terminated, is true at the next timepoint. The axioms dealing with Trajectory and AntiTrajectory, DEC3 and DEC4, are the same as EC5 and EC6. The definitions of StoppedIn and StartedIn, DEC1 and DEC2, are the same as EC3 and EC4.

Example 17.6. Consider again the light example. Let Σ be as for EC.

Proposition 17.15. Σ ∧ DEC |= ¬HoldsAt(On,1).

Proof. From (17.13), we have ¬∃e(Happens(e,0) ∧ Initiates(e,On,0)). From this, (17.28), ¬ReleasedAt(On,1) (which follows from (17.29)), and DEC6, we have

¬HoldsAt(On,1). Proposition 17.16. Σ ∧ DEC |= HoldsAt(On,3).

Proof. From Happens(TurnOn,2) (which follows from (17.13)), Initiates(TurnOnOn,2) (which follows from (17.10)), and DEC9, we have HoldsAt(On,3).  Proposition 17.17. Σ ∧ DEC |= ¬HoldsAt(On,5).

Proof. From Happens(TurnOff,4) (which follows from (17.13)), Terminates(TurnOff,

On,4) (which follows from (17.11)), and DEC10, we have ¬HoldsAt(On,5).

17.2.6 Equivalence of DEC and EC

We have the following equivalence between DEC and EC.

Proposition 17.18. If the domain of the timepoint sort is restricted to the integersthen DEC is logically equivalent to EC.

Proof. (EC |= DEC) By universal instantiation, substituting t1+1 for t2. For example, DEC9 is obtained from EC14 via the following chain of equivalences:

Happens(e,t1) ∧ Initiates(e,f,t1) ∧ t< t+ 1 ∧ ¬StoppedIn(t1,f,t+ 1)∧

¬ReleasedIn(t1,f,t+ 1) ⊃ HoldsAt(f,t+ 1)

Happens(e,t1) ∧ Initiates(e,f,t1)∧

¬∃e,t (Happens(e,t) ∧ t< t < t+ 1 ∧ Terminates(e,f,t))∧

¬∃e,t (Happens(e,t) ∧ t< t < t+ 1 ∧ Releases(e,f,t)) ⊃ HoldsAt(f,t+ 1)

≡ (for integer time)

Happens(e,t1) ∧ Initiates(e,f,t1) ⊃ HoldsAt(f,t+ 1)

(DEC |= EC) By a series of lemmas showing that each EC axiom follows from DEC.

See [70] or [74].

17.2.7 Other Versions

Other versions of the event calculus have been developed to support

  • causal constraints for instantaneously interacting indirect effects [101].
  • continuously changing parameters using differential equations [64, 66].
  • events with duration [66, 97, 100].
  • hierarchical or compound events [97, 100].

 17.3 Relationship to other Formalisms

The event calculus is closely related to the situation calculus (see Chapter 16) and temporal action logics (see Chapter 18). The relation between the event calculus and the situation calculus is treated by Kowalski and Sadri [43, 44] and Van Belleghem, Denecker, and De Schreye [112]. The relation between the event calculus and temporal action logics is treated by Mueller [75]. Bennett and Galton [4] define a versatile event logic (VEL) and use it to describe versions of the situation calculus and the event calculus. A problem for future research is the relation of the event calculus and nonmonotonic causal logic.

17.4 Default Reasoning

An axiomatization is elaboration tolerant to the degree that it can be extended easily [61]. In the examples given so far, we have fully specified the effects of events and the event occurrences. That is, we have supplied bi-implications for the predicates InitiatesTerminatesReleases, and Happens. This is not very elaboration tolerant, because whenever we wish to add event effects and occurrences, we must modify these bi-implications.

Instead, we should be able to write individual axioms specifying what effects particular events have on particular fluents and what events occur. But then we have two problems:

  1. how to derive what effects particular events do not have on particular fluents, or the frame problem [8, 62, 98, 105] (see also Section 16.2), and
  2. how to derive what events do not occur.

These problems can be solved using any framework for default or nonmonotonic reasoning [5, 7] (see also Chapters 6 and 7). In this section, we discuss the use of circumscription [51, 56, 57, 59] (see Section 6.4) and negation as failure [11].

17.4.1 Circumscription

Consider the light example. Instead of writing the single axiom

Happens(e,t) ≡ (e = TurnOn ∧ t = 2) ∨ (e = TurnOff ∧ t = 4) (17.30)

we write several axioms:

Happens(TurnOn,2) (17.31)

Happens(TurnOff,4) (17.32)

Then we circumscribe Happens in (17.31) ∧ (17.32), which yields (17.30).

Circumscription allows us to assume by default that the events known to occur are the only events that occur. That is, there are no extraneous events. If we allowed extraneous events, then we could no longer prove, say, that the light is off at timepoint 6, because we could no longer prove the absence of events turning on the light between timepoints 4 and 6. If we later add the axiom

Happens(TurnOn,5)

then we recompute the circumscription, which allows us to prove that in fact the light is on at timepoint 6.

Similarly, we write separate axioms for InitiatesTerminates, and Releases, and circumscribe these predicates, which allows us to assume by default that the known effects of events are the only effects of events. That is, there are no extraneous event effects. If we allowed extraneous event effects, then we could no longer prove that the light is off at timepoint 6 if some unrelated event occurred between timepoints 4 and

6, because we could no longer prove that the unrelated event does not turn on the light.

17.4.2 Computing Circumscription

It is difficult to compute circumscription in general [16]. The circumscription of a predicate in a formula, which is defined by a formula of second-order logic, does not always reduce to a formula of first-order logic [47]. In many cases, however, we can compute circumscription using the following two propositions. The first proposition asserts that certain circumscriptions reduce to predicate completion. (See Section 7.3.2.)

Proposition 17.19. Let ρ be an n-ary predicate symbol and Δ(x1,...,xnbe a formula whose only free variables are x1,...,xnIf Δ(x1,...,xndoes not contain ρ, then the circumscription CIRC[∀x1,...,x(Δ(x1,...,xn) ⊃ ρ(x1,...,xn)];ρ) is equivalent to ∀x1,...,x(Δ(x1,...,xn) ≡ ρ(x1,...,xn)).

Proof. See the proof of Proposition 2 of Lifschitz [51]. (See also [84].)

This gives us the following method for computing circumscription of ρ in a formula:

  1. Rewrite the formula in the form ∀x1,...,xn (Δ(x1,...,xn) ⊃ ρ(x1,...,xn)), where Δ(x1,...,xn) does not contain ρ.
  2. Apply Proposition 17.19.

Example 17.7. Let Σ = Initiates(E1,F1,t) ∧ Initiates(E2,F2,t). We compute

CIRC[Σ;Initiates] by rewriting Σ as

(e = E∧ f = F1) ∨ (e = E∧ f = F2) ⊃ Initiates(e,f,t)

and then applying Proposition 17.19, which gives

Initiates(e,f,t) ≡ (e = E∧ f = F1) ∨ (e = E∧ f = F2)

The second proposition allows us to compute the circumscription of several predicates, called parallel circumscription. We start with a definition.

Definition 17.1. A formula Δ is positive relative to a predicate symbol ρ if and only if all occurrences of ρ in Δ are in the range of an even number of negations in an equivalent formula obtained by eliminating ⊃ and ≡ from Δ.

Proposition 17.20. Let ρ1,...,ρbe predicate symbols and Δ be a formulaIf Δ is positive relative to every ρithen the parallel circumscription CIRC[Δ;ρ1,...,ρnis equivalent tohttps://lh4.googleusercontent.com/VYh2lSc39GhxsXnIUiteNKeot8_51uDUlMyz6XXpiOfUX85jSfwK386GYw5fp7q-m7CxCEXGnj80T0xIDUoTrj1bcGoRWepwSoFqBqjRM3EprI5bzICEIZf1siZfPImt9hG0puE CIRC[Δ;ρi].

Proof. See the proof of Proposition 14 of Lifschitz [51].

Further methods for computing circumscription are discussed in Section 6.4.4.

Example 17.8. Let Σ be the conjunction of the following axioms:

Initiates(TurnOn,On,t)

Terminates(TurnOff,On,t)

Let Δ be the conjunction of the following axioms:

Happens(TurnOn,2)

Happens(TurnOff,4)

Let Γ be the conjunction of (17.14), (17.28), and (17.29). We can use circumscription to prove that the light is on at timepoint 3.

Proposition 17.21.

CIRC[Σ;Initiates,Terminates,Releases] ∧ CIRC[Δ;Happens] ∧ Γ ∧ EC |= HoldsAt(On,3)

Proof. From CIRC[Σ;Initiates,Terminates,Releases], Propositions 17.20 and 17.19, we have

(Initiates(e,f,t) ≡ (e = TurnOn ∧ f = On)) ∧

(Terminates(e,f,t) ≡ (e = TurnOff ∧ f = On)) ∧

¬Releases(e,f,t) (17.33)

From CIRC[Δ;Happens] and Proposition 17.19, we have

Happens(e,t) ≡ (e = TurnOn ∧ t = 2) ∨ (e = TurnOff ∧ t = 4) (17.34)

From this and EC3, we have ¬StoppedIn(2,On,3). From this, Happens(TurnOn,2) (which follows from (17.34)), Initiates(TurnOn,On,2) (which follows from (17.33)), 2 < 3, ¬ReleasedIn(2,On,3) (which follows from (17.34) and EC13), and EC14, we have HoldsAt(On,3).

17.4.3 Historical Note

Notice that we keep the event calculus axioms EC outside the scope of any circumscription. This technique, known as filtering, was introduced in the features and fluents framework [14, 15, 89, 90] (see also Chapter 18) and incorporated into the event calculus by Shanahan [96, 98]. The need for filtering became clear after Hanks and McDermott [32] introduced the Yale shooting scenario, which exposed problems with simply circumscribing the entire situation calculus axiomatization of the scenario. Shanahan [98] describes treatments of the Yale shooting scenario in the situation calculus and the event calculus; Shanahan [105] and Lifschitz [52] provide a modern perspective.

17.4.4 Negation as Failure

Instead of using circumscription for default reasoning in the event calculus, logic programming with the negation as failure operator not may be used [41, 45, 93, 94]. For example, we write rules such as the following:

clipped(T 1,F,T 2) ← happens(E,T), T 1 <= T, T < T 2, terminates(E,F,T).

holds_at(F,T 2) ← holds_at(F,T 1), T 1 < T 2, not clipped(T 1,F,T 2).

These rules are similar to axioms EC1 and EC9. Then we add rules such as the following to our domain description: initiates(turn_on,on,T). terminates(turn_off,on,T). happens(turn_on,2). happens(turn_off,4).

Mueller [73] provides complete lists of event calculus rules for use with answer set solvers [3, 79] along with sample domain descriptions.

17.5 Event Calculus Knowledge Representation

This section describes methods for representing knowledge using the event calculus. These methods can be used with BEC, EC, and DEC. Those that do not involve trajectories or release from the commonsense law of inertia can also be used with SEC.

17.5.1 Parameters

We represent events and fluents with parameters as functions that return event and fluent terms. For example, we may represent the event of person p turning on light l using a function TurnOn(p,l), and the property that light l is turned on using a function On(l). We then require the following unique names axioms:

TurnOn(p1,l1) = TurnOn(p2,l2) ⊃ p= p∧ l= l(17.35)

On(l1) = On(l2) ⊃ l= l(17.36)

If we have another event TurnOff(p,l), then we also require the unique names axiom:

TurnOn(p1,l1) = TurnOff(p2,l2) (17.37)

The U notation [48] is convenient for defining unique names axioms. If φ1,...,φare function symbols, then U[φ1,...,φk] is an abbreviation for the conjunction of the formulas φi(x1,...,xm) = φj(y1,...,yn)

where m is the arity of φi, n is the arity of φj, and x1,...,xand y1,...,yare distinct variables such that the sort of xis the sort of the pth argument position of φand the sort of yis the sort of the pth argument position of φj, for each 1  https://lh4.googleusercontent.com/wGL-37oXVH1XkrWZE82wEFYUearyrWrFRfn0b4_VOBeGHEQT2LurE1Mn78R3weUCWm5ONNgixTi1or0RG3mMcGBgEDaIoM4Hzc7oP_ub-ZsbF2mhAv6r9wdhBcX0tO2tXx3YDa0k, and the conjunction of the formulas φi(x1,...,xm) = φi(y1,...,ym) ⊃ x= y∧ ··· ∧ x= ym

where m is the arity of φand x1,...,xand y1,...,yare distinct variables such that the sort of xand yis the sort of the pth argument position of φi, for each

https://lh4.googleusercontent.com/3rxYVUKn4WCe7iu9Si64FXpp365t6jFhsxE9hskhECcIMBnsGDHkP8Uobax-Y2iT4VSiEbKYgBpVqHT295uWW0yBIqdFSbyrycDcVFHF6TaxK3c2RSWiJbivbFjq8Mqjv0fF5pg.

We may then use this notation to replace (17.35), (17.36), and (17.37) with

U[TurnOn,TurnOff] ∧ U[On]

In the remainder of this section, we assume that appropriate unique names axioms are defined.

17.5.2 Event Effects

The effects of events are represented using effect axioms, which are of the form γ ⊃ Initiates(α,β,τ), or γ ⊃ Terminates(α,β,τ)

where γ is a condition, α is an event, β is a fluent, and τ is a timepoint. A condition is a formula containing atoms of the form HoldsAt(β,τ) and ¬HoldsAt(β,τ), where β is a fluent and τ is a timepoint.

Example 17.9. Consider a counter that can be incremented and reset. The fluent Value(c,v) represents that counter c has value v. The event Increment(c) represents that counter c is incremented, and the event Reset(c) represents that the counter c is reset. We use two effect axioms to represent that, if the value of a counter is v and the counter is incremented, its value will be v + 1 and will no longer be v:

HoldsAt(Value(c,v),t) ⊃ Initiates(Increment(c),Value(c,v + 1),t) (17.38)

HoldsAt(Value(c,v),t) ⊃ Terminates(Increment(c),Value(c,v),t) (17.39)

We use two more effect axioms to represent that, if the value of a counter is v and the counter is reset, its value will be 0 and will no longer be v:

Initiates(Reset(c),Value(c,0),t) (17.40)

HoldsAt(Value(c,v),t) ∧ c = 0 ⊃ Terminates(Reset(c),Value(c,v),t)

(17.41)

The effect of an event can depend on the context in which it occurs. The condition γ represents the context. In the example of the counter, the effect of incrementing the counter depends on its current value.

17.5.3 Preconditions

We might represent the effect of turning on a device as follows:

Initiates(TurnOn(p,d),On(d),t)

But there are many things that could prevent a device from going on. It could be unplugged or broken, its on-off switch could be broken, and so on. A qualification is a condition that prevents an event from having its intended effects. The qualification problem is the problem of representing and reasoning about qualifications.

A partial solution to the qualification problem is to use preconditions. The condition γ of effect axioms can be used to represent preconditions.

Example 17.10. If a person turns on a device, then, provided the device is not broken, the device will be on:

¬HoldsAt(Broken(d),t) ⊃ Initiates(TurnOn(p,d),On(d),t) (17.42)

But this is not elaboration tolerant, because whenever we wish to add qualifications, we must modify (17.42). Instead we can use default reasoning.

Example 17.11. Instead of writing (17.42), we write

¬Ab1(d,t) ⊃ Initiates(TurnOn(p,d),On(d),t) (17.43)

Ab1(d,t) is an abnormality predicate [28, 58–60]. It represents that at timepoint t, device d is abnormal in some way that prevents it from being turned on. In general, we use a distinct abnormality predicate for each type of abnormality. We then add qualifications by writing cancellation axioms [23, 51, 59]:

HoldsAt(Broken(d),t) ⊃ Ab1(d,t) (17.44)

¬HoldsAt(PluggedIn(d),t) ⊃ Ab1(d,t) (17.45)

We then circumscribe the abnormality predicate Abin the conjunction of cancellation axioms (17.44) and (17.45), which yields

Ab1(d,t) ≡ HoldsAt(Broken(d),t) ∨ ¬HoldsAt(PluggedIn(d),t) (17.46)

We then reason using (17.43) and (17.46). Whenever we wish to add additional qualifications, we add cancellation axioms and recompute the circumscription of the abnormality predicates in the cancellation axioms.

17.5.4 State Constraints

Law-like relationships among properties are represented using state constraint, which are formulas containing atoms of the form HoldsAt(β,τ) and ¬HoldsAt(β,τ), where β is a fluent and τ is a timepoint.

For example, we may use two state constraints to represent that a counter has exactly one value at a time:

∃v HoldsAt(Value(c,v),t) (17.47)

HoldsAt(Value(c,v1),t) ∧ HoldsAt(Value(c,v2),t) ⊃ v= v(17.48)

17.5.5 Concurrent Events

In the event calculus, events may occur concurrently. That is, we may have Happens(e1, t1) and Happens(e2,t2) where e= eand t= t2. We represent the effects of concurrent events using effect axioms whose conditions contain atoms of the form Happens(α,τ) and ¬Happens(α,τ), where α is an event and τ is a timepoint [66].

Example 17.12. Consider again the example of the counter. Suppose that the value of a counter is 5 at timepoint 0:

HoldsAt(Value(C,5),0) (17.49)

Further suppose that the counter is simultaneously incremented and reset at timepoint 1:

Happens(Increment(C),1)

(17.50)

Happens(Reset(C),1)

(17.51)

(17.50) leads us to conclude

HoldsAt(Value(C,6),2)

whereas (17.51) leads us to conclude

HoldsAt(Value(C,0),2)

These formulas contradict the state constraint (17.48).

In order to deal with this, we may specify exactly what happens when a counter is simultaneously incremented and reset. There are a number of possibilities.

One possibility is that nothing happens. We replace the effect axioms (17.38), (17.39), (17.40), and (17.41) with the following effect axioms:

¬

Happens(Reset(c),t) ∧ HoldsAt(Value(c,v),t) ⊃

Initiates(Increment(c),Value(c,v + 1),t) (17.52)

¬

Happens(Reset(c),t) ∧ HoldsAt(Value(c,v),t) ⊃

Terminates(Increment(c),Value(c,v),t) (17.53)

¬

Happens(Increment(c),t) ⊃

Initiates(Reset(c),Value(c,0),t) (17.54)

¬

Happens(Increment(c),t) ∧ HoldsAt(Value(c,v),t) ∧ c = 0 ⊃

Terminates(Reset(c),Value(c,v),t) (17.55)

Another possibility is that the counter is neither incremented nor reset, but that the counter enters an error state. We use the effect axioms (17.52), (17.53), (17.54), and (17.55), and a further effect axiom that represents that, if a counter is simultaneously reset and incremented, it will be in an error state:

Happens(Reset(c),t) ⊃

Initiates(Increment(c),Error(c),t)

We could also have written this as

Happens(Increment(c),t) ⊃

Initiates(Reset(c),Error(c),t)

Another possibility is that, if a counter is simultaneously reset and incremented, the incrementing takes priority and the counter is incremented:

HoldsAt(Value(c,v),t) ⊃

Initiates(Increment(c),Value(c,v + 1),t)

HoldsAt(Value(c,v),t) ⊃

Terminates(Increment(c),Value(c,v),t)

¬

Happens(Increment(c),t) ⊃

Initiates(Reset(c),Value(c,0),t)

¬

Happens(Increment(c),t) ∧ HoldsAt(Value(c,v),t) ∧ c = 0 ⊃

Terminates(Reset(c),Value(c,v),t)

Similarly, we could represent that, if a counter is simultaneously reset and incremented, the resetting takes priority and the counter is reset.

17.5.6 Triggered Events

Events that are triggered under certain circumstances are represented using trigger axioms [94, 96, 98], which are of the form γ ⊃ Happens(α,τ)

where γ is a condition, α is an event, and τ is a timepoint.

Example 17.13. Consider a thermostat that turns on a heater when the temperature drops below A, and turns off the heater when the temperature rises above B. We represent this using two effect axioms and two trigger axioms:

Initiates(TurnOn,On,t)

Terminates(TurnOff,On,t)

HoldsAt(Temperature(v),t) ∧ v < A ∧ ¬HoldsAt(On,t) ⊃

Happens(TurnOn,t)

HoldsAt(Temperature(v),t) ∧ v > B ∧ HoldsAt(On,t) ⊃

Happens(TurnOff,t)

The conditions ¬HoldsAt(On,t) and HoldsAt(On,t) are required to prevent TurnOn and TurnOff from repeatedly triggering.

17.5.7 Continuous Change

Examples of continuous change include falling objects, expanding balloons, and containers being filled. Continuous change is represented using trajectory axioms [94, 95, 98], which are of the form γ ⊃ Trajectory1122), or γ ⊃ AntiTrajectory1122)

where γ is a condition, βand βare fluents, and τand τare timepoints. Trajectory is used to determine the truth value of fluent βafter fluent βis initiated, until βis terminated. AntiTrajectory is used to determine the truth value of fluent βafter fluent βis terminated, until βis initiated.

Although DEC does not support continuous time, we may still use Trajectory and AntiTrajectory in DEC to represent gradual change. Gradual change is a discrete approximation to continuous change in which the value of a changing fluent is only represented for integer timepoints.

Example 17.14. Consider a falling object. We use effect axioms to represent that, if a person drops an object, then it will be falling, and if an object hits the ground, then it will no longer be falling:

Initiates(Drop(p,o),Falling(o),t) (17.56)

Terminates(HitGround(o),Falling(o),t) (17.57)

We represent that, if a person drops an object, then its height will be released from the commonsense law of inertia:

Releases(Drop(p,o),Height(o,h),t) (17.58)

(For an object o, Height(o,h) is released for all h.) We use a trajectory axiom to represent that the height of the object is given by an equation of free-fall motion, where G is the acceleration due to gravity (9.8 m/sec2):

HoldsAt(Height(o,h),t1) ⊃

Trajectory(Falling(o),t1,Heighthttps://lh5.googleusercontent.com/WEtiDEKVAaxCWetMfx1zh8WpwekyJlbzFYBRLqDX8fVTZYe6QzMQTHHNgjJ4GzX8FoM-QEGCGrcu48xtPNKLSFumkZjVnEXwTJdtA5YdXkNva4lQZv0gDfm9UiIDoedZ7gRvxQc (17.59)

We use a trigger axiom to represent that, when an object is falling and its height is 0, it hits the ground:

HoldsAt(Falling(o),t) ∧ HoldsAt(Height(o,0),t) ⊃

Happens(HitGround(o),t) (17.60)

We specify that, if an object hits the ground and its height is h, then its height will be h and its height will no longer be released from the commonsense law of inertia:

HoldsAt(Height(o,h),t) ⊃ Initiates(HitGround(o),Height(o,h),t) (17.61)

We specify that an object has a unique height:

HoldsAt(Height(o,h1),t) ∧ HoldsAt(Height(o,h2),t) ⊃ h= hAt timepoint 0, Nathan drops an apple whose height is G/2:

(17.62)

¬HoldsAt(Falling(Apple),0)

(17.63)

HoldsAt(Height(Apple,G/2),0)

(17.64)

Happens(Drop(Nathan,Apple),0)

(17.65)

We can then show that the apple will hit the ground at timepoint 1, and its height at timepoint 2 will be zero.

Proposition 17.22. Let (17.60) ∧https://lh5.googleusercontent.com/-nkIIbu6HaTSa0XdsXXab0HwARdo2ri242nk_OWn-DLtGCxHjdzfeT3GjsrCAhUWjCcvC9cvD29eMLPVSbE7xVOMAYIwYEJ2i9-4KIqUvHaCyy23t6NTE9JGYDIDX6TGbQbQa1I

  1. 65), Ω = U[Drop, ] ∧ U[ , ], Γ =

(17.63) ∧ (17.64). Then we have

CIRC[Σ;Initiates,Terminates,Releases] ∧

CIRC[Δ;Happens] ∧ Ω ∧ Γ ∧ EC

 HoldsAt(Height(Apple,0),1) ∧

Happens(HitGround(Apple),1) ∧ HoldsAt(Height(Apple,0),2).

Proof. See the proofs of Propositions 7.2 and 7.3 of Mueller [74].

17.5.8 Nondeterministic Effects

Nondeterministic effects of events can be represented in the event calculus using determining fluents [98], or fluents released from the commonsense law of inertia that are used within the conditions of effect axioms.

Example 17.15. Consider the example of rolling a die with six sides. We define a determining fluent DieDF(d,s) which represents that die d will land on side s. This fluent is released from the commonsense law of inertia. In EC and DEC, we require the axiom

ReleasedAt(DieDF(d,s),t)

In BEC, a fluent that is never initiated or terminated and is neither InitiallyN nor InitiallyP is released from the commonsense law of inertia, so no further axioms are required to released DieDF from the commonsense law of inertia.

We use state constraints to represent that, at any timepoint, DieDF(d,s) assigns one of the sides {1,...,6} to a die:

∃s HoldsAt(DieDF(d,s),t)

HoldsAt(DieDF(d,s1),t) ∧ HoldsAt(DieDF(d,s2),t) ⊃ s= s2

HoldsAt(DieDF(d,s),t) ⊃ s = 1 ∨ s = 2 ∨ s = 3 ∨ s = 4 ∨ s = 5 ∨ s = 6

We use effect axioms to represent that, if a die is rolled at a timepoint, it will land on the side assigned to the die by DieDF at that timepoint:

HoldsAt(DieDF(d,s),t) ⊃ Initiates(Roll(d),Side(d,s),t)

HoldsAt(Side(d,s1),t) ∧ HoldsAt(DieDF(d,s2),t) ∧ s= s

Terminates(Roll(d),Side(d,s1),t)

Suppose a die D is rolled at timepoint 0:

Happens(Roll(D),0)

What side of the die faces up at timepoint 1? Because DieDF is free to take on any of six values at timepoint 0, we get six classes of models: one in which HoldsAt(DieDF(D,1),0) and therefore HoldsAt(Side(D,1),1), one in which HoldsAt(DieDF(D,2),0) and therefore HoldsAt(Side(D,2),1), and so on.

17.5.9 Indirect Effects

Suppose that a person and a book are in the living room of a house. When the person walks out of the living room, the book will normally remain in the living room. But if the person is holding the book and walks out of the living room, then the book will no longer be in the living room. That is, an indirect effect or ramification of the person walking out of the living room is that the book the person is holding changes location. The ramification problem [19, 24, 101] is the problem of representing and reasoning about the indirect effects of events. Much research has been performed on the ramification problem [2, 19, 24, 29, 30, 35, 48, 50, 53–55, 85, 91, 101, 111]. Several methods can be used for solving this problem in the event calculus.

Example 17.16 (State constraints). Consider again the example of a light. We represent the direct effect of turning on a light using an effect axiom:

Initiates(TurnOn(l),On(l),t)

We may use a state constraint to represent the indirect effect of turning on the light, namely that the light is not off:

¬HoldsAt(Off(l),t) ≡ HoldsAt(On(l),t)

The fluent Off(l) must be released from the commonsense law of inertia. In EC and

DEC, we require the axiom

ReleasedAt(Off(l),t)

This method of representing indirect effects works if it is possible to divide fluents into primitive and derived fluents [39, 48, 50, 101]. Here On is primitive and Off is derived. The direct effects of events on primitive fluents are represented using effect axioms, whereas the indirect effects of events on derived fluents are represented using state constraints.

Example 17.17 (Release from inertia and state constraints). Suppose that we wish to represent the indirect effects of walking while holding an object, namely that the object moves along with the person holding it. We create a simple axiomatization of space. We start by representing the direct effects of walking. If a person walks from location lto location l2, then the person will be at land will no longer be at l1:

Initiates(Walk(p,l1,l2),At(p,l2),t) l= l⊃ Terminates(Walk(p,l1,l2),At(p,l1),t)

We also represent the direct effects of picking up and setting down an object. If a person and an object are at the same location and the person picks up the object, then the person will be holding the object:

HoldsAt(At(p,l),t) ∧ HoldsAt(At(o,l),t) ⊃ Initiates(PickUp(p,o),Holding(p,o),t)

If a person sets down an object, then the person will no longer be holding it:

Terminates(SetDown(p,o),Holding(p,o),t)

We then represent the indirect effects of walking with a Releases axiom, a state constraint, and an effect axiom. If a person and an object are at the same location and the person picks up the object, then the object’s location will be released from the commonsense law of inertia:

HoldsAt(At(p,l),t) ∧ HoldsAt(At(o,l),t) ⊃

Releases(PickUphttps://lh4.googleusercontent.com/rvrICIvrfGEGLyrwjj-O1WjsAPrZCQZ7HTdHkKCqSsoDDIb619Uym0-QI57MoDYu5J9eKnld9VY5L0XHfkzIBWs_z6LVgTN3k4x2rBmcmWax0iWMzGohtWyQU1yIwtn86EzqGFo (17.66)

(For any given objecthttps://lh5.googleusercontent.com/074Vr85WZCz8vv65CqScWo96iKtWpZUIexUhXQ1mTgf3WLlEC_d1nf1D0LsNLbGGZHqStfMeLeXC9eDN8BQDLfsZzfFqOSSM_W0AQCdwla7hlK5kgxsQctwiYM-gIQH9qizoJPk is released for all l.) If a person who is holding an object is located at l, then the object is also located at l:

HoldsAt(Holding(p,o),t) ∧ HoldsAt(At(p,l),t) ⊃ HoldsAt(At(o,l),t)

(17.67)

If a person is holding an object, the person is located at l, and the person sets down the object, then the object will be located at l and the object’s location will no longer be released from the commonsense law of inertia:

HoldsAt(Holding(p,o),t) ∧ HoldsAt(At(p,l),t) ⊃

Initiates(SetDown(p,o),At(o,l),t) (17.68)

Example 17.18 (Effect axioms). Another way of representing indirect effects is simply to add more effect axioms. We replace (17.66), (17.67), and (17.68) with effect axioms that state that, if a person who is holding an object walks from location lto location l2, then the object will be at location land will no longer be at l1:

HoldsAt(Holding(p,o),t) ⊃ Initiates(Walk(p,l1,l2),At(o,l2),t)

HoldsAt(Holding(p,o),t) ∧ l= l

Terminates(Walk(p,l1,l2),At(o,l1),t)

Example 17.19 (Effect constraints). Another way of representing indirect effects is to use effect constraints [98, 101], which are of the form γ ∧ π1(α,β1,τ) ⊃ π2(α,β2,τ)

where γ is a condition, πand πare Initiates or Terminates, α is an event variable, βand βare fluents, and τ is a timepoint. We use effect constraints to represent that an object moves along with the person holding it:

HoldsAt(Holding(p,o),t) ∧ Initiates(e,At(p,l),t) ⊃ Initiates(e,At(o,l),t)

HoldsAt(Holding(p,o),t) ∧ Terminates(e,At(p,l),t) ⊃ Terminates(e,At(o,l),t)

The event calculus can also be extended to deal with instantaneously interacting indirect effects [101].

The aforementioned methods for dealing with ramifications have various advantages and disadvantages. The method of state constraints is simple, but it requires a clear separation of fluents into those directly affected by events (primitive fluents) and those indirectly affected by events (derived fluents).

The method of releasing a fluent from the commonsense law of inertia allows a fluent to be primitive at some timepoints and derived at other timepoints. But then more bookkeeping is required. We must release the fluent from the commonsense law of inertia, and later make the fluent again subject to this law.

The method of using effect axioms is also simple, but it is less elaboration tolerant. In our example, if we add another way for a person to change location, such as running, we must also add axioms for the indirect effects of running:

HoldsAt(Holding(p,o),t) ⊃ Initiates(Run(p,l1,l2),At(o,l2),t)

HoldsAt(Holding(p,o),t) ∧ l= l⊃ Terminates(Run(p,l1,l2),At(o,l1),t)

The method of using effect constraints is the most elaboration tolerant. But we cannot apply Proposition 17.19 in order to compute the circumscription of Initiates and Terminates in effect constraints.

17.5.10 Partially Ordered Events

We may represent partially ordered events using inequalities involving timepoints. For example, we may represent that John picked up a pen and a pad in some unspecified order, and then walked from the office to the living room as follows:

Happens(PickUp(John,Pen),T1)

Happens(PickUp(John,Pad),T2)

Happens(Walk(John,Office,LivingRoom),T3)

T1 < T3

T2 < T3

Using the simple axiomatization of space of Example 17.17 in Section 17.5.9, we can conclude that John was holding both the pen and the pad at T3, and that the pen and the pad are both in the living room after T3. But we cannot conclude that John was holding the pad when he picked up the pen, or that John was holding the pen when he picked up the pad. There are three classes of models:

  1. those in which John picks up the pen and then the pad (T< T2),
  2. those in which John picks up the pad and then the pen (T< T1), and
  3. those in which John picks up the pen and pad simultaneously (T= T2).

17.6 Action Language E

Instead of using classical logic for reasoning about action and change, specialized action languages [22, 25, 26, 81] can be used. The E action language introduced by Antonis C. Kakas and Rob Miller [35, 36] is closely related to the event calculus.

A language of E is specified by a set of fluents, a set of events, a set of timepoints, and a partial order on the set of timepoints. An E domain description consists of a set of statements, which are defined as follows.

Definition 17.2. If β is a fluentthen β and ¬β are fluent literals.

Definition 17.3. If γ is a fluent literal and τ is a timepointthen γ holds-at τ is a statement.

Definition 17.4. If α is an event and τ is a timepointthen α happens-at τ is a statement.

Definition 17.5. If α is an event, β is a fluentand Γ is a set of fluent literalsthen α initiates β when Γ and α terminates β when Γ

are statements.

The notation α initiates β is an abbreviation for α initiates β when ∅, and the notation α terminates β is an abbreviation for α terminates β when ∅.

Example 17.20. We represent the example of turning on and off a light using the following E domain description:

TurnOn initiates On TurnOff terminates On ¬On holds-at TurnOn happens-at TurnOff happens-at 4

This domain description entails the following:

¬On holds-at 1 On holds-at 3 ¬On holds-at 5

Kakas and Miller [35, 36] specify the semantics of E using simple definitions of structures and models. Miller and Shanahan [66] show that E corresponds to the EC of Section 17.2.4 without the predicates ReleasedAtReleasesTrajectory, and AntiTrajectory. They define conditions under which an E domain description matches an EC domain description and prove that, if an E domain description matches an EC domain description, the domain descriptions entail the same fluent truth values. Dimopoulos, Kakas, and Michael [13] give a translation of E domain descriptions into answer set programs [3, 20, 21] (see also Chapter 7).

An E domain description can be translated into an EC or DEC domain description as follows. We assume that the timepoints are the integers and the partial order is . We divide the E domain description into sets of holds-athappens-atinitiates, and terminates statements. We translate each holds-at statement

[¬]β holds-at τ into the formula

[¬]HoldsAt(β,τ)

We translate the set of happens-at statements αhappens-at τ1

...

αhappens-at τn

into the formula

Happens(e,t) ≡ (e = α∧ t = τ1) ∨ ··· ∨ (e = α∧ t = τn)

We translate the set of initiates/terminates statements αinitiates/terminates β1when [¬]γ1,1,...,[¬]γ1,p

...

αinitiates/terminates βnwhen [¬]γn,1,...,[¬]γn,q

Table 17.5. Online resources for automated event calculus reasoning

https://docs.google.com/drawings/u/0/d/sgSMgxCi3StqPpFe7gxGF9Q/image?w=454&h=1&rev=1&ac=1&parent=1SBEeJu9f3Hqm8hHfqg_NSnWZIwC_Lp3s

Event calculus planner [103, 104] http://www.iis.ee.ic.ac.uk/~mpsha/planners.html

Event calculus answer set programming [73] http://www.signiform.com/csr/ecas/ (event calculus rules) http://www.tcs.hut.fi/Software/smodels/ (solver)

Discrete Event Calculus Reasoner [70, 71] http://decreasoner.sourceforge.net

TPTP problem library [110] http://www.cs.miami.edu/~tptp/ (see CSR problem domain)

E-RES [37, 38]

http://www2.cs.ucy.ac.cy/~pslogic/

https://docs.google.com/drawings/u/0/d/s6U8X0X2d8K1-9fgC1_LmkQ/image?w=454&h=1&rev=1&ac=1&parent=1SBEeJu9f3Hqm8hHfqg_NSnWZIwC_Lp3s

into the formula

Initiates/Terminates(e,f,t) ≡

(e = α1 ∧ f = β1 ∧ [¬]HoldsAt(γ1,1,t) ∧ ··· ∧ [¬]HoldsAt(γ1,p,t)) ∨ ···∨

(e = α∧ f = β∧ [¬]HoldsAtn,1,t) ∧ ··· ∧ [¬]HoldsAtn,q,t))

An extension to E [35] provides support for indirect effects. The statement γ whenever Γ

where γ is a fluent literal and Γ is a set of fluent literals represents that (1) γ holds at every timepoint at which Γ holds, and (2) every event occurrence that brings about Γ also brings about γ. The language E has been further developed into the language Modular-E [34], which addresses the ramification and qualification problems along with the issues of elaboration tolerance and modularity.

17.7 Automated Event Calculus Reasoning

A number of techniques can be used to perform automated reasoning in the event calculus, including logic programming in Prolog, answer set programming, satisfiability solving, and first-order logic automated theorem proving. Table 17.5 provides pointers to online resources for event calculus reasoning.

17.7.1 Prolog

The original event calculus was formulated as a logic program, and logic programming in Prolog can be used to perform event calculus reasoning. If Prolog is used, however, special care must be taken to avoid infinite loops [10, 45, 87, 93, 94, 98, 103]. Event calculus reasoning can be performed through abductive logic programming [6, 12, 17, 103].

17.7.2 Answer Set Programming

Answer set solvers [3] such as smodels [79] can be used to solve event calculus deduction problems [73]. Answer set solvers can also be used for reasoning in the E language [13].

17.7.3 Satisfiability (SAT) Solving

As a result of the growth in the capabilities of propositional satisfiability (SAT) solvers [92], several event calculus reasoning programs have been built that exploit off-theshelf SAT solvers. The program of Shanahan and Witkowski [109] solves planning problems using SAT solvers. The Discrete Event Calculus Reasoner [70, 71] uses SAT solvers to perform various types of event calculus reasoning including deduction, abduction, postdiction, and model finding. The E-RES program [37, 38] for solving E reasoning problems uses SAT solvers to generate classical models of state constraints.

The Discrete Event Calculus Reasoner uses several techniques to reduce the size of the SAT encoding of event calculus problems [70]:

  1. The domains of arguments to predicates are restricted by using many-sortedlogic.
  2. Atom definitions are expanded [80, p. 361] in order to eliminate a large number of InitiatesTerminatesReleasesTrajectory, and AntiTrajectory ground atoms.
  3. Triply quantified time is eliminated from most event calculus axioms by usingDEC [70].
  4. A compact conjunctive normal form is computed using the technique of renaming subformulas [27, 80, 83].

The Discrete Event Calculus Reasoner distribution includes a library of 99 event calculus reasoning problems that can be solved using the program.

17.7.4 First-Order Logic Automated Theorem Proving

Although first-order logic entailment is undecidable, first-order logic automated theorem proving (ATP) systems [86] have been applied successfully to event calculus deduction problems [77, 78]. But in some cases, the systems require human guidance in the form of lemmas. Event calculus problems are included in the TPTP problem library [110] along with the results of running ATP systems on them.

17.8 Applications of the Event Calculus

An important area of application of the event calculus is commonsense reasoning [74]. Event calculus formalizations have been developed for a number of commonsense domains, including beliefs [46], egg cracking [68, 99, 106], emotions [74], goals and plans [74], object identity [74], space [68, 96], and the zoo world [1, 33, 71]. The event calculus has also been used to model electronic circuits [101] and water tanks [64].

The event calculus can be applied to problems in high-level cognition including natural language understanding and vision. It has been used to build models of story events and states in space and time [69, 72, 76], represent the semantics of natural language tense and aspect [113], and represent event occurrences in stories [31]. The event calculus has been used to implement the higher-level vision component of an upper-torso humanoid robot [102, 107, 108].

Another application area of the event calculus is business systems. The event calculus has been used to track the state of contracts for performance monitoring [18], to model workflows [10, 114], and to improve the flexibility of applications that use electronic payment systems [115]. Other applications of the event calculus include database updates [41], planning [12, 17, 67, 97, 103, 109], and representing legislation [42].

Bibliography

  1. V. Akman, S.T. Erdogan, J. Lee, V. Lifschitz, and H. Turner. Representing the zoo world and the traffic world in the language of the causal calculator. Artificial Intelligence, 153:105–140, 2004.
  2. A.B. Baker. Nonmonotonic reasoning in the framework of situation calculus. Artificial Intelligence, 49(1–3):5–23, 1991.
  3. C. Baral. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge, 2003.
  4. B. Bennett and A.P. Galton. A unifying semantics for time and events. Artificial Intelligence, 153(1–2):13–48, 2004.
  5. D.G. Bobrow. Editor’s preface. Artificial Intelligence, 13(1–2), 1980 (Special issue on Non-monotonic Reasoning).
  6. A. Bracciali and A.C. Kakas. Frame consistency: Computing with causal explanations. In J.P. Delgrande and T. Schaub, editors, Proceedings of the Tenth International Workshop on Non-Monotonic Reasoning, pages 79–87. Whistler, Canada, 2004.
  7. G. Brewka, J. Dix, and K. Konolige. Nonmonotonic Reasoning: An Overview. CSLI, Stanford, CA, 1997.
  8. F.M. Brown, editor. The Frame Problem in Artificial Intelligence: Proceedings of the 1987 Workshop, Los Altos, CA, 1987. Morgan Kaufmann.
  9. I. Cervesato, M. Franceschet, and A. Montanari. A guided tour through some extensions of the event calculus. Computational Intelligence, 16(2):307–347, 2000.
  10. N.K. Cicekli and Y. Yildirim. Formalizing workflows using the event calculus. In M.T. Ibrahim, J. Küng, and N. Revell, editors. Database and Expert Systems ApplicationsLecture Notes in Computer Science, vol. 1873, pages 222–231. Springer, Berlin, 2000.
  11. K.L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors. Logic and Data Bases, pages 293–322. Plenum, New York, 1978.
  12. M. Denecker, L. Missiaen, and M. Bruynooghe. Temporal reasoning with abductive event calculus. In B. Neumann, editor, Proceedings of the Tenth European Conference on Artificial Intelligence, pages 384–388, Chichester, UK, 1992. John Wiley.
  13. Y. Dimopoulos, A.C. Kakas, and L. Michael. Reasoning about actions and change in answer set programming. In V. Lifschitz and I. Niemelä, editors.

Proceedings of the Seventh International Conference on Logic Programming and Nonmonotonic ReasoningLecture Notes in Computer Science, vol. 2923, pages 61–73. Springer, Berlin, 2004.

  1. P. Doherty. Reasoning about action and change using occlusion. In A.G. Cohn, editor, Proceedings of the Eleventh European Conference on Artificial Intelligence, pages 401–405, Chichester, UK, 1994. John Wiley.
  2. P. Doherty and W. Łukaszewicz. Circumscribing features and fluents. In D.M. Gabbay and H.J. Ohlbach, editors. Temporal LogicLecture Notes in Computer Science, vol. 827, pages 82–100. Springer, Berlin, 1994.
  3. P. Doherty, W. Łukaszewicz, and A. Szałas. Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning, 18(3):297–336, 1997.
  4. K. Eshghi. Abductive planning with event calculus. In R.A. Kowalski and K.A. Bowen, editors. Logic ProgrammingProceedings of the Fifth International Conference and Symposium, vol. 1, pages 562–579. MIT Press, Cambridge, MA, 1988.
  5. A.D.H. Farrell, M.J. Sergot, M. Sallé, and C. Bartolini. Using the event calculus for tracking the normative state of contracts. International Journal of Cooperative Information Systems, 14(2–3):99–129, 2005.
  6. J.J. Finger. Exploiting constraints in design synthesis. PhD thesis, Department of Computer Science, Stanford University, Stanford, CA, 1987.
  7. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R.A. Kowalski and K.A. Bowen, editors. Logic Programming: Proceedings of the Fifth International Conference and Symposium, vol. 2, pages 1070–1080. MIT Press, Cambridge, MA, 1988.
  8. M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9(3–4):365–386, 1991.
  9. M. Gelfond and V. Lifschitz. Representing action and change by logic programs. Journal of Logic Programming, 17(2–4):301–321, 1993.
  10. M.R. Genesereth and N.J. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, Palo Alto, CA, 1987.
  11. M.L. Ginsberg and D.E. Smith. Reasoning about action I: A possible worlds approach. Artificial Intelligence, 35(2):165–195, 1988.
  12. E. Giunchiglia, J. Lee, V. Lifschitz, N.C. McCain, and H. Turner. Nonmonotonic causal theories. Artificial Intelligence, 153:49–104, 2004.
  13. E. Giunchiglia and V. Lifschitz. An action language based on causal explanation: Preliminary report. In Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Conference on Innovative Applications of Artificial Intelligence, pages 623–630, Menlo Park, CA, 1998. AAAI Press.
  14. E. Giunchiglia and R. Sebastiani. Applying the Davis–Putnam procedure to nonclausal formulas. In Proceedings of the Sixth Congress of the Italian Association for Artificial Intelligence, Bologna, 1999.
  15. B. Grosof. Default reasoning as circumscription: A translation of default logic into circumscription or maximizing defaults is minimizing predicates. In Proceedings of the Non-Monotonic Reasoning Workshop, pages 115–124, Menlo Park, CA, 1984. AAAI Press.
  16. J. Gustafsson and P. Doherty. Embracing occlusion in specifying the indirect effects of actions. In L.C. Aiello, J. Doyle, and S.C. Shapiro, editors, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, pages 87–98, San Francisco, 1996. Morgan Kaufmann.
  17. A.R. Haas. The case for domain-specific frame axioms. In F.M. Brown, editor, The Frame Problem in Artificial IntelligenceProceedings of the 1987 Workshop, pages 343–348, Los Altos, CA, 1987. Morgan Kaufmann.
  18. H. Halpin, J.D. Moore, and J. Robertson. Automatic analysis of plot for story rewriting. In D. Lin and D. Wu, editors, Proceedings of the 2004 Conference on Empirical Methods in Natural Language Processing, pages 127–133, Barcelona, Spain, 2004.
  19. S. Hanks and D.V. McDermott. Nonmonotonic logic and temporal projection. Artificial Intelligence, 33(3):379–412, 1987.
  20. A.C. Kakas and L. Michael. Modeling complex domains of actions and change. In S. Benferhat and E. Giunchiglia, editors, Proceedings of the Ninth International Workshop on Non-Monotonic Reasoning, pages 380–390, Toulouse, France, 2002.
  21. A.C. Kakas, L. Michael, and R. Miller. Modular-E: an elaboration tolerant approach to the ramification and qualification problems. In S. McIlraith, P. Peppas, and M. Thielscher, editors, Seventh International Symposium on Logical Formalizations of Commonsense Reasoning, Corfu, Greece, 2005.
  22. A.C. Kakas and R. Miller. Reasoning about actions, narratives and ramifications. Linköping Electronic Articles in Computer and Information Science, 2(012), 1997.
  23. A.C. Kakas and R. Miller. A simple declarative language for describing narratives with actions. Journal of Logic Programming, 31(1–3):157–200, 1997.
  24. A.C. Kakas, R. Miller, and F. Toni. An argumentation framework for reasoning about actions and change. In M. Gelfond, N. Leone, and G. Pfeifer, editors. Proceedings of the Fifth International Conference on Logic Programming and Nonmonotonic ReasoningLecture Notes in Computer Science, vol. 1730, pages 78–91. Springer, Berlin, 1999.
  25. A.C. Kakas, R. Miller, and F. Toni. E-RES—A system for reasoning about actions, events and observations. In C. Baral and M. Truszczynski, editors, Proceedings of the Eighth International Workshop on Non-Monotonic Reasoning, Breckenridge, CO, 2000.
  26. R.A. Kowalski. Logic for Problem Solving. North-Holland, New York, 1979.
  27. R.A. Kowalski. Database updates in the event calculus. Technical Report DOC 86/12, London: Imperial College of Science, Technology, and Medicine, 1986.
  28. R.A. Kowalski. Database updates in the event calculus. Journal of Logic Programming, 12:121–146, 1992.
  29. R.A. Kowalski. Legislation as logic programs. In G. Comyn, N.E. Fuchs, and M. Ratcliffe, editors. Logic Programming in Action, Second International Logic Programming Summer SchoolLecture Notes in Computer Science, vol. 636, pages 203–230. Springer, Berlin, 1992.
  30. R.A. Kowalski and F. Sadri. The situation calculus and event calculus compared. In M. Bruynooghe, editor. Logic Programming: The 1994 International Symposium, pages 539–553. MIT Press, Cambridge, MA, 1994.
  31. R.A. Kowalski and F. Sadri. Reconciling the event calculus with the situation calculus. Journal of Logic Programming, 31(1–3):39–58, 1997.
  32. R.A. Kowalski and M.J. Sergot. A logic-based calculus of events. New Generation Computing, 4(1):67–95, 1986.
  33. F. Lévy and J.J. Quantz. Representing beliefs in a situated event calculus. In H. Prade, editor, Proceedings of the Thirteenth European Conference on Artificial Intelligence, pages 547–551, Chichester, UK, 1998. John Wiley.
  34. V. Lifschitz. Computing circumscription. In Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 121–127, Los Altos, CA, 1985. Morgan Kaufmann.
  35. V. Lifschitz. Formal theories of action. In F.M. Brown, editor, The Frame Problem in Artificial Intelligence: Proceedings of the 1987 Workshop, pages 35–57, Los Altos, CA, 1987. Morgan Kaufmann.
  36. V. Lifschitz. Pointwise circumscription. In M.L. Ginsberg, editor. Readings in Nonmonotonic Reasoning, pages 179–193. Morgan Kaufmann, Los Altos, CA, 1987.
  37. V. Lifschitz. Frames in the space of situations. Artificial Intelligence, 46(3):365– 376, 1990.
  38. V. Lifschitz. Circumscription. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors. Nonmonotonic Reasoning and Uncertain ReasoningHandbook of Logic in Artificial Intelligence and Logic Programming, vol. 3, pages 298–352. Oxford University Press, Oxford, 1994.
  39. V. Lifschitz. Book review: M. Shanahan, Solving the frame problem. Artificial Intelligence, 123(1–2):265–268, 2000.
  40. F. Lin. Embracing causality in specifying the indirect effects of actions. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 1985–1993, San Mateo, CA, 1995. Morgan Kaufmann.
  41. F. Lin and R. Reiter. State constraints revisited. Journal of Logic and Computation, 4(5):655–678, 1994.
  42. N.C. McCain and H. Turner. A causal theory of ramifications and qualifications. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 1978–1984, San Mateo, CA, 1995. Morgan Kaufmann.
  43. J. McCarthy. Epistemological problems of artificial intelligence. In R. Reddy, editor, Proceedings of the Fifth International Joint Conference on Artificial Intelligence, pages 1038–1044, Los Altos, CA, 1977. William Kaufmann.
  44. J. McCarthy. Circumscription—a form of non-monotonic reasoning. Artificial Intelligence, 13(1–2):27–39, 1980.
  45. J. McCarthy. Applications of circumscription to formalizing common sense knowledge. In Proceedings of the Non-Monotonic Reasoning Workshop, pages 295–324, Menlo Park, CA, 1984. AAAI Press.
  46. J. McCarthy. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence, 28:89–116, 1986.
  47. J. McCarthy. Generality in artificial intelligence. Communications of the ACM, 30(12):1030–1035, 1987.
  48. J. McCarthy. Elaboration tolerance. In R. Miller and M. Shanahan, editors, Fourth Symposium on Logical Formalizations of Commonsense Reasoning, London, 1998. Queen Mary and Westfield College.
  49. J. McCarthy and P.J. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors. Machine Intelligence, vol. 4, pages 463–502. Edinburgh University Press, Edinburgh, Scotland, 1969.
  50. R. Miller and M. Shanahan. Narratives in the situation calculus. Journal of Logic and Computation, 4(5):513–530, 1994.
  51. R. Miller and M. Shanahan. Reasoning about discontinuities in the event calculus. In L.C. Aiello, J. Doyle, and S.C. Shapiro, editors, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, pages 63–74, San Francisco, 1996. Morgan Kaufmann.
  52. R. Miller and M. Shanahan. The event calculus in classical logic—Alternative axiomatisations. Linköping Electronic Articles in Computer and Information Science, 4(016), 1999.
  53. R. Miller and M. Shanahan. Some alternative formulations of the event calculus. In A.C. Kakas and F. Sadri, editors. Computational Logic: Logic Programming and Beyond: Essays in Honour of Robert A. Kowalski, Part IILecture Notes in Computer Science, vol. 2408, pages 452–490. Springer, Berlin, 2002.
  54. L. Missiaen, M. Bruynooghe, and M. Denecker. Chica, an abductive planning system based on event calculus. Journal of Logic and Computation, 5(5):579– 602, 1995.
  55. L. Morgenstern. Mid-sized axiomatizations of commonsense problems: A case study in egg cracking. Studia Logica, 67:333–384, 2001.
  56. E.T. Mueller. Story understanding through multi-representation model construction. In G. Hirst and S. Nirenburg, editors, Text Meaning: Proceedings of the HLT-NAACL 2003 Workshop, pages 46–53. Association for Computational Linguistics, East Stroudsburg, PA, 2003.
  57. E.T. Mueller. Event calculus reasoning through satisfiability. Journal of Logic and Computation, 14(5):703–730, 2004.
  58. E.T. Mueller. A tool for satisfiability-based commonsense reasoning in the event calculus. In V. Barr and Z. Markov, editors, Proceedings of the Seventeenth International Florida Artificial Intelligence Research Society Conference, pages 147–152, Menlo Park, CA, 2004. AAAI Press.
  59. E.T. Mueller. Understanding script-based stories using commonsense reasoning. Cognitive Systems Research, 5(4):307–340, 2004.
  60. E.T. Mueller. Event calculus answer set programming. http://www. signiform.com/csr/ecas/, 2005.
  61. E.T. Mueller. Commonsense Reasoning. Morgan Kaufmann, San Francisco, 2006.
  62. E.T. Mueller. Event calculus and temporal action logics compared. Artificial Intelligence, 170(11):1017–1029, 2006.
  63. E.T. Mueller. Modelling space and time in narratives about restaurants. Literary and Linguistic Computing, 22(1):67–84, 2007.
  64. E.T. Mueller and G. Sutcliffe. Discrete event calculus deduction using first-order automated theorem proving. In B. Konev and S. Schulz, editors. Proceedings of the Fifth International Workshop on the Implementation of Logics, number ULCS-05-003, pages 43–56. Department of Computer Science, University of Liverpool, Liverpool, UK, 2005.
  65. E.T. Mueller and G. Sutcliffe. Reasoning in the event calculus using first-order automated theorem proving. In I. Russell and Z. Markov, editors. Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, pages 840–841. AAAI Press, Menlo Park, CA, 2005.
  66. I. Niemelä and P. Simons. Smodels—an implementation of the stable model and well-founded semantics for normal logic programs. In J. Dix, U. Furbach, and A. Nerode, editors. Proceedings of the Fourth International Conference on Logic Programming and Nonmonotonic ReasoningLecture Notes in Computer Science, vol. 1265, pages 420–429. Springer, Berlin, 1997.
  67. A. Nonnengart and C. Weidenbach. Computing small clause normal forms. In J.A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning, vol. 1, pages 335–367. Elsevier and MIT Press, Amsterdam and Cambridge, MA, 2001.
  68. E.P.D. Pednault. ADL: Exploring the middle ground between STRIPS and the situation calculus. In R.J. Brachman, H.J. Levesque, and R. Reiter, editors, Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, pages 324–332, San Mateo, CA, 1989. Morgan Kaufmann.
  69. J.A. Pinto and R. Reiter. Temporal reasoning in logic programming: A case for the situation calculus. In D.S. Warren, editor. Logic Programming: Proceedings of the Tenth International Conference, pages 203–221. MIT Press, Cambridge, MA, 1993.
  70. D.A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2:293–304, 1986.
  71. R. Reiter. Circumscription implies predicate completion (sometimes). In D.L. Waltz, editors, Proceedings of the National Conference on Artificial Intelligence, pages 418–420, Menlo Park, CA, 1982. AAAI Press.
  72. R. Reiter. Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press, Cambridge, MA, 2001.
  73. J.A. Robinson and A. Voronkov. Handbook of Automated Reasoning, vols. 1 and 2. Elsevier and MIT Press, Amsterdam and Cambridge, MA, 2001.
  74. F. Sadri. Three recent approaches to temporal reasoning. In A.P. Galton, editor. Temporal Logics and their Applications, pages 121–168. Academic Press, London, 1987.
  75. F. Sadri and R.A. Kowalski. Variants of the event calculus. In L. Sterling, editor, Logic Programming: The Twelfth International Conference, pages 67–81, Cambridge, MA, 1995. MIT Press.
  76. E. Sandewall. Filter preferential entailment for the logic of action in almost continuous worlds. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 894–899, San Mateo, CA, 1989. Morgan Kaufmann.
  77. E. Sandewall. Features and Fluents: The Representation of Knowledge about Dynamical Systems, vol. I. Oxford University Press, Oxford, 1994.
  78. L.K. Schubert. Monotonic solution of the frame problem in the situation calculus: An efficient method for worlds with fully specified actions. In H.E. Kyburg Jr., R.P. Loui, and G.N. Carlson, editors. Knowledge Representation and Defeasible Reasoning, pages 23–67. Kluwer, Dordrecht, 1990.
  79. B. Selman, H.A. Kautz, and D.A. McAllester. Ten challenges in propositional reasoning and search. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, pages 50–54, San Mateo, CA, 1997. Morgan Kaufmann.
  80. M. Shanahan. Prediction is deduction but explanation is abduction. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 1055–1060, San Mateo, CA, 1989. Morgan Kaufmann.
  81. M. Shanahan. Representing continuous change in the event calculus. In L.C. Aiello, editor, Proceedings of the Ninth European Conference on Artificial Intelligence, pages 598–603, London, 1990. Pitman.
  82. M. Shanahan. A circumscriptive calculus of events. Artificial Intelligence, 77:249–284, 1995.
  83. M. Shanahan. Robotics and the common sense informatic situation. In W. Wahlster, editor, Proceedings of the Twelfth European Conference on Artificial Intelligence, pages 684–688, Chichester, UK, 1996. John Wiley.
  84. M. Shanahan. Event calculus planning revisited. In S. Steel and R. Alami, editors. Recent Advances in AI PlanningLecture Notes in Computer Science, vol. 1348, pages 390–402. Springer, Berlin, 1997.
  85. M. Shanahan. Solving the Frame Problem. MIT Press, Cambridge, MA, 1997.
  86. M. Shanahan. A logical formalisation of Ernie Davis’s egg cracking problem. In R. Miller and M. Shanahan, editors, Fourth Symposium on Logical Formalizations of Commonsense Reasoning, London, 1998. Queen Mary and Westfield College.
  87. M. Shanahan. The event calculus explained. In M.J. Wooldridge and M.M. Veloso, editors. Artificial Intelligence TodayRecent Trends and DevelopmentsLecture Notes in Computer Science, vol. 1600, pages 409–430. Springer, Berlin, 1999.
  88. M. Shanahan. The ramification problem in the event calculus. In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, pages 140–146, San Mateo, CA, 1999. Morgan Kaufmann.
  89. M. Shanahan. What sort of computation mediates best between perception and action? In H.J. Levesque and F. Pirri, editors. Logical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter, pages 352–369. Springer, Berlin, 1999.
  90. M. Shanahan. An abductive event calculus planner. Journal of Logic Programming, 44(1–3):207–240, 2000.
  91. M. Shanahan. Abductive event calculus planners [Computer software], 2000.
  92. M. Shanahan. The frame problem. In L. Nadel, editor. Encyclopedia of Cognitive Science, vol. 2, pages 144–150. Nature Publishing Group, London, 2002.
  93. M. Shanahan. An attempt to formalise a non-trivial benchmark problem in common sense reasoning. Artificial Intelligence, 153:141–165, 2004.
  94. M. Shanahan. Perception as abduction: Turning sensor data into meaningful representation. Cognitive Science, 29:103–134, 2005.
  95. M. Shanahan and D.A. Randell. A logic-based formulation of active visual perception. In D. Dubois, C.A. Welty, and M.-A. Williams, editors, Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning, pages 64–72, Menlo Park, CA, 2004. AAAI Press.
  96. M. Shanahan and M. Witkowski. Event calculus planning through satisfiability. Journal of Logic and Computation, 14(5):731–745, 2004.
  97. G. Sutcliffe and C.B. Suttner. The TPTP problem library for automated theorem proving, 2005.
  98. M. Thielscher. Ramification and causality. Artificial Intelligence, 89:317–364, 1997.
  99. K. Van Belleghem, M. Denecker, and D. De Schreye. On the relation between situation calculus and event calculus. Journal of Logic Programming, 31(1– 3):3–37, 1997.
  100. M. van Lambalgen and F. Hamm. The Proper Treatment of Events. Blackwell, Malden, MA, 2005.
  101. J. Wilk. Dynamic workflow pulling the strings. Distinguished Project (MEng). Department of Computing, Imperial College London, London, 2004.
  102. P. Yolum and M.P. Singh. Reasoning about commitments in the event calculus: An approach for specifying and executing protocols. Annals of Mathematics and Artificial Intelligence, 42(1–3):227–253, 2004.

Handbook of Knowledge Representation

Edited by F. van Harmelen, V. Lifschitz and B. Porter

© 2008 Elsevier B.V. All rights reserved

DOI: 10.1016/S1574-6526(07)03018-0

References

  1. ^ Kowalski, Robert; Sergot, Marek (1986-03-01). "A logic-based calculus of events"New Generation Computing4 (1): 67–95. doi:10.1007/BF03037383ISSN 1882-7055S2CID 7584513.
  2. ^ Miller, Rob; Shanahan, Murray (2002), Kakas, Antonis C.; Sadri, Fariba (eds.), "Some Alternative Formulations of the Event Calculus"Computational Logic: Logic Programming and Beyond: Essays in Honour of Robert A. Kowalski Part II, Lecture Notes in Computer Science, Berlin, Heidelberg: Springer, pp. 452–490, doi:10.1007/3-540-45632-5_17ISBN 978-3-540-45632-2, retrieved 2020-10-05
  3. ^ Kowalski, Robert (1992-01-01). "Database updates in the event calculus"The Journal of Logic Programming12 (1): 121–146. doi:10.1016/0743-1066(92)90041-ZISSN 0743-1066.
  4. ^ Eshghi, Kave (1988). "Abductive planning with event calculus"Iclp/SLP: 562–579.
  5. ^ Lambalgen, Hamm (2005). The proper treatment of events. Malden, MA: Blackwell Pub. ISBN 978-0-470-75925-7OCLC 212129657.
  6. ^ Skarlatidis, Anastasios; Paliouras, Georgios; Artikis, Alexander; Vouros, George A. (2015-02-17). "Probabilistic Event Calculus for Event Recognition"ACM Transactions on Computational Logic16 (2): 11:1–11:37. arXiv:1207.3270doi:10.1145/2699916ISSN 1529-3785S2CID 6389629.
  7. ^ Skarlatidis, Anastasios; Artikis, Alexander; Filippou, Jason; Paliouras, Georgios (March 2015). "A probabilistic logic programming event calculus"Theory and Practice of Logic Programming15 (2): 213–245. doi:10.1017/S1471068413000690ISSN 1471-0684S2CID 5701272.

Further reading[edit]

Categories

Wikipedia

Tags: LOGICMOO
     

Child Pages

My Recent Modifications

Copywrite © 2020 LOGICMOO (Unless otherwise credited in page)