Circumscriptive Event Calculus as Answer Set Programming

1 Introduction

The stable model semantics is the mathematical basis of answer set programming [Marek and Truszczy´nski, 1999; Niemel¨a, 1999; Lifschitz, 2008]. Recently, Ferraris, Lee and Lifschitz [2007] presented a general definition of a stable model that applies to the syntax of arbitrary first-order sentences, under which logic programs are viewed as a special class of first-order sentences. The new semantics is similar to the definition of circumscription [McCarthy, 1980; 1986], and can even be characterized in terms of circumscription [Ferraris et al., 2007, Corollary 1]. Essentially the same characterization was also independently given in [Lin and Zhou, 2007].

The opposite direction, turning (parallel) circumscription into the stable model semantics, was shown in [Lee and Lin, 2004; Janhunen and Oikarinen, 2004] limited to the propositional case. The first contribution of this paper is a generalization of the result from [Lee and Lin, 2004]: turning first-order circumscription into the general stable model semantics. Such close relationship between the two formalisms is curious since they have formed rather disparate traditions in knowledge representation. In particular, they have provided different solutions to the frame problem. A group of action formalisms, such as circumscriptive event calculus [Shanahan, 1995] and temporal action logics [Doherty et al., 1998], is based on classical logic, using circumscription to handle the frame problem. On the other hand, the solution provided by answer set programming (ASP), that is carried over to high level action language A [Gelfond and Lifschitz, 1998] and many of its descendants that are based on ASP, uses both default negation (not) and strong negation (¬)-the idea of which is closely related to Reiter's default logic solution [Reiter, 1980]. Interestingly, the development of the event calculus has spanned over both classical logic and logic programming traditions. The original version of the event calculus [Kowalski and Sergot, 1986] was formulated as logic programs but not under the stable model semantics (that was the time before the invention of the stable model semantics). More extensive later developments of the event calculus have been carried out under the classical logic setting via circumscription [Shanahan, 1995; Miller and Shanahan, 1999].

In this paper we show how to embed circumscriptive event calculus into the general language of stable models, and furthermore into answer set programs under certain conditions. The reformulation of the event calculus in the stable model semantics here can be viewed as turning back the event calculus to the logic program tradition, in the modern form of answer set programming. In contrast to the SATbased approaches from [Shanahan and Witkowski, 2004; Mueller, 2004a] which turn circumscription into completion and hence cannot handle certain recursive axioms of the event calculus, we show that the ASP approach can compute the full version of the event calculus assuming that the domain is given and finite. Our work shows that the new stable model semantics is a nonmonotonic formalism as general as circumscription, with the unique advantage of having efficient ASP solvers as computational tools.

Our work is motivated by Mueller's work that is available on the webpage

http://decreasoner.sourceforge.net/csr/ecas/,

where a few example answer set programs are given to illustrate that event calculus like reasoning can be done using ASP solvers. However, this is rather a "proof of concept" and no formal justification is provided there.

2 Review of the Event Calculus

Here we follow the extensive syntax of circumscriptive event calculus described in [Mueller, 2006, Chapter 2].

We assume a many-sorted first-order language, which contains an event sort, a fluent sort, and a timepoint sort. A fluent term is a term whose sort is a fluent; an event term and a timepoint term are defined similarly. A condition is defined recursively as follows:

• A comparison (τ1 < τ2, τ1 ≤ τ2, τ1 ≥ τ2, τ1 > τ2, τ1 = τ2, τ1 ̸= τ2) for terms τ1, τ2 is a condition;
• If f is a fluent term and t is a timepoint term, then HoldsAt(f, t) and ¬HoldsAt(f, t) are conditions;
• If γ1 and γ2 are conditions, then γ1 ∧γ2 and γ1 ∨γ2 are conditions;
• If v is a variable and γ is a condition, then ∃vγ is a condition.

We will use e and ei to denote event terms, f and fi to denote fluent terms, t and ti to denote timepoint terms, and γ and γi to denote conditions. We understand formula F ↔G as shorthand for (F → G) ∧ (G → F); formula ⊤ as shorthand for ⊥ → ⊥; formula ¬F as shorthand for F → ⊥.

An event calculus domain description is defined as 1

where

• Σ is the conjunction of universal closures of axioms of the form

where each of π1 and π2 is either Initiates or Terminates;

• Δ is the conjunction of universal closures of temporal ordering formulas (comparisons between timepoint terms) and axioms of the form

where σ is Started or Stopped and each πj (1 ≤ j ≤ n) is either Initiated or Terminated, which are defined as follows:

↔ (Started(f, t)∧

Initiated(f, t) def

1 The syntax from [Mueller, 2006, Chapter 2] allows CIRC[Θ ; Ab1, . . . , Abn] where Θ is a conjunction of cancellation axioms, which we omit here for simplicity of presentation.

• Ξ is a conjunction of first-order sentences (outside the scope of circumscription) including unique name axioms, state constraints, and one of the two axiomatizations of the event calculus, EC and DEC axioms [Mueller, 2006].

As listed, circumscriptive event calculus descriptions look different from logic programs. The former may contain existential quantifiers; only some parts of the description are circumscribed on selected lists of predicates. Nonetheless, we will see that the differences are not essential.

3 Review of the General Stable Model Semantics

Under the new definition of stable models presented in [Ferraris et al., 2007] that is applicable to arbitrary first-order sentences, a logic program is identified with a universal formula, called the FOL-representation. For example, the FOLrepresentation of the program

is

The review here follows [Ferraris et al., 2010], a journal version of [Ferraris et al., 2007], in which the stable model operator was extended to distinguish between intensional and extensional predicates. Let p be a list of distinct predicate constants p1, . . . , pn, and let u be a list of distinct predicate variables u1, . . . , un of the same length as p. By u ≤ p we denote the conjunction of the formulas ∀x(ui(x) → pi(x)) for all i = 1, . . . n where x is a list of distinct object variables whose length is the same as the arity of pi. Expression u < p stands for (u ≤ p) ∧ ¬(p ≤ u).

For any first-order sentence F , expression SM[F ; p] stands for the second-order sentence 2

where p is the list p1, . . . , pn of predicate constants that are called intensional, u is a list u1, . . . , un of distinct predicate variables corresponding to p, and F ∗ (u) is defined recursively:

• pi(t)∗ = ui(t) for any tuple t of terms;
• F ∗ = F for any atomic formula F that does not contain members of p;

SM[F] defined in [Ferraris et al., 2007] is identical to SM[F ; p] where intensional predicate constants p range over all predicate constants occurring in F. Let σ(F) be the signature consisting of the object, function and predicate constants occurring in F . According to [Ferraris et al., 2007], an interpretation of σ(F) that satisfies SM[F; p] is called a stable model of F, where p is the list of all predicate constants in σ(F). If F contains at least one object constant, an Herbrand stable model of F is called an answer set of F. The answer sets of a logic program Π are defined as the answer sets of the FOL-representation of Π. It turns out that this definition, applied to the syntax of logic programs, is equivalent to the traditional definition of answer sets based on grounding and fixpoint construction [Ferraris et al., 2007].

2 Here we use expression SM[F; p] in place of SMp[F] used in [Ferraris et al., 2010].

The fact that intensional predicates p in SM[F; p] is allowed not to include some predicates occurring in the formula is not essential in view of the following proposition. By pr(F) we denote the list of all predicate constants occurring in F ; by Choice(p) we denote the conjunction of "choice formulas" ∀x(p(x) ∨¬p(x)) for all predicate constants p in p where x is a list of distinct object variables whose length is the same as the arity of p.

Proposition 1 [Ferraris et al., 2010, Theorem 2] If p is a subset of pr(F), then

is logically valid.

However, it will be convenient to describe our main results in this paper by allowing p to be partial.

4 Turning Circumscription and Event Calculus Descriptions into SM

We say that an occurrence of a predicate constant in a formula F is strictly positive if that occurrence is not in the antecedent of any implication. For instance, in (p → q) → r, only r has a strictly positive occurrence.

For any set p of predicate constants and any formulas G and H, we call implication G → H canonical (relative to p) if

• every occurrence of every predicate constant from p in G is strictly positive in G, and
• every occurrence of every predicate constant from p in H is strictly positive in H.

For instance, p(x) → q(x) is a canonical implication relative to {p, q}, while its contraposition ¬q(x) → ¬p(x) is not. Also ∃x p(x) → ∃x q(x) is a canonical implication relative to {p, q}.

By a canonical theory (relative to p) we mean the conjunction of sentences of the form

where x is a list of variables (possibly empty), and G→H is a canonical implication (relative to p). For instance,

is a canonical theory relative to {p, q}, while

is not a canonical theory relative to {p} (it becomes canonical if ∃ is replaced with ∀). Note that any quantifier-free formula (and universal formula) can be equivalently rewritten as a conjunction of canonical implications. One way is by converting to a conjunctive normal form and then rewriting each clause as a canonical implication. An arbitrary sentence that contains existential quantifiers can still be turned into a canonical theory using Skolemization, which preserves satisfiability.

The following proposition shows that, for any canonical theory, circumscription coincides with the stable model semantics.

Proposition 2 For any canonical theory F relative to p,

is logically valid.

For instance, for (3) that is canonical relative to {p, q}, formulas CIRC[(3); p, q] and SM[(3); p, q] are equivalent to each other. Also any sentence F is clearly equivalent to a canonical theory relative to ∅, so that CIRC[F; ∅] is equivalent to SM[F; ∅], which in turn is equivalent to F. On the other hand, for (4) that is not canonical relative to p, CIRC[(4); p] is not equivalent to SM[(4); p]: the only Herbrand model of the signature {p/2, a, b} that satisfies CIRC[(4); p] is {p(a, a)} while the Herbrand models of the same signature that satisfy SM[(4); p] are {p(a, a)} and {p(a, a), p(b, a)}.

It turns out that canonical theories cover a wide range of formalisms based on circumscription. Indeed, in the syntax of the event calculus described in Section 2, all axioms in Σ are already canonical relative to {Initiates,Terminates,Releases}; all axioms in Δ are already canonical relative to {Happens}. Though not described here in detail, one can check that descriptions in temporal action logics are canonical as well.

The following theorem shows a few equivalent reformulations of circumscriptive event calculus in terms of the stable model semantics. We assume that Ξ was already equivalently rewritten so that it contains no strictly positive occurrences of Initiates, Terminates, Releases, Happens (by prepending ¬¬ to such occurrences).

Theorem 1 Given an event calculus description (1), let p be the set of all predicate constants (other than equality and comparisons) occurring in it. The following theories are equivalent to each other: 3

• (a) CIRC[Σ; I, T,R] ∧CIRC[Δ;H] ∧Ξ
• (b) SM[Σ; I, T,R] ∧ SM[Δ;H] ∧Ξ ;
• (c) SM[Σ∧Δ∧Ξ; I, T,R,H] ;
• (d) SM[Σ∧Δ∧Ξ∧Choice(p \ {I, T,R,H}); p].

The equivalence between (a) and (b) is immediate from Proposition 2; the equivalence between (b) and (c) follows from the general splitting theorem for the stable model semantics [Ferraris et al., 2009]; the equivalence between (c) and (d) is immediate from Proposition 1.

5 Turning Event Calculus Descriptions into Answer Set Programs

Like answer set programs, the intensional predicates of formula (d) in Theorem 1 are all the predicates that occur in the event calculus description. On the other hand, the description contains formulas that may not be in the rule form, and may contain existential quantifiers, which are not allowed in answer set programs. In this section we provide a translation of the event calculus into answer set programs so that ASP solvers can be applied for event calculus reasoning. To facilitate the discussion, we introduce the notion of RASPL-1M programs. Syntactically similar codes are accepted by LPARSE 4 -the front-end of several ASP solvers, such as SMODELS 5 , CMODELS 6 , CLASP, and CLINGO 7 .

3 Due to lack of space, we abbreviate the names of circumscribed predicates.

5.1 RASPL-1M Programs

The definition of stable models reviewed in Section 3 can be easily extended to many-sorted first-order languages, similar to the extension of circumscription to many-sorted firstorder languages (Section 2.4 of [Lifschitz, 1994]). We define RASPL-1M programs as a special class of sentences under this extension, which are essentially a many-sorted extension of RASPL-1 programs from [Lee et al., 2008]. We assume that the underlying signature contains an integer sort and contains several built-in symbols, such as integer constants, builtin arithmetic functions, such as +, -, and comparison operators, such as <, ≤, >, ≥. Since we do not need counting aggregates in this paper, for simplicity, we will assume that every "aggregate expression" is an atom or a negated atom. That is, a rule is an expression of the form

(0 ≤ k ≤ m ≤ n ≤ p), where each Ai is an atom, possibly equality or comparison. A program is a finite list of rules.

The "choice rule" of the form {A} ← Body where A is an atom, stands for A ← Body, not not A.

The semantics of a RASPL-1M program is understood by turning it into its corresponding many-sorted FOLrepresentation, as in RASPL-1. The integer constants and built-in symbols are evaluated in the standard way, and we consider only those "standard" interpretations. The answer sets of a RASPL-1M program are the Herbrand interpretations of the signature consisting of the object, function and predicate constants occurring in the program, that satisfy SM[F ; p], where F is the FOL-representation of the program and p is the list of predicate constants occurring in F .

5.2 Turning Event Calculus Descriptions to RASPL-1M Programs

The following procedure turns an event calculus description into a RASPL-1M program. As before, we assume that Ξ was already equivalently rewritten so that it contains no strictly positive occurrences of Initiates, Terminates, Releases, Happens (by prepending ¬¬ to such occurrences).

Definition 1 (Translation EC2ASP) 1. Rewrite all the definitional axioms of the form

4 http://www.tcs.hut.fi/Software/smodels

5 http://www.tcs.hut.fi/Software/smodels .

6 http://www.cs.utexas.edu/users/tag/cmodels.html .

7 http://potassco.sourceforge.net .

• as ∀x(G → p(x)).
• For each axiom that contains existential quantifiers, repeat the following until there are no existential quantifiers:
• (a) Replace maximal negative occurrences of ∃yG(y) in the axiom by G(z) where z is a new variable.
• (b) Replace maximal positive occurrences of ∃yG(x, y) in the axiom where x is the list of all free variables of ∃yG(x, y), by the formula ¬¬pG(x) where pG is a new predicate constant, and add the axiom

1. Add choice formulas ∀x(p(x) ∨ ¬p(x)) for all the predicate constants p except for those in {Initiates, Terminates, Releases, Happens} ∪ p1 ∪ p2 where
2. p1 is the set of all predicate constants p considered in Step 1.
3. p2 is the set of all new predicate constants pG introduced in Step 2.
4. Identifying the formulas with programs with nested expressions [Lifschitz et al., 1999], apply the conversion from [Lifschitz et al., 1999] that turns programs with nested expressions into disjunctive logic programs.

For example, consider DEC5 axiom:

In order to eliminate the positive occurrence of the existential quantifier in the formula, we apply Step 2(b), introducing the formula

and replacing (7) with 8

Step 4 turns these formulas into rules

Due to lack of space, instead of presenting a formal proof, we attempt to give the idea of the translation. Step 1 can be dropped without affecting the correctness, but keeping it yields a simpler program. Step 2 eliminates existential quantifiers. Step 2(a) is one of the steps in prenex normal form conversion. Eliminating positive occurrences of existential quantifiers using new predicates as in Step 2(b) works only if G contains no strictly positive occurrences of predicates to minimize, which is the case with the syntax of the event calculus (Section 2). The following proposition justifies this step of eliminating existential quantifiers.

8 The proof of Theorem 2 uses the fact that ¬¬ is put in front of pG(x) in Step 2(b). Indeed, the translation would be incorrect if ¬¬ was simply dropped.

Proposition 3 Let F be a sentence, let p be a list of distinct predicate constants and let q be a predicate constant that does not belong to the signature of F . For any occurrence of a subformula ∃xG(x, y) of F where y is the list of all free variables in ∃xG(x, y), let F ′ be the formula obtained from F by replacing that occurrence with ¬¬q(y). If G(x, y) contains no strictly positive occurrences of predicate constants from p, then the models of

restricted to the signature of F are precisely the models of SM[F ; p].

Alternatively, if the domain is known and finite, existential quantifiers can be replaced with multiple disjunctions. But this translation is not modular, and such multiple disjunctions need to be updated when the domain changes. Also one would imagine Skolemization, but there is a problem since answer sets are Herbrand models. Consider

which asserts that p is a singleton. If Step 2 was replaced with Skolemization, the translation would yield RASPL-1M program

(b is a Skolem constant), which has no answer sets. Step 3 is to expand the list of intensional predicates to cover all the predicates occurring in the description, as in Proposition 1. The transformation until Step 3 yields a set of implications where each antecedent and consequent is formed from atoms by allowing ¬, ∧, and ∨ nested arbitrarily, similar to the syntax of a program with nested expressions from [Lifschitz et al., 1999]. The well-known transformation that turns a program with nested expressions into a disjunctive logic program from [Lifschitz et al., 1999] can be applied to turn these set of implications into a RASPL-1M program.

Theorem 2 Let T be an event calculus domain description, let σ be the signature consisting of the object, function and predicate constants occurring in T, and let Π be a RASPL-1M program obtained by applying the translation EC2ASP to T. The stable models of Π restricted to σ (disregarding all new predicate constants pG introduced in Step 2 (b)) are precisely the models of T of signature σ.

Turning the resulting RASPL-1M program further into the input language of LPARSE requires minor rewriting, such as moving equality or negated atoms to the body (e.g., not p(t) ← . . . into ← . . . , p(t)), and adding domain predicates in the body for all variables occurring in the rule. 9

6 Experiments

We have implemented a prototype of an ASP-based event calculus reasoner called ECASP, based on the translation in Section 5.2. The implementation, along with the results of our experiments are available at the ECASP homepage:

9 If we are only interested in answer sets, rather than (nonHerbrand) stable models (recall the distinction described in Section 3), UNA axioms can be dropped.

http://reasoning.eas.asu.edu/ecasp .

The system turns an event calculus description into the input language of LPARSE.

6.1 Comparison with SAT-based Approach

The Discrete Event Calculus (DEC) reasoner 10 is an implementation of the event calculus written by Erik Mueller [2004b]. The system reduces event calculus reasoning into satisfiability checking by turning circumscription into predicate completion ([Lifschitz, 1994, Proposition 2]) and then finds the models using SAT solvers. Thanks to the availability of efficient SAT solvers, the system outperforms traditional abductive event calculus planners. Compared to another similar approach in [Shanahan and Witkowski, 2004], the system handles a wider range of reasoning tasks. Out of the 14 benchmark problems from [Shanahan, 1997; 1999], the DEC reasoner was shown to be able to handle 11 of them, while the other approach can handle only one [Mueller, 2004a].

However, since circumscription is not always reducible to completion, the DEC reasoner is unable to handle effect constraints, disjunctive event axioms and compound events. For example, it is well known that the following effect constraints that describe the indirect effects of the agent's walking on the objects that he is holding cannot be handled by predicate completion.

On the other hand, the rule corresponding to this formula can be directly handled by answer set solvers. Indeed, our implementation can handle all event calculus axioms reviewed in Section 2, and solved all 14 benchmark problems.

We compared the performance of (i) the DEC reasoner (v 1.0) running RELSAT (v 2.0) with (ii) ECASP with LPARSE (v 1.1.1)+CMODELS (v 3.75) running RELSAT (v 2.0), (iii) ECASP with GRINGO (v 2.0.2) +CLASP (v 1.1.3) (CLASPD (v 1.1) used for disjunctive programs), and (iv) ECASP with CLINGO (v 2.0.2). ECASP turns the input in the language of the DEC reasoner into the language of LPARSE. Both LPARSE and GRINGO turn the result into a ground ASP program. CMODELS turns this ground program into a set of clauses and then invokes a SAT solver to compute answer sets, while CLASP computes answer sets using the techniques similar to those used in SAT solvers but without generating clauses. CLINGO is a system that combines GRINGO and CLASP in a monolithic way. We have tested many examples and some notable differences are reported in the table. The first five examples are part of the benchmark problems from [Shanahan, 1997; 1999]. The next four are from [Mueller, 2006]. (We increased timepoints to see more notable differences.) All experiments were done on a Pentium machine with 3.00 GHz CPU and 2GB RAM running 64 bit Linux. The reported run times were obtained using the Linux time command, except for the DEC reasoner for which we recorded the times reported by the system. This was to avoid including the time spent by the DEC reasoner in producing output in a neat format. For the DEC reasoner, the times in parentheses are "(encoding time + SAT solving time)." For the others, they are the times spent by each of the grounder and the solver. CMODELS time includes the time spent in converting the ground program generated by LPARSE into a set of clauses, and calling the SAT solver. The time spent by ECASP in translating an event calculus description into a logic program (with variables) is negligible for these problems. '-' denotes that the system cannot solve the example due to the limited expressivity. For instance, BusRide includes disjunctive event axioms, which results in a disjunctive program that cannot be handled by CLINGO.

10 http://decreasoner.sourceforge.net .

Overall, ECASP with CLINGO was the clear winner, followed by ECASP with GRINGO+CLASP. Though the DEC reasoner and CMODELS call the same SAT solver RELSAT, the number of atoms produced by the DEC reasoner is in general much smaller. This is because the DEC reasoner adopts an encoding method (that is based on predicate completion) which avoids a large number of ground instances of atoms such as Initiates(e, f, t), Terminates(e, f, t), and Releases(e, f, t). On the other hand, in several examples, the number of clauses generated by CMODELS is 0, which means that the answer sets were found without calling the SAT solver. This is because for these examples the unique answer set coincides with the well-founded model, which is efficiently computed by CMODELS without calling SAT solvers. Out of the 14 benchmark examples from [Shanahan, 1997; 1999], eight of them belong to this case. Another reason for the good performance of the ASP approach is the efficient grounding methods implemented in LPARSE and GRINGO, which are drastically faster than that of the DEC reasoner.

6.2 Comparison withMueller's ASP Approach

Though no general method was given in Mueller's ASP approach on the webpage cited in the introduction, we observe a few notable differences. One difference is that no choice rules were used in Mueller's examples so that all predicates are to be minimized, which resulted in considering prediction problems only. On the other hand, our approach can handle planning and postdiction problems as well. To solve a planning problem, Happens should be exempt from minimization in logic programs, which can be achieved by adding choice rules for it. More examples can be found from the ECASP homepage.

7 Conclusion

The possibility of embedding circumscriptive theories into the new language of stable models indicates that the latter is as general as the former, and that ASP is a viable approach to computing circumscriptive theories. We observe that the ASP approach can compute the full version of the event calculus, assuming that the domain is known and finite. Thanks to remarkable progress of ASP solvers in computing stable models, together with efficient grounding methods, our experiments showed promising results.

More synergies are expected from the relationship between the event calculus and ASP. In addition to action languages, circumscriptive event calculus can now be regarded as another useful high level action formalism for ASP, addressing some issues that are not well regarded in the context of action languages, such as describing continuous change and hierarchical planning. Embedding both the event calculus and action languages into ASP may be useful in comparing these high level formalisms and even merging the descriptions written in each of them.

Acknowledgements

We are grateful to Vladimir Lifschitz and Erik Mueller for useful comments on the idea of this paper and several pointers to earlier work. We are also grateful to anonymous referees for their useful comments. The authors were partially supported by the National Science Foundation under Grant IIS-0839821.