# action_language_bc_preliminary_report__4948a1d5.pdf

Action Language BC+: Preliminary Report

Joseph Babb and Joohyung Lee School of Computing, Informatics, and Decision Systems Engineering Arizona State University Tempe, AZ, 85287, USA {Joseph.Babb,joolee}@asu.edu

Action languages are formal models of parts of natural language that are designed to describe effects of actions. Many of these languages can be viewed as high level notations of answer set programs structured to represent transition systems. However, the form of answer set programs considered in the earlier work is quite limited in comparison with the modern Answer Set Programming (ASP) language, which allows several useful constructs for knowledge representation, such as choice rules, aggregates, and abstract constraint atoms. We propose a new action language called BC+, which closes the gap between action languages and the modern ASP language. Language BC+ is defined as a high level notation of propositional formulas under the stable model semantics. Due to the generality of the underlying language, BC+ is expressive enough to encompass many modern ASP language constructs and the best features of several other action languages, such as B, C, C+ and BC. Computational methods available in ASP solvers are readily applicable to compute BC+, which led us to implement the language by extending system CPLUS2ASP.

Introduction Action languages are formal models of parts of natural language that are used for describing properties of actions. The semantics of action languages describe transition systems directed graphs whose vertices represent states and whose edges represent actions that affect the states. Many action languages, such as languages A (Gelfond and Lifschitz 1993) and B (Gelfond and Lifschitz 1998, Section 5), can be viewed as high level notations of answer set programs structured to represent transition systems. Languages C (Giunchiglia and Lifschitz 1998) and C+ (Giunchiglia et al. 2004) are originally defined in terms of nonmonotonic causal theories, but their definite fragments can be equivalently turned into logic programs as well, leading to the implementation CPLUS2ASP, which uses ASP solvers for computation (Babb and Lee 2013). The main advantage of using action languages over ASP programs is their structured abstract representations for describing transition systems, which allows their users to focus on high level descriptions and avoids the cryptic syntax

Copyright c 2015, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

and the recurring pattern of ASP rules for representing transition systems. However, the existing work on action languages have two limitations. First, they do not allow many useful ASP constructs, such as choice rules, aggregates, abstract constraint atoms, and external atoms, that have recently been introduced into ASP and have been shown to be very useful. The inability to use these modern constructs in action languages is what often prevents the users from writing in action languages, and instead forces them to write in the language of ASP directly. Another issue is that even when we do not use such constructs, there are certain limitations that each action language has in comparison with another. For instance, in language B, the frame problem is solved by enforcing in the semantics that every fluent be governed by the commonsense law of inertia, which makes it difficult to represent fluents whose behavior is described by defaults other than inertia. Languages C and C+ do not have this limitation, but instead they do not handle Prolog-style recursive definitions, such as transitive closure, available in B. The recently proposed language BC (Lee, Lifschitz, and Yang 2013) combines the attractive features of B and C+, but it is not a proper generalization. In comparison with C+, it does not allow us to describe complex dependencies among actions, thus it is unable to describe several concepts that C+ is able to express naturally, such as defeasible causal laws (Giunchiglia et al. 2004, Section 4.3) and action attributes (Giunchiglia et al. 2004, Section 5.6). We present a simple solution to these problems. The main idea is to define an action language in terms of a general stable model semantics, which has not been considered in the work of action languages. We present a new action language called BC+, which is defined as a high level notation of propositional formulas under the stable model semantics in (Ferraris 2005). It has been well studied in ASP that several useful constructs, such as aggregates, abstract constraint atoms, and conditional literals, can be identified with abbreviations of propositional formulas (e.g.,(Ferraris 2005; Pelov, Denecker, and Bruynooghe 2003; Son and Pontelli 2007; Harrison, Lifschitz, and Yang 2014)). Thus, BC+ employs such constructs as well. Further, it is more expressive than the other action languages mentioned above, allowing them to be easily embedded. The computation of BC+ is carried out by ASP solvers, which is implemented by modify-

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence

ing system CPLUS2ASP (Babb and Lee 2013), which was originally designed to compute C+ using ASP solvers. The paper is organized as follows. We first review propositional formulas under the stable model semantics, and how they express the concept of defaults in the presence of uniqueness and existence of value constraints. Next we present the syntax and the semantics of BC+, as well as a useful fragment and abbreviations. We also show how propositional formulas under the stable model semantics can be viewed as a special case of BC+. Then we show how each of BC and C+ can be embedded in BC+, and explain the advantages of BC+ over the two languages.

Preliminaries According to (Ferraris 2005), stable models of a propositional formula are defined as follows. The reduct F X of a propositional formula F relative to a set X of atoms is the formula obtained from F by replacing every maximal subformula that is not satisfied by X with . Set X is called a stable model of F if X is a minimal set of atoms satisfying F X. It has been shown that logic programs can be identified with propositional formulas under the stable model semantics in the form of conjunctions of implications. Throughout this paper, we consider propositional formulas whose signature σ consists of atoms of the form c=v, 1 where c is called a constant and is associated with a finite set Dom(c) of cardinality 2, called the domain, and v is an element of its domain. If the domain of c is {f, t} then we say that c is Boolean; we abbreviate c = t as c and c = f as c. Bartholomew and Lee [2014] show that this form of propositional formulas is useful to express the concept of default values on multi-valued fluents. By UECσ ( Uniqueness and Existence Constraint ) we denote the conjunction of

v =w : v,w Dom(c) (c = v c = w), (1)

v Dom(c) c = v . (2)

for all constants c of σ. It is clear that an interpretation of σ that satisfies UECσ can be identified with a function that maps each constant c into an element in its domain.

Example 1 Consider a signature σ to be {c=1, c=2, c= 3}, where c is a constant and Dom(c) = {1, 2, 3}. UECσ is

(c=1 c=2) (c=2 c=3) (c=1 c=3) (c=1 c=2 c=3).

Let F1 be (c = 1 (c = 1)) UECσ. Due to UECσ, each of {c = 1}, {c = 2}, and {c = 3} is a model of F1, but {c = 1} is the only stable model of F1.2 This is because the reduct F {c=1} 1 is equivalent to c=1, for which {c=1} is the minimal model. On the other hand, for instance, the reduct

1Note that c = v is an atom in the propositional signature, and not an equality in first-order logic. 2We identify an interpretation with the set of atoms that are true in it.

F {c=2} 1 is equivalent to , for which the minimal model is , not {c=2}. Let F2 be F1 conjoined with c=2. Similarly, we can check that the only stable model of F2 is {c = 2}. This illustrates the nonmonotonicity of the semantics. Note that the presence of double negations is essential in (2). Without them, F1 would have three stable models: {c=1}, {c=2}, and {c=3}. In ASP, formulas of the form F F are called choice formulas and denoted by {F}ch. For example, F1 above can be written as {c = 1}ch UECσ. As shown in Example 1, in the presence of UECσ, a formula of the form {c = v}ch expresses that c has the value v by default, which can be overridden in the presence of other evidence (Bartholomew and Lee 2014). Aggregates in ASP can be understood as shorthand for propositional formulas as shown in (Ferraris 2005). For instance, the count aggregate expresion 2{p, q, r} is shorthand for (p q) (q r) (p r).

Syntax of BC+ The syntax of language BC+ is similar to the syntax of C+. The following description repeats the syntax description in Section 4.2 from (Giunchiglia et al. 2004). In language BC+, constants are divided into two groups: fluent constants and action constants. Fluent constants are further divided into regular and statically determined. A fluent formula is a formula such that all constants occurring in it are fluent constants. An action formula is a formula that contains at least one action constant and no fluent constants. A static law is an expression of the form caused F if G (3) where F and G are fluent formulas. An action dynamic law is an expression of the form (3) in which F is an action formula and G is a formula. A fluent dynamic law is an expression of the form caused F if G after H (4) where F and G are fluent formulas and H is a formula, provided that F does not contain statically determined constants. Static laws can be used to talk about causal dependencies between fluents in the same state; action dynamic laws can be used to express causal dependencies between concurrently executed actions; fluent dynamic laws can be used for describing direct effects of actions. A causal law is a static law, an action dynamic law, or a fluent dynamic law. An action description is a finite set of causal laws. The formula F in each of causal laws (3) and (4) is called the head of the causal law.

Semantics of BC+ For any action description D, we define a sequence of propositional formulas PF0(D), PF1(D), . . . so that the stable models of PFm(D) represent paths of length m in the transition system corresponding to D. The signature σD,m of PFm(D) has the constants i:c such that

Figure 1: The transition system described by SD.

i {0, . . . , m} and c is a fluent constant of D, and i {0, . . . , m 1} and c is an action constant of D. The domain of i:c is the same as the domain of c. By i:F we denote the result of inserting i: in front of every occurrence of every constant in formula F. The translation PFm(D) is the conjunction of i:F i:G (5) for every static law (3) in D and every i {0, . . . , m}, and (5) for every action dynamic law (3) in D and every i {0, . . . , m 1};3

i+1:F (i+1:G) (i:H) (6) for every fluent dynamic law (4) in D and every i {0, . . . , m 1}; {0:c=v}ch (7) for every regular fluent constant c and every v Dom(c); UECσD,m, which can also be abbreviated using the count aggregate as the conjunction of

1{i:c=v1, . . . , i:c=vm}1 (8)

for every i:c in σD,m and every v1, . . . , vm in Dom(i:c). Note how the translation PFm(D) treats regular and statically determined fluent constants in different ways: formulas (7) are included only when c is regular. Statically determined fluents are useful for describing defined fluents, whose value is determined by the fluents in the same state only. We refer the reader to (Giunchiglia et al. 2004, Section 5) for more details. As an example, the transition system shown in Figure 1 can be described by the following action description SD, where p is a Boolean regular fluent constant and a is a Boolean action constant. caused p if after a, caused {a}ch, caused { a}ch, caused {p}ch if after p, caused { p}ch if after p,

The translation PFm(SD) turns this description into the following propositional formulas. The first line of (9) is turned into the formulas

3We identify F G with G F.

(0 i < m), the second and the third lines into

{i:a}ch, {i: a}ch (10)

(0 i < m), and the fourth and the fifth lines into

{i+1:p}ch i:p, {i+1: p}ch i: p (11) (0 i < m). In addition,

{0:p}ch, {0: p}ch

come from (7), and

1{i:p, i: p}1 (0 i m), 1{i:a, i: a}1 (0 i < m)

come from (8). For every stable model X of PF0(D), the set of fluent formulas c=v such that 0 : c=v belongs to X is a state of D. In view of the uniqueness and existence of value constraints, for every state s and every fluent constant c, there is exactly one v such that c=v belongs to s. For every stable model X of PF1(D), D includes the transition s0, e, s1 , where si (i = 0, 1) is the set of fluent formulas c=v such that i : c=v belongs to X, and e is the set of action formulas c=v such that 0 : c=v belongs to X. The soundness of this definition is guaranteed by the following fact:

Theorem 1 For every transition s0, e, s1 , s0 and s1 are states.

The stable models of PFm(D) represent the paths of length m in the transition system corresponding to D. For m = 0 and m = 1, this is clear from the definition of a transition system; for m > 1 this needs to be verified as the following theorem shows. For every set X of elements of the signature σD,m, let Xi (i < m) be the triple consisting of the set consisting of atoms A such that i:A belongs to X, and A contains fluent constants, the set consisting of atoms A such that i:A belongs to X, and A contains action constants, and the set consisting of atoms A such that (i + 1):A belongs to X, and A contains fluent constants.

Theorem 2 For every m 1, X is a stable model of PFm(D) iff X0, . . . , Xm 1 are transitions.

For example, {0 : p, 0 : a, 1 : p, 1 : a, 2 : p} is a stable model of PF2(SD), and each of p, a, p and p, a, p is a transition of SD.

Useful Abbreviations Like C+, several intuitive abbreviations of causal laws can be defined for BC+. Expression default c = v if F stands for caused {c = v}ch if F. 4 This abbreviation is intuitive in view of the reading of choice formulas in the presence of uniqueness and existence of value constraints we introduced earlier (recall Example 1). Similarly,

default c=v if F after G

4Here and after, we often omit if F if F is .

stands for caused {c=v}ch if F after G. Other abbreviations of BC+ causal laws are defined similarly as in C+.

If c is a Boolean action constant, we express that F is an effect of executing c by c causes F, which stands for the fluent dynamic law caused F if after c. If c is an action constant, the expression exogenous c stands for the action dynamic laws default c=v for all v Dom(c). If c is a regular fluent constant, the expression inertial c stands for the fluent dynamic laws default c=v after c=v for all v Dom(c). constraint F where F is a fluent formula stands for the static law caused if F. always F stands for the fluent dynamic law caused if after F. nonexecutable F if G stands for the fluent dynamic law caused if after F G.

Embedding Formulas under SM in BC+

We defined the semantics of BC+ by reducing the language to propositional formulas under the stable model semantics. The reduction in the opposite direction is also possible. Any propositional formula F under the stable model semantics can be turned into an action description in BC+ by treating every atom of F as a statically determined fluent constant with Boolean values, rewriting F as the static law caused F, and adding default c=f for every constant c.

Proposition 1 The stable models of a propositional formula F are exactly the states of the transition system described by the BC+ description obtained from F by the above translation.

It is known that the problem of determining the existence of stable models of propositional formulas is ΣP 2 -complete (Ferraris 2005). The same complexity applies to BC+ in view of Proposition 1. On the other hand, from the translation PFm(D), a useful fragment in NP can be defined based on the known results in ASP. The following is an instance. We say that action description D is definite if the head of every causal law is either , an atom c = v, or a choice formula {c = v}ch. We say that a formula is a simple conjunction if it is a conjunction of atoms and count aggregates, each of which may be preceded by negation. A simple action description is a definite action description such that G in every causal law (3) is a simple conjunction, and G and H in every causal law (4) are simple conjunctions. The next section presents an example of a simple action description.

Example: Blocks World

An attractive feature of BC+ is that aggregates (or more generally, abstract constraints) are directly usable in causal laws because they are understood as abbreviations of propositional formulas (Ferraris 2005; Pelov, Denecker, and Bruynooghe 2003; Son and Pontelli 2007; Lee and Meng

2009). We illustrate this advantage by formalizing an elaboration of the Blocks World from (Lee, Lifschitz, and Yang 2013) by a simple BC+ description. Let Blocks be a non-empty finite set of symbols (block names) that does not include the symbol Table. The action description below uses the following fluent and action constants: for each B Blocks, regular fluent constant Loc(B) ( Location ) with the domain Blocks {Table}, and statically determined Boolean fluent constant In Tower(B); for each B Blocks, Boolean action constant Move(B); for each B Blocks, action constant Dest(B) ( Destination ) with the domain Blocks {Table} {None}, where None is an auxiliary symbol for an undefined value. In the list of static and dynamic laws below, B, B1 and B2 are arbitrary elements of Blocks, and L is an arbitrary element of Blocks {Table}. Blocks are not on itself: constraint Loc(B) =B. The definition of In Tower(B): caused In Tower(B) if Loc(B)=Table, caused In Tower(B) if Loc(B)=B1 In Tower(B1), default In Tower(B). Blocks don t float in the air: constraint In Tower(B). No two blocks are on the same block: constraint {b : Loc(b)=B}1. Only k towers are allowed to be on the table (k is a positive integer): constraint {b : Loc(b)=Table}k. The effect of moving a block: Move(B) causes Loc(B)=L if Dest(B)=L A block cannot be moved unless it is clear: nonexecutable Move(B) if Loc(B1)=B. Concurrent actions are limited by the number g of grippers: always {b : Move(b)}g. The commonsense law of inertia: inertial Loc(B). Actions are exogenous: exogenous Move(B), exogenous Dest(B). Dest is an attribute of Move: always Dest(B)=None Move(B). Besides the inability to represent aggregates, other action languages have difficulties in representing this example. Languages C and C+ do not allow us to represent the recursive definition of In Tower. Languages B and BC do not allow us to represent action attributes like Dest. (The usefulness of attributes in expressing elaboration tolerance was discussed in (Lifschitz 2000).) In the following two sections, we compare BC+ with BC and C+.

Relation to Language BC Review: BC The signature σ for a BC description D is defined the same as in BC+ except that every action constant is assumed to be Boolean. The main syntactic difference between BC causal laws and BC+ causal laws is that the former allows only the conjunction of atoms in the body, and distinguishes between if and ifcons clauses. A BC static law is an expression of the form

A0 if A1, . . . , Am ifcons Am+1, . . . , An (12)

(n m 0), where each Ai is an atom containing a fluent constant. It expresses, informally speaking, that every state satisfies A0 if it satisfies A1, . . . , Am, and Am+1, . . . , An can be consistently assumed. A BC dynamic law is an expression of the form

A0 after A1, . . . , Am ifcons Am+1, . . . , An (13)

(n m 0), where (i) A0 is an atom containing a regular fluent constant, (ii) each of A1, . . . , Am is an atom containing a fluent constant, or a=t where a is an action constant, and (iii) Am+1, . . . , An are atoms containing fluent constants. It expresses, informally speaking, that the end state of any transition satisfies A0 if its beginning state and its action satisfy A1, . . . , Am, and Am+1, . . . , An can be consistently assumed about the end state. An action description in language BC is a finite set consisting of BC static and BC dynamic laws. The semantics of BC is defined by using reduction PFBC m to a sequence of logic programs under the stable model semantics. The signature σD,m of PFBC m is defined the same as that of PFm defined in Section Semantics of BC+. For any BC action description D, by PFBC m (D) we denote the conjunction of

i:A0 i : (A1 Am Am+1 An) (14) for every BC static law (12) in D and every i {0, . . . , m};

(i + 1):A0 i:(A1 Am) (i+1):( Am+1 An) (15) for every BC dynamic law (13) in D and every i {0, . . . , m 1}; the formula i : (a = t a = f) for every action constant a and every i {0, . . . , m 1}; the formula (7) for every regular fluent constant c and every element v Dom(c); the formulas (1) and (2) for every constant i:c in σD,m. Note how the translations (14) and (15) treat if and ifcons clauses differently by either prepending double negations in front of atoms or not. In BC+, only one if clause is enough since the formulas are understood under the stable model semantics.

Embedding BC in BC+ Despite the syntactic differences, language BC can be easily embedded in BC+ as follows. For any BC description D, we define the translation bc2bcp(D), which turns a BC description into an equivalent BC+ description as follows: replace every causal law (12) with

caused A0 if A1 Am Am+1 An; (16) replace every causal law (13) with

caused A0 if Am+1 An after A1 Am;

add the causal laws exogenous a for every action constant a.

Theorem 3 For any action description D in language BC, the transition system described by D is identical to the transition system described by the description bc2bcp(D) in language BC+.

Advantages of BC+ over BC In BC, every action is assumed to be Boolean, and action dynamic laws are not available. This prevents us from describing defeasible causal laws (Giunchiglia et al. 2004, Section 4.3) and action attributes (Giunchiglia et al. 2004, Section 5.6), which BC+ and C+ are able to express naturally. Also, syntactically, BC is not expressive enough to describe dependencies among actions. For a simple example, in BC+ we can express that action a1 is not executable when a2 is not executed at the same time by the fluent dynamic law

caused after a1 a2,

but this not syntactically allowed in BC. On the other hand, the presence of choice formulas in the head of BC+ causal laws and the different treatment of A and A in the bodies may look subtle to those who are not familiar with the stable model semantics for propositional formulas. Fortunately, in many cases one can hide these constructs by using the default proposition in BC+ as the following example illustrates. Consider the leaking container example from (Lee, Lifschitz, and Yang 2013) in which a container loses k units of liquid by default. This example was used in that paper to illustrate the advantages of BC over B that is able to express defaults other than inertia. In this domain, the default decrease of Amount over time can be represented in BC+ using the default proposition

default Amount=x after Amount=x+k, (17)

which stands for fluent dynamic law

caused {Amount=x}ch after Amount=x+k,

which can be further turned into propositional formulas

{i+1:Amount=x}ch i:Amount=x+k (18)

(i < m). On the other hand, the abbreviation (17) in BC stands for the causal law

caused Amount=x after Amount=x+k ifcons Amount=x,

Notation: s, s ranges over {Switch1, Switch2}; x, y ranges over {Up, Dn}. Regular fluent constants: Domains: Status(s) {Up, Dn} Action constants: Domains: Flip(s) Boolean

Causal laws:

Flip(s) causes Status(s)=x if Status(s)=y (x = y) caused Status(s)=x if Status(s )=y (s = s , x = y) inertial Status(s) exogenous Flip(s)

Figure 2: Two Switches

which is further turned into

i+1:Amount=x i:Amount=x+k (i+1:Amount=x)

(i < m), which is strongly equivalent to (18). Our experience is that, in most cases, instead of remembering the subtle difference between if and if cons clauses in BC, it is more intuitive to use the default proposition in BC+.

Relation to C+ Due to the space limitation, we refer the reader to (Giunchiglia et al. 2004) for the review of C+. The syntax of C+ has the same form of causal laws as BC+.

Embedding Definite C+ in BC+ We say that C+ action description D is definite if the head of every causal law is either or an atom c=v. For any definite C+ description D, we define the translation cp2bcp(D), which turns a C+ description into BC+, as follows:

replace every C+ causal law (3) with

caused F if G;

replace every C+ causal law (4) with

caused F if G after H.

The following theorem asserts the correctness of this translation.

Theorem 4 For any definite action description D in language C+, the transition system described by D is identical to the transition system described by the description cp2bcp(D) in language BC+.

Advantages of BC+ over C+ Recall that the syntax of BC+ is identical to the syntax of C+, but its semantics is given via the stable model semantics. An advantage of this approach is that it allows the advances in ASP directly usable in the context of action languages. We already observed that being able to use aggregates in BC+ provides a succinct representation of the Blocks World domain. However, the expansion of choice formulas and aggregates into propositional formulas as in the stable model

semantics does not work in C+ as defined in (Giunchiglia et al. 2004), which is based on nonmonotonic causal theories. The embedding of C+ in BC+ tells us that if clauses always introduce double negations, whose presence do not necessarily lead to minimal models. This accounts for the fact that the definite fragment of C+ does not handle the concept of transitive closure correctly. The inability to consider minimal models in such cases introduce some unintuitive behavior of C+ in representing causal dependencies among fluents. Consider two switches which can be flipped but cannot be both up or down at the same time. If one of them is down and the other is up, the direct effect of flipping only one switch is changing the status of that switch, and the indirect effect is changing the status of the other switch. This domain can be represented in BC+ as shown in Figure 2. The description in BC+ has the following four transitions possible from the initial state where Switch1 is Dn and Switch2 is Up:

{St(Sw1)=Dn, St(Sw2)=Up}, { Flip(Sw1), Flip(Sw2)}, {St(Sw1)=Dn, St(Sw2)=Up} ,

{St(Sw1)=Dn, St(Sw2)=Up}, {Flip(Sw1), Flip(Sw2)}, {St(Sw1)=Up, St(Sw2)=Dn} ,

{St(Sw1)=Dn, St(Sw2)=Up}, { Flip(Sw1), Flip(Sw2)}, {St(Sw1)=Up, St(Sw2)=Dn} ,

{St(Sw1)=Dn, St(Sw2)=Up}, {Flip(Sw1), Flip(Sw2)}, {St(Sw1)=Up, St(Sw2)=Dn} .

The second and the third transitions exhibit the indirect effect of the action Flip. If this description is understood in C+, five transitions are possible from the same initial state: in addition to the four transitions above,

{St(Sw1)=Dn, St(Sw2)=Up}, { Flip(Sw1), Flip(Sw2)}, {St(Sw1)=Up, St(Sw2)=Dn} is also a transition because, according to the semantics of C+, this is causally explained by the cyclic causality. Obviously, this is unintuitive.

Conclusion We implemented language BC+ by modifying system CPLUS2ASP (Babb and Lee 2013), which was originally designed to compute the definite fragment of C+ using ASP solvers. As the translation PFC+ m (D) for C+ is similar to the translation PFm(D) for BC+, modifying this translation to accept BC+ input is straightforward. Besides the action languages considered in this paper, language K (Eiter et al. 2004) is also defined via ASP. Since K assumes knowledge-states, it is not directly comparable to BC+ which assumes world-states. A further extension of BC+ is possible. It is straightforward to extend BC+ to the first-order level, by using the firstorder stable model semantics from (Ferraris, Lee, and Lifschitz 2011) or its extension with generalized quantifiers (Lee and Meng 2012) in place of propositional formulas. This will allow BC+ to include more general constructs, such as constraint atoms, external atoms, nonmonotonic dl-atoms, as they are instances of generalized quantifiers as shown in (Lee and Meng 2012).

Acknowledgements We are grateful to Michael Bartholomew, Vladimir Lifschitz, and the anonymous referees for their useful comments. This work was partially supported by the National Science Foundation under Grant IIS-1319794 and by the South Korea IT R&D program MKE/KIAT 2010-TD-300404-001, and the Brain Pool Korea program.

References Babb, J., and Lee, J. 2013. Cplus2ASP: Computing action language C+ in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 122 134. Bartholomew, M., and Lee, J. 2014. Stable models of multivalued formulas: partial vs. total functions. In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), 583 586. Eiter, T.; Faber, W.; Leone, N.; Pfeifer, G.; and Polleres, A. 2004. A logic programming approach to knowledge-state planning: Semantics and complexity. ACM Trans. Comput. Log. 206 263. Ferraris, P.; Lee, J.; and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175:236 263. Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 119 131. Gelfond, M., and Lifschitz, V. 1993. Representing action and change by logic programs. Journal of Logic Programming 17:301 322. Gelfond, M., and Lifschitz, V. 1998. Action languages.5 Electronic Transactions on Artificial Intelligence 3:195 210. Giunchiglia, E., and Lifschitz, V. 1998. An action language based on causal explanation: Preliminary report. In Proceedings of National Conference on Artificial Intelligence (AAAI), 623 630. AAAI Press. Giunchiglia, E.; Lee, J.; Lifschitz, V.; Mc Cain, N.; and Turner, H. 2004. Nonmonotonic causal theories. Artificial Intelligence 153(1 2):49 104. Harrison, A. J.; Lifschitz, V.; and Yang, F. 2014. The semantics of gringo and infinitary propositional formulas. In Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR. Lee, J., and Meng, Y. 2009. On reductive semantics of aggregates in answer set programming. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 182 195. Lee, J., and Meng, Y. 2012. Stable models of formulas with generalized quantifiers.6 In Proceedings of International Workshop on Nonmonotonic Reasoning (NMR). Lee, J.; Lifschitz, V.; and Yang, F. 2013. Action language BC: Preliminary report. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI).

5http://www.ep.liu.se/ea/cis/1998/016/ 6http://peace.eas.asu.edu/joolee/papers/smgq-nmr.pdf

Lifschitz, V. 2000. Missionaries and cannibals in the Causal Calculator. In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), 85 96. Pelov, N.; Denecker, M.; and Bruynooghe, M. 2003. Translation of aggregate programs to normal logic programs. In Proceedings Answer Set Programming. Son, T. C., and Pontelli, E. 2007. A constructive semantic characterization of aggregates in answer set programming. TPLP 7(3):355 375.