Soundness and Completeness Theorems for Three Formalizations of Action

1 Introduction

Most of the past work in reasoning about action has been done using nonmonotonic logics. Several nonmono­ tonic formalisms have appeared in the literature [Mc­ Carthy, 1980; Reiter , 1980; McDermott and Doyle, 1980; Moore, 1985] and a number of technical results about these have been obtained. Moreover, there has been a flurry of formalisms which are variations of the above which were designed to handle instances in which the original formalisms yield counterintuitive results 1 · How­ ever, the focus of most of this work has been on for­ malizing specific problems. This makes it very difficult to compare the different approaches as to the range of applicability of each.

There also have been attempts recently to reason about action in first order logic [Pednault , 1989; Schu­ bert , 1990; Reiter , 1991]. Again, most of the work has been in terms of specific examples.

In this paper, we focus on a general class of problems, which are expressible in a simple declarative language A introduced in [Gelfond and Lifschitz, 1992]. In that p~per, the authors also define a translation from A into the language of extended logic programs and prove its soundness. Our work is similar in that we provide sim­ ple translations from A into three different methodolo­ gies which have been proposed in the literature, but we prove both the soundness and completeness of the three translations relative to the semantics of A . Our mo­ tivation is to precisely characterize the strengths and limitations of various formalizations of action and in that, our work is is related .to that in [Lifschitz, 1991 ; Lin and Shoham, 1991].

·This work was partially supported by National Science Foundation under grant IRI-9101078.

1 The most notorious among such instances is the Yale shooting problem [Hanks and McDermott, 1987], for which a large number of solutions have been proposed.

The first two translations we provide use the first order methods for reasoning about action, suggested by Ped­ nault [Pednault, 1989] and Reiter [Reiter, 1991]. The third one is the nonmonotonic formalism of circumscrip­ tion. The soundness and completeness of the three trans­ lations is interesting since it lets us compare these three methodologies in a mathematically precise fashion : we get the result that they are equivalent in the sense that they all faithfully capture the semantics of A. Many problems which have been discussed extensively in the literature, such as the Yale shooting problem, are spe­ cial cases of the formalization presented here. Thus, our work yields three classes of successful formalizations of wide applicability. Unlike other approaches like that in [Shoham, 1988], in addition to reasoning forward in time, the formalizations support reasoning backwards in time as well. They also let us deal with incompletely specified initial situations.

The technically most difficult part of this paper is the formalization based on circumscription. It is based on the following idea of Baker [Baker, 1991]: When the abnormality predicate Ab is circumscribed, the Result function and the situation constant corresponding to the initial situation, So are allowed to vary. A theorem is proved which shows that the circumscription yields re­ sults which are intuitively expected. This result shows how to apply the methods in [Baker, 1991] in a general setting. The theorem is proved in a fashion which makes it plausible that the methods of proof can be employed in other situations as well .

In the next section, we describe the language A which is used to formalize the domain of actions. Section 3 de­ scribes Pednault's approach and a translation of actions described in A which uses his scheme. Section 4 presents a translation based on Reiter's approach. In Section 5, we provide a translation which uses the circumscriptive approach. Section 6 contains concluding remarks. The proofs of all the theorems are omitted.

2 The Language A

In this section, we describe the languge A introduced in [Gelfand and Lifschitz, 1992]. The reader who is in­ terested in more examples and motivation is referred to that paper.

Consider two disjoint nonempty sets of symbols, called fluent names and action names. A fluent expression is a fluent name possibly preceded by ....,, A v-proposition specifies the value of a fluent after performing zero or more actions from the initial situation. It is of the form

where F is a fluent expression, and A1, .. . ,Am (m ~ 0) are action names. If m = 0, we will write (1) as

initially F.

An e-proposition describes the effect of an action on a fluent and is of the form

where A is an action name, and each ofF, P1, ... , Pn (n ~ 0) is a fluent expression. Let us denote by IFI the fluent name occurring in the fluent expression F. If IFI occurs unnegated (negated) in (2), we call it a positive (negative) e-proposition and say that A affects IFI pos­ itively (negatively). We also say that this e-proposition describes the effect of A on F, and that P1 , ... , Pn are its preconditions. If n = 0, we will drop if and write simply

A causes F.

A proposition is a v-proposition or an e-proposition. A domain description, or simply domain, is a set of propo­ sitions (not necessarily finite).

Example 1. The Blocks World domain DB, motivated by problem D4 from [Lifschitz, 1989], is defined as fol­ lows. The fluent names are Ontable and Jnhand; the action names are Putdown, Pickup, Lower and Wait. The propositions of DB are:

initially -,Qntable, Ontable after Wait,-Putdown, Put down causes On table if Inhand, Put down causes -,Jnhand if Inhand, Pickup causes Inhand if Ontable, Pickup causes -,Qntable if Ontable, Lower causes Ontable if Inhand.

The following definitions will be useful in describing the semantics of A.

A state is a set of fluent names. Given a fluent name F and a state u, we say that F holds in u ifF E u; -,F holds in u ifF fl. u. A transition function is a mapping <I> of the set of pairs (A, u), where A is an action name and u is a state, into the set of states. A structure is a pair (u0 , <I>), where u0 is a state (the initial state of the structure), and <I> is a transition function .

For any structure M and any action names A1, ... , Am, by MA,; ... ;Am we denote the state

where <I> and u0 are the transition function and the initial state of M. We say that a v-proposition (1) is true in a structure M if F holds in the state M A 1 ; ... ;Am I and that it is false otherwise.

A structure (uo, <I>) is a model of a domain description D if every v-proposition from D is true in (u0 , <I>) and for every action name A, every fluent name F, and every state u, the following two conditions are satisfied:

• (i) if D includes an e-proposition describing the effect of A on F (-,F) whose preconditions hold in u, then F (...,F) holds in the state <I>(A, u).
• (ii) otherwise, F holds in the state <I>( A, u) iff F holds in the state u.

Note that there can be at most one transition func­ tion <I>, satisfying conditions (i) and (ii). Hence different models of the same domain differ only by their initial states.

A v-proposition is entailed by a domain description D if it is true in every model of D.

A domain description is consistent if it has a model.

Example 1 (continued). The domain description DB is consistent . Its only model is defined by the equations

It is easy to see, for instance, that

initially Inhand, Ontable after Lower; Wait, -,Jnhand after Lower; Wait; Put down,

is entailed by DB.

3 Translation into Pednault's Scheme

3.1 Review of Pednault's Proposal

In this section, we review Pednault's proposal for gener­ ating the frame axioms. We will conform for the most part to the notation introduced in [Reiter, 1991].

Pednault assumes that corresponding to each fixed flu­ ent F and each fixed action A there are two effect axioms, a positive effect axiom of the form 2 :

and a negative effect axiom of the form

Here, 11"A(s) denotes the action preconditions of the action A. These are the prerequisites that must be sat­ isfied for the execution of action A. They depend only on A. €t(s) (€j;(8)) denotes the positive (negative) flu­ ent preconditions under which action A, if performed, will lead to F becoming true (false) in the resulting sit­ uation Result(A,s). We assume that in (3) and (4), 8 is universally quantified.

Pednault observes that he can obtain the frame axioms from the effect axioms systematically if a completeness assumption for the fluent preconditions is made. The assumption is that the positive (negative) fluent precon­ ditions specify all the conditions under which an action if performed will lead to the truth (falsity) of the fluent in the resulting situation. Using this assumption, we can say that if in situation 8, we have 11"A(8), then the only way that F can change from false in situation 8 to true in situation Re8ult(A, s) is if 4(s) were true. This can be formalized as

Rewriting the above as

we see that this is a frame axiom. Similarly, we can generate the frame axiom

11"A(s) 1\ H olds(F, s) 1\ ...,€j;(s) :J H olds(F, Result(A, s)) from (4) .

3.2 The Translation P(D)

Let D be a finite domain. The following notation will be used: If A1, ... , Am are action names, [A1; ... ; Am] stands for the ground term

If t is a term,

The translation of a v-proposition a of the form (1), denoted P(a), is

Since corresponding to an F, A pair (where F is a flu­ ent name and A is an action), Pednault has just two effect axioms, e-propositions are not translated individ­ ually. Rather the set of all e-propositions describing the effect of A on F or -,F, SF,A, is partitioned into two subsets sj.,A and SF,A· sj.,A (Sj;,A) consists of all the e-propositions describing the effect of A on F (-.F). The e-propositions in each of these two sets are then trans­ lated as a group. To express this formally, define for any e-proposition E of the form (2),

2 The form of the effect axioms in our review is more spe­ cial than the ones actually used by Pednault: we deal with individual actions and fluents rather than families parameter­ ized by x and y. We use such a simplification in our review of Reiter's proposal also.

Also define,

Now, we can translate the collection of e-propositions in SF,A as

Using the notation of the previous section we see that 11"A(s) can be identified with true, 4(s) can be identi­ fied with precondt,A (s) and €j;(s) can be identified with precondj; A (s).

Let F v' and Av be, respectively, the set of all the flu­ ent names and action names mentioned in the domain ?escription D. Then we will also add the following ax­ IOms:

1. The domain closure axiom (DCA) for fluents:

1. The domain closure axiom (DCA) for actions:

1. The unique name assumption (UNA) axiom for flu­ ents:

1. The unique name assumption (UNA) axiom for ac­ tions:

By P(D), we denote the collection of axioms which con­ sist of these four axioms, the axioms of the form (5), (6) and (7) and the frame axioms obtained from the effect axioms by the process outlined in the previous section. That is, we add for each fluent-action pair F, A, the two frame axioms

• -.H olds(F, s)/\...,precondt,A (s) :::> ...,H o/ds(F, Result(A, s)),

Example 1 (continued). P(DB) consists of the follow­ ing axioms 1-11 and sixteen frame axioms (including two trivial ones) of the form (8) and (9).

1. ...,Holds( On table, So).
2. Holds( Ontable, Result(Putdown, Result( Wait, So)))
3. Holds(Inhand,s):::> Holds( Ontable, Result(Putdown, s)) .
4. H olds(Inhand, s) :::> ...,Holds(Inhand, Result(Putdown, s)).
5. Holds( Ontable, s) :::> Holds(Inhand, Result(Pickup, s)).
6. Holds( Ontable, s) :::> -,Holds( Ontable, Result( Pickup, s)).
7. H olds(Inhand, s) :::> Holds( Ontable, Result( Lower, s)).
8. f = Ontable V f = Inhand.
9. a= Putdown V a= Pickup V a= Lower V a= Wait.
10. Ontable ¥ Inhand.
11. Put down ¥ Pickup 1\ Put down ¥ Lower 1\ Put down ¥ Wait 1\ Pickup ¥ Lower 1\ Pickup ¥ Wait 1\ Lower ¥ Wait.

3.3 Soundness and Completeness

We can relate the notion of entailment in the sense of first order logic and entailment relation for the language A using the following theorem.

Theorem 1 Let D be any finite, consistent domain, and let P(D) be defined as before. For any v-proposition a,

Theorem 1 can be thought of as expressing the soundess and completeness of the translation P. Note that it gives a very strong characterization of what can be proved from P(D). For instance, using this theorem, we can conclude in the case of Example 1 that P(D) F= H olds(Inhand, S0 ). Note that this corresponds to rea­ soning about the past. Similarly, we can conclude that P(D) F= ...,H olds(Inhand, [Lower; Wait; Putdown]). This corresponds to reasoning about the future, when the initial situation is incompletely specified. Domains in which each v-proposition has the form initially F, are just a simple special case of this theorem. Such domains correspond to temporal projection problems, which have been the focus of much attention in the literature.

In the subsequent sections, we shall propose similar translations from D into other domains. In each case, we will prove theorems of exactly the same form as The­ orem 1, the only change being that instead of the trans­ lation P, we will have other translation schemes. Thus all the remarks of the previous paragraph apply to these translation schemes as well.

4 Translation into Reiter's Scheme

4.1 Review of Reiter's Proposal

Like Pednault, Reiter also has two effect axioms for each fluent F. But in these effect axioms, the actions are uni­ versally quantified (following the proposal by Schubert [Schubert, 1990]) . So he calls them general effect axioms. They are of the form

The predicate Poss(a, s) intuitively means that a is pos­ sible in situation s. Pass is defined by action precondi­ tion axioms of the form

for each action A, where 1rA(s) stands for the action A's preconditions.

Reiter also makes a completeness assumption, accord­ ing to which (10) and (11) account for all the conditions under which action a can affect the value of F . As be­ fore, this completeness assumption leads to what Reiter calls explanation closure axioms. They are equivalent to frame axioms of the following form:

Comparing these frame axioms with the ones obtained by Pednault, we see that the reification of actions allows Reiter to express the frame axioms in a more compact way.

4.2 The Translation R(D)

The translation of the domain D into Reiter's scheme, R(D), is very similar to the translation P(D) into Ped­ nault's scheme: the translation of v-propositions is ex­ actly the same and the UNA and DCA for fluents and ac­ tions are included in the translation, as before. The only differences are in the translation of the e-propositions and in the form of the added frame axioms. These dif­ ferences arise due to the fact that here, actions in the general effect statements are universally quantified.

With a fixed fluent name F, we associate two sets: the set At of action names which affect it positively and the set Af. of those which affect it negatively. Note that it is possible for a particular action name to be in both these sets or to be in neither of them.

Now we can give the translation of e-propositions into Reiter's formalism as follows:

In comparison to the notation used in Section 4.1, Pass( a, s) corresponds to true, lfr(a, s) to

R(D) consists of the translation of all the v­ propositions and e-propositions, that is, all sentences of the form (5), (12) and (13), the UNA and DCA for flu­ ents and actions, and the frame axioms generated by the process outlined in the previous section.

We can now prove a theorem about R(D) exactly sim­ ilar to Theorem 1.

Theorem 2 Let D be any finite, consistent domain and let R(D) be defined as before. For any v-proposition a,

In [Elkan, 1992], Elkan proposed a similar scheme for reasoning about action. We can easily prove a theorem of the same form as Theorem 2 for this scheme also.

5 Translation into Circumscriptive Scheme

In this section we will propose a translation into a cir­ cumscriptive scheme, based on the method of [Baker, 1991] and state again the soundness and completeness of the translation. This result is of independent interest, since it shows that circumscription can handle reasoning about actions elegantly.

5.1 Review of Circumscription

Circumscription was introduced by McCarthy [Mc­ Carthy, 1980; McCarthy, 1986] as a formalism for non­ monotonic reasoning. Intuitively, circumscribing a pred­ icate in a sentence means assuming that the extent of the predicate is as small as possible. We formally define this as follows :

For any predicate symbols P, Q of the same arity, let P = Q stand for Vx(P(x) = Q(x)) and P ~ Q stand for Vx(P(x) :J Q(x)). Let Z stand for the tu­ ple Z 1 ,Z2 , ... Zm of object, function, and/or predicate constants. Let A(P, Z) be a sentence containing Z and a predicate constant P.

The circumscription of P in A with Z varied, denoted by CIRC(A;P;Z) is the sentence

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

In reasoning about action using circumscription, we first introduce an axiom for the "commonsense law of inertia"

This says that the values offluents normally persist, after an action is performed. The predicate Ab(f, a, s) intu­ itively means the following: f is abnormal with respect to a in situation s.

Traditionally [McCarthy, 1986], the formula B' con­ sisting of the conjunction of the universal closures of all the domain axioms is circumscribed with respect to Ab while varying the predicate Holds. But this does not work, as noted by Hanks and McDermott in [Hanks and McDermott, 1987]. A simple solution, proposed by Baker in [Baker, 1991] is to vary the function Result instead. For this method to work correctly, we need an "existence of situation" axiom, which intuitively says that, corresponding to any subset of fluents, there is a situation in which exactly these hold. This can be formu­ lated as follows: Let q range over states, that is, subsets of the set of all fluents. Define

Now, the existence of situations axiom can be written as

Baker [Baker, 1991] suggests ways to write this axiom in a more compact form.

5.2 The Translation B(D)

Let us first define an auxiliary translation TB(D) as a preliminary step before defining B(D). TB(D) is similar to P(D) in that the translations of the v-propositions are exactly the same as in P(D), and in that TB(D) includes the UN A and DCA for actions and the DCA for fiuents. Each e-proposition is translated individually in TB(D). That is, the translation of an e-proposition E of the form (2), which describes the effect of A on F is simply

In addition to the above, TB(D) contains axioms (14) and (15). (Note that we do not need to add the UNA for fluents, since it follows from (15).)

Let B' be the conjunction of the universal closures of the axioms of TB(D). Let us denote the formula CI RC(B'; Ab; Result, So) by B(D). The following the­ orem about B( D) can now be proved:

Theorem 3 Let D be any finite, consistent domain and let B(D) be defined as before. For any v-proposition a ,

Note that this theorem is of the same form as Theo­ rems 1 and 2. Using this theorem, we can prove a "re­ stricted monotonicity" result [Lifschitz, 1993] for Baker's approach to formalizing action.

The proof of Theorem 3 is based on the following lemma about the result of circumscribing Ab.

The Main Lemma Let D be a finite, consistent do­ mam. Then B(D) is equivalent to the conjunction of B' and

Note that this lemma characterizes Ab completely.

6 Summary and Discussion

In this paper, we have shown that the methods in [Perl­ nault, 1989; Reiter, 1991; Baker, 1991] are applicable to a large class of problems. These methods support rea­ soning forward as well as backward in time. We have also compared these methods in a mathematically pre­ cise fashion. Moreover, we have shown how to apply the methods in [Baker, 1991] to reason about actions using circumscription, in a general setting. The results of this paper, in combination with the soundness the­ orem for the translation into logic programming from [Gelfond and Lifschitz, 1992], suggest that the computa­ tional mechanism of logic programming can be used for implementing the theories of action proposed by Perl­ nault, Reiter and Baker.

One major assumption we make is that the problem domain under consideration can be formalized in A. As is pointed out in [Gelfond and Lifschitz, 1992], A is rather limited in its expressive power. For instance, we assume here that the fluents are all independent. This means that we are spared the task of coping with the "ramification problem" . Another issue we do not ad­ dress here is the qualification problem.

It seems, however, that the methods outlined in this paper will prove capable of being extended to more com­ plex domains. This is the topic of our ongoing research.

Acknowledgements

I wish to thank Vladimir Lifschitz for discussing this work with me and for his help with the contents and presentation of this paper. I also wish to thank Michael Gelfond, Norm McCain, Jeff Rickel and Thomas Woo for comments on an earlier ·draft.