A Simple Formalization of Actions Using Circumscription

1 Introduction

Solving the frame problem-the problem of represent­ ing succinctly what remains unchanged as a result of performing an action-is one of major challenges in the logical approach to Artificial Intelligence. This problem was one of the motivating factors behind the emergence of several nonmonotonic formalisms in the 1980s. It has led, in particular , to the development of circumscription in [McCarthy, 1980] and [McCarthy, 1986]. Circumscrip­ tion is a syntactic transformation that expresses a min­ imality property of models. The idea was to solve the frame problem by postulating that, whenever an action is executed, the "difference" between the two states of the world, before and after the event, is minimal. How­ ever, the straightforward formalization based on this idea turned out to be inadequate [Hanks and McDermott, 1987].

In this paper, we present a simple formalization of ac­ tions using the framework of nested abnormality theories (NATs) [Lifschitz, 1995], a formalism based on circum­ scription. The main feature of this framework is that the effects of various circumscriptions are confined to the parts of the axiom set called "blocks." As a result, the circumscriptions that solve the frame problem become rather simple, and, in several examples, we will be able to eliminate all their second-order quantifiers using existing techniques for computing circumscriptions. These exam­ ples involve actions with indirect effects and, in one case, these effects are nondeterministic. One of the two meth­ ods for computing circumscriptions employed here is a generalization of predicate completion [Lifschitz, 1993] and the other is based on the SCAN algorithm [Gabbay and Ohlbach, 1992].

The idea behind the approach to the frame problem presented here is closest to that of Winslett [1988] . The main difference is that Winslett's formalization is in terms of theory update, and ours includes the full ex­ pressive power of the situation calculus. Combining the ideas of [Winslett, 1988] with the situation calculus is achieved by the use of NATs.

Another closely related .direction of research is de­ scribed in [Lin and Shoham, 1991] and [Lin and Reiter , 1994]. Central to the formalization presented there is a minimality condition formulated in terms of models. To obtain meaningful conclusions with their formalization, Lin, Shoham and Reiter need to impose certain consis­ tency conditions and on include certain "tree axioms" (that impose a tree structure to the universe of situa­ tions). In contrast, the use of circumscription described in this paper allows us to dispense with the consistency conditions and the tree axioms.

Also, this paper differs from earlier work in that we in­ vestigate the applicability of symbolic methods to com­ puting the circumscriptions involved in the solution to the frame problem-an issue not considered by Winslett or by Lin, Shoham and Reiter.

The rest of the paper is organized as follows . In the next two sections, we review the notion of a causal the­ ory introduced in [Lin and Reiter, 1994] and give a few examples. Section 4 introduces the new formalization. In Section 5, we illustrate via examples how the effect of circumscriptions can be computed by syntactic manip­ ulations and using SCAN. In Section 6, we relate this paper to action languages [Gelfond and Lifschitz, 1993] and indicate directions for future work.

For the terminology and notation related to circum­ scription, the reader is referred to [Lifschitz, 1993].

2 Causal Theories

For clarity, we will present the new formalization in the context of a simple class of theories called "causal." This class of theories is essentially the same as that defined in [Lin and Reiter, 1994].

The formalism is based on the situation calculus [Mc­ Carthy and Hayes, 1969]. Consider a first-order language with object variables for situations and actions, and pos­ sibly variables of other sorts. In this section, by s we will denote a situation variable, by a an action variable, and by x, y tuples of distinct variables of other sorts. The nonlogical constants of the language are

• binary function constant Result; Result( a, s) is the situation obtained by performing action a in situa­ tions;
• binary predicate constant Poss; Poss(a, s) expresses that it is possible to execute a in situation s;
• function constants (some of them possibly of arity 0) called action symbols; for an action symbol A, A( x) is an action term;
• predicate constants called fluent symbols; for a flu­ ent symbol F, F ( x, s) is an atomic formula.

A language of this kind will be called a causal language. Two groups of axioms will be allowed in a causal theory-"effect axioms" and "ramification constraints." In order to describe the syntactic form that these axioms may have, we need the following definition. A formula <I> is a simple state formula if every occurrence of a sit­ uation term in <I> is an occurrence of the same variable s as the last argument of a fluent symbol. Clearly, So, Result and Poss cannot occur in a simple state formula.

A set of axioms in a causal language is a causal theory if it consists of

• some effect axioms of the forms

where w(x, a, s) is a simple state formula,

• some ramification constraints, that are assumed to be simple state formulas that do not contain action terms.

3 Examples

We will now illustrate the definitions introduced so far with a few examples . The first example is reproduced from [Lin and Reiter, 1994].

Example 1. Consider a blocks world domain in which the only actions possible are painting blocks with differ­ ent colours . To describe this domain, we first introduce an action term paint(x, y) that stands for the action of painting block x with colour y. The following effect ax­ iom describes what this action does:

Note that this axiom can be rewritten as

so that it will have the form of the effect axioms given in ( 1) .

The only ramification constraint that we have for this domain is that a block can have just one colour. This constraint is expressed by the simple state formula

Our intention is that, in view of the ramification con­ straint, the action of painting a block with a new colour should have the indirect effect of making the old colour disappear.

Example 2. The "murder mystery" from [Baker, 1991] can be formalized by the effect axioms

and the constraint

Example 3. Consider a table divided into three sec­ tors F, G and H. A block is always in exactly one of these three locations. There is an action A, which, if performed when the block is in location F, moves it out of that location. Hence, after the action is performed, the block is in location G or H, but we do not know which. Thus, this is a domain where the indirect effects are nondeterministic.

To represent this domain as a causal theory, we intro­ duce three fluents F, G and H. The only effect axiom lS

The constraints are

4 Turning a Causal Theory into an Abnormality Theory

In nested abnormality theories, as defined in [Lifschitz, 1995], parts of the axiom set can be grouped into "blocks" of the form

where C1 , ... , Cm are function and/or predicate symbols (said to be "described" by the block) and <1>1, ... , <I>n are formulas . Typically, some of these formulas contain the predicate constant Ab. Such a block corresponds to the circumscription of Ab in <1>1 1\ . . . 1\ <I>n with C1, . . . , Cm varied:

There can be several such blocks in the theory. More­ over, blocks can be "nested" in the sense that each <I>; can be itself a block. This possibility corresponds roughly to the use of priorities in traditional applications of circum­ scription. In this paper, we discuss abnormality theories with a particularly simple structure-the circumscrip­ tion operator is applied in them only once, so that no nesting of circumscriptions is possible. The reader fa­ miliar with the idea of circumscription will find it easy to understand these examples without a detailed review of the general formalism.

Let us assume that the signature and the axiom set of the given causal theory T are finite. We will denote the set of fluent symbols ofT by F, the set of its effect propo­ sitions by E and the set of its ramification constraints by C . The language of the abnormality theory Tab cor­ responding to T includes, in addition to the variables of the sorts available in T, variables for "aspects." Aspects will serve as arguments of the abnormality predicate A b. This device, proposed in [McCarthy, 1986], allows us to distinguish between different kinds of abnormality: an object abnormal in one "aspect" can be normal in an­ other. For every fluent symbol F ofT, we will need a new function symbol Asp F.

For every fluent symbol F, Tab will include the axiom

where FR ("F-Result") is a new predicate constant. These axioms can be viewed as explicit definitions of the constants FR. Using these constants, the effect axioms (1) can be rewritten as

The set of formulas obtained in this way from the effect axioms in E will be denoted by ER.

The "commonsense law of inertia" can be expressed in this notation by the formulas

--,Ab(AspF(x), a, s)I\Poss(a, s) :J (FR(x, a, s) = F(x, s)) for all F E F , which formalize the idea of minimal change. We will denote this set of formulas by I .

Each ramification constraint will have a counterpart, obtained from it by replacing each atomic part F(t, s) (where t is a tuple of terms) with FR(t, a, s) for a fixed action variable a. For instance, the counterpart of the ramification constraint (2) is

The set of formulas obtained in this way from the con­ straints in C will be denoted by CR .

We also introduce unique names axioms for actions and aspects. They are the formulas

A(x) # A'(y), A(x) = A(y) :J x = y, AspF(x) # AspF,(y), AspF(x) = AspF(Y) :J x = y

for arbitrary pairs of distinct action symbols A , A' and for arbitrary pairs of distinct fluent symbols F, F'. We denote this set of formulas by UNA.

The axioms of the abnormality theory Tab are:

UNA, c , FR(x, a, s) = F(x, Result( a, s)) (FE F), {FR : }. I, ER, CR

Here F R stands for the list of all predicates FR.

Note the use ofF R instead of Result in the range of cir­ cumscription. The intuition behind this style of describ­ ing actions can roughly be explained as follows. When we use circumscription to determine the effect of an ac­ tion a on a fluent in a situations, the only two situations that are of interest are the situation s and the situation obtained by performing the action a in s-for instance, we do not want to consider the sequence of actions that lead to situation s nor do we wish to consider what hap­ pens afterward. The new formalization achieves this by "removing" the Result function from the range of cir­ cumscription. In this part of the axiom set, we accept the local "theory update" view, as in Winslett's work.

According to the semantics of nested abnormality the­ ories [Lifschitz, 1995], the block at the end of the axiom set stands for the axiom formed as follows. Let <I> be the universal closure of the conjunction of all three groups of formulas included in the block. Denote the circum­ scription

CIRC[<I>; Ab; F)

by C(Ab). The axiom represented by the block is the formula 3abC( ab), where ab is a predicate variable that takes the same arguments as Ab. The last step­ replacing the predicate Ab by an existentially quantified variable- is motivated by the fact that, in an abnormal­ ity theory, Ab is an auxiliary constant whose value can be safely "forgotten."

For instance, the nested abnormality theory T~b cor­ responding to Example 1 has the following axioms:

(i) paint(x1, yt) = paint(x2, Y2) :J (x1 = x2/\Y1 = Y2), (ii) Aspcolour(xl,Yl) = Aspcolour(x2,Y2) :J (x1 = x2 1\ Yl = Y2), (iii) colour(x, Yl, s) 1\ colour(x, Y2, s) :J Yl = Y2, (iv) colourR(x, y, a, s)::: colour(x, y, Result( a, s)), { colourR : }. (v) --,Ab(Aspcolour(x,y),a,s)I\Poss(a,s) :J colourR(x, y, a, s) = colour(x, y, s), (vi) Poss(a, s) :J [a= paint(x, y) :J colourR(x, y, a, s)], (vii) colourR(x, Yl, a, s) 1\ colourR(x, Y2, a, s) :J Y1 = Y2

5 Computing Ramifications

In this section, we illustrate via examples how exist­ ing methods for computing circumscriptions can be em­ ployed in conjunction with the formalization presented above.

5.1 Completion

In many case, it is possible to compute the effects of actions using the syntactic methods for computing cir­ cumscriptions from [Lifschitz, 1993]. As an illustration, we will consider computing the circumscription from Ex­ ample 1 in some detail.

We will have occasion to use the following propositions from [Lifschitz, 1993].

Lemma 1. The circumscription CIRC[A(P, Z); P; Z] is equivalent to

Lemma 2. If A(x) does not contain p and B(p) is neg­ ative relative top then

is equivalent to B(.XxA(x)).

Lemma 3. If F(x) does not contain P, then the cir­ cumscription

is equivalent to 'v'x(F(x) = P(x)) .

Lemma 3 shows that circumscription can be some­ times evaluated by a process similar to the predicate completion algorithm from [Clark, 1978].

Let <I> be the conjunction of the universal closures of formulas ( v), (vi) and (vii) from the nested abnor­ mality theory T~b (Section 4) . By the definition of the semantics of nested abnormality theories, the block at the end of T~b stands for the formula 3ab C(ab) where C(Ab) stands for CIRC[<I>; Ab; colourR]· By Lemma 1, this circumscription is equivalent to the conjunction of <I> and CIRC[3colourR <I>;Ab]. 1 Using Lemma2, it is easy to eliminate the second-order quantifier in the formula 3colourR <I> . After a few simplification steps, we can use Lemma 3 to show that, in the presence of axioms (i)­ (iv), C(Ab) is equivalent to the conjunction of <I> and the following explicit definition for Ab:

Ab(z , a, s) = Poss(a, s) 1\ 3xy[z = Aspcolour(x, y)l\ ((-,colour(x, y, s) 1\ a= paint(x, y))V (colour(x, y, s) 1\3 y'(a = paint(x, y') 1\ y ::f y')))].

It follows that T~b is equivalent to the conjunction of formulas ( i)-( iv), (vi), (vii) and the result of substi­ tuting this expression for Ab in (v). The result of this substitution is essentially the conjunction of all "frame axioms" that are needed in conjunction with the causal theory of Example 1. We see that syntactic methods of computing circumscriptions can be employed to generate the necessary frame axioms.

The effect of the circumscriptions in Examples 2 and 3 can be computed in a similar way.

5.2 SCAN

SCAN [Gabbay and Ohlbach, 1992] is an algorithm for eliminating second-order quantifiers over predicate vari­ ables P1 , . .. , Pn in formulas of the form 3Pl . .. Pn <I>, where <I> is a first-order formula. If SCAN terminates, then the resulting formula is equivalent to the original formula.

Recall that CIRC[A; P; Z], the circumscription of the predicate P in formula A with the functions and/ or pred­ icates in the tuple Z varied, is the sentence

1 To simplify notation, we use colourR both as a predicate constant and predicate variable.

Here p is a predicate variable of the same arity as P, z stands for a tuple of variables which matches the tuple Z in arities and the sorts of arguments, and p < P stands for (p :S: P) 1\ -,(p = P) .

Hence to compute circumscriptions using SCAN, we input the formula 3pz[A(p, z) 1\ p < P] to it, negate the resulting formula and take its conjunction with the for­ mulaA(P, Z). Note that if z includes function constants, SCAN cannot be applied. For instance, since Baker's cir­ cumscriptive approach [Baker, 1991] involves varying the Result function, it cannot be used directly with SCAN.

An implementation of SCAN has been developed by Engel and Ohlbach 2 . Consider the application of this system to computing the circumscriptions from Sec­ tion 4.

In Example 1, the following set offormulas is taken as input to SCAN; the variables p and Rare eliminated.

(all x all y all xa all xs ( (-p(asp(x,y),xa,xs) & Poss(xa,xs)) -> (c(x,y,xs) <-> R(x,y,xa,xs)))). (all x all y all xa all xs ( (Poss(xa,xs) & (xa = paint(x,y))) -> R(x,y,xa,xs))). (all x all yi all y2 all xa all xs ( ((R(x,yi,xa,xs) & R(x,y2,xa,xs)) -> (yi = y2))). (all xf all xa all xs (p(xf,xa,xs) -> Ab(xf,xa,xs))). (exists xf exists xa exists xs ( -p(xf,xa,xs) & Ab(xf,xa,xs))). (all xi all yi all x2 all y2 ( (paint(xi,yi) = paint(x2,y2)) -> ((xi= x2) & (yi = y2)))). (all xi all yi all x2 all y2 ( (asp(xi,yi) = asp(x2,y2)) -> ((xi= x2) & (yi = y2)))). (all x all yi all y2 all xs ( (c(x,yi,xs) & c(x,y2,xs)) -> (yi = y2))). (all x (x = x)).

In the above formulas , R stands for colour R and c stands for colour. The first three formulas are direct encodings of ( v), (vi) and (vii). The next two formulas express that p < Ab. The next four are not a part of the circumscription formula; they are included to help SCAN simplify its output . Of these, the first three are formulas (i), (ii) and (iii) of the NAT.

SCAN produces the following 14 clauses as its output (in 1.6 seconds on a Sun 4) .

i paint(x,y)!=paint(z,u)lx=z. 2 paint(x,y)!=paint(z,u)ly=u. 3 asp(x,y)!=asp(z,u)lx=z. 4 asp(x,y)!=asp(z,u)ly=u . 5 -c(x,y,z)l -c(x,u,z)ly=u.

2 For more information on the implementation, see http: / /www.mpi-sb.mpg.de/guide/staff/ohlbach/scan/scan.html

6 Ab($c3,$c2,$c1). 7 x=x. 8 -Poss(paint(x,y),z)lc(x,y,z)l Ab(asp(x,y),paint(x,y),z). 9 -Poss(paint(x,y),$c1)1 -Poss($c2,$c1)1 c(x,y,$c1)1$c3!=asp(x,y)l$c2!=paint(x,y). 10 -Poss(paint(x,y),z)l -Poss(paint(x,u),z)l y=ulpaint(x,u)!=paint(x,y) . 11 -Poss(paint(x,y),z)l -c(x,u,z)l Ab(asp(x,u),paint(x,y),z)ly=u. 12 -Poss(paint(x,y),z)l -c(x,u,z)l Ab(asp(x,u),paint(x,y),z)lu=y. 13 -Poss($c2,$c1)1 -c(x,y,$c1)l$c3!=asp(x,y)l -Poss(paint(x,z),$c1)1z=ylpaint(x,z)!=$c2. 14 -Poss($c2,$c1)1 -c(x,y,$c1)1$c3!=asp(x,y)l -Poss(paint(x,z),$c1)ly=zlpaint(x,z)!=$c2.

In the set of clauses above, the expressions beginning with $ are Skolem constants introduced by SCAN in the process of converting the input into clauses, and the sym­ bol I stands for V.

By unskolemizing (that is, appending an existential quantifier to) this set of clauses, negating them, conjoin­ ing them with the axioms outside the block and simplify­ ing them, we can get an explicit definition of Ab identical to the formula obtained in Section 5.1, and consequently the frame axioms.

Some of this process of simplification of the set of clauses and elimination of Ab can be automated. For instance, to eliminate the redundant clauses, SCAN can be directed to try to derive each newly generated clause from the others for a fixed amount of time. In addi­ tion, SCAN can eliminate Ab from the simplified set of clauses.

The causal theory corresponding to Example 2 is

UNA, Walking(s) :::) Alive(s), Walkingn(a, s) = Walking(Result(a, s)), Aliven(a, s) = Alive(Result(a, s)), Loadedn(a, s) = Loaded(Result(a, s)), { WalkingR, Aliven, Loadedn : }. Pass( a, s) 1\ ·Ab(Aspectwalking, a, s) :::) Walkingn(a, s) = Walking(s), Poss(a, s) 1\ ·Ab(AspectAlive, a, s) :::) Aliven(a, s) = Alive(s), Poss(a, s) 1\ ·Ab(AspectLoaded, a, s) :::) Loadedn(a, s) = Loaded(s), Poss(Load, s) :::) Loadedn(Load, s), Pass (Shoot, s) 1\ Loaded ( s) :::) ·Alive R (Shoot, s), Pass (Shoot, s) :::) ·Loaded R (Shoot, s), Walkingn(a, s) :::) Aliven(a, s) .

When the corresponding formulas were input to SCAN, it produced 16 clauses in 1.8 seconds. Here again, we can further eliminate Ab and produce the frame ax­ ioms. For this example, SCAN helped in the automation of this process even better than in the previous case. For instance, consider the following clauses among the ones generated by SCAN:

x=LILo(y)l -Poss(x,y)l -Lor(x,y) . Lo(x)l -Poss(y,x)IAlr(y,x)l -Al(x).

In these clauses, L stands for Load, Lo for Loaded and Lor for Loadedn, Al for Alive and Alr for Aliven. Rewriting the first one as

Poss(a, s) 1\ a =f. Load 1\ ·Loaded(s) :::) ·Loaded (Result (a, s))

makes it clear that this a negative frame axiom for Loaded. Similarly, the second one can be rewritten as

Pass( a, s) 1\ ·Loaded( s) 1\ Alive( s) :::) Alive(Result( a, s)),

a positive frame axiom for Alive. Frame axioms of a similar and easy to comprehend form were generated for the other fluents also.

In Example 3, SCAN was used to generate the frame axioms in a similar way.

6 Discussion

In [Giunchiglia et al., 1995] , the method for represent­ ing actions from Section 4 is usef\l to define a translation from the high-level action language An to NATs. In some ways, An is more expressive than the language of causal theories from Section 2; for instance, it in­ cludes nonpropositional fluents. In other ways, it is less expressive-in An, actions .have no parameters, such as x andy in paint(x, y). The main difference between An and the language of causal theories, however, is that the former has a semantics, based on the notion of a transi­ tion function. The translation from [Giunchiglia et al., 1995] is complete relative to this semantics.

We have presented evidence that this approach to for­ malizing actions leads, in some cases, to the circumscrip­ tions that can be evaluated using the predicate comple­ tion method or the SCAN algorithm. One of these ex­ amples (Example 3) involves a "ternary state constraint" in the sense of Section 3.1 of [Pinto, 1994] and thus is not amenable to the methods developed there for the generation of successor state axioms in the case when all constraints are binary.

Our plans for the future include the development of an experimental program that uses SCAN for the com­ pletely automated generation of frame axioms. For this purpose, the simplification procedure used currently in SCAN will need to be enhanced.

The set of formulas produced by SCAN is equivalent to the formula input to SCAN, if the algorithm termi­ nates. Hence, even if we know that a given second-order formula is equivalent to some first-order formula, there is no guarantee that SCAN will ever find it . It would be interesting to isolate classes of action domains for which it can be proved that SCAN terminates when applied to the corresponding circumscriptive theory.

Acknowledgements

We would like to thank Enrico Giunchiglia, Fangzhen Lin, Norman McCain, Ray Reiter and Hudson Turner for useful discussions on the topic ofreasoning about ac­ tions. Special thanks to Thorsten Engel and Hans Juer­ gen Ohlbach for making the implementation of SCAN available to us. This research was supported in part by National Science Foundation under grant IRI-9306751.