A Logic of Intention

1 Introduction

Formalization of intention has drawn the attention of researchers [Cohen and Levesque 1990; Rao and Geor­ geff 1991; Konolige and Pollack 1993; Wainer 1994; Linder et a/., 1995; Huang et a/., 1996; Singh, 1997; Schild, 1999]. The common idea is to formalize intention into a modal operator on the framework of Kripkean possible world semantics. Many varieties of the seman­ tics have been put forward, and a lot of models of inten­ tion have been established. But all the formalizations suffer from the side-effect problem [Bratman, 1987]. The problem has two most difficult cases, the one concerning ~los~nes.s of intention consequences under tautological Imphcabons and the other concerning closeness under logical equivalencies. The former is about the relation between tautological implications and intention conse­ quences. It asks the question

• (Q) Given \j/, a tautological implication of <p, whether intending that \jl is a consequence of intending that <p?

The latter is a special case of the former where "equiva­ lence" is substituted for "implication" and "conse-

A Logic of Intention

Xiaoping Chen Guiquan Liu Dept. of Computer Science & Technology Univ. of Science & Technology of China He Fei, An Hui Province, 230027 P.R. China

quence".

To the question (Q), some of the previous theories an­ swer "yes", most of the others answer "no", and the re­ mainders give indefinite answers. We argue that both of th " " dth " " e yes an e no answers are wrong. Moreover, the first answer causes confusion between an agent's goal and its side-effects, and the second answer results in for­ saking the specification of intention consequences.

We provide an alternative approach to formalizing in­ tention. The basic idea is to develop a novel semantics which introduce "cognitive abstraction" into interpreta­ tion rules. It turns out that the semantics produces an appropriate specification of intention consequences to the extent that all and only the instances of side-effects, ex­ cept those in absorbent forms, are avoided. Besides that, the semantics supports a decision procedure for the in­ tention consequences defined in the semantics.

In the next section, we examine the side-effect problem and previous work on it. Section 3 states our motivation and basic ideas. The semantics is developed in section 4 and discussed in depth in section 5. Finally, in section 6, we draw some conclusions and point the way toward further development of our logic of intention.

2 The Side-effect problem

The language we use in this section is a modal extension of a propositional language with operators I and B, where I and B represent intention and belief, respectively. <p and \jl are arbitrary formulas, ::::) and = represent material im­ plication and equivalence, respectively. The so-called side-effect problem is captured by the following cases

(SEB) t=B(<p::::)\!f) ~ t=I(<p)::::)I(\!f)

(SET) t=<p::::)\j/ ~ t=I( <p ):)I( \!f)

(SEL) t=<p=\j/ ~ t=I(<p)=I(\j/)

(SEB) is the case of side-effect under belief implica­ tions. In this case, an agent's intentions are closed under his/her belief implications. (SET) is the case of side­ effect under tautological implications (logical consequences ), that is, an agent's intentions are closed under tautological implications. It can be regarded as a special case of the well-known problem of logical omniscience [Hintikka, 1962]. As pointed out in [Konolige and Pol­ lack, I993], this problem is more serious and harmful to intention than belief: logically consequential closure cannot be assumed for intention, even as an idealization; not all the consequences of an agent's intention are inten­ tions of the agent, even the consequences he/she has an­ ticipated. (SEL) is another case of the side-effect prob­ lem.

There are good solutions to (SEB), e.g. [Cohen and Levesque, I990; Rao and Georgeff, 199I; Wainer, I994], so we will not consider it in this paper. But, on the other hand, neither (SET) nor (SEL) has been solved satisfacto­ rily. A major difficulty in dealing with (SET) comes from the fact that either of the following rules has exceptions,

That is, tautological implications cannot be transferred to intention consequences in a globally uniform manner.

Previous work concerning (SET) can be classified into three categories. The models of intention in the first cate­ gory take (CI) and reject (C2) [Cohen and Levesque, I990; Wainer, I994). These models employ normal mo­ dal logics to characterize cognitive states including in­ tention. This makes them tolerate and hence suffer from (SET)(Strictly speeking, [Cohen and Levesque, I990] takes some more constraints on (C I), which avoids (SET) in some way. But Cohen and Levesque did not consider the way satisfactory). The models in the second category take (C2) with constraint FC\Jf:::Jq>. For example, the repre­ sentationalist theory of intention [Konolige and Pollack, I993] employs the minimal model semantics [Chellas, I980] to interpret the operator I. The only way to infer formulas containing I is by using the rule q>=\!fll(q>)=I(\Jf). Hence, if any intention is derivable from another in the theory, then their content must be logical equivalence. This means that both (SET) and the intention .conse­ quence are eliminated from the model. The models in the third category restrict both (Cl) and (C2) such that ne­ ither of them are valid for all q> and \Jf [Linder et a/., I995; Huang eta/., I996). Obviously, these models are more appropriate than the ones in the other two categories. But these models are not self-contained: one could not em­ ploy these models by themselves to decide whether F=I( q> ):::JI(\Jf) holds for any q> and \Jf· For instance, the model proposed in [Linder eta/., 1995] uses awareness [Fagin and Halpern, I988] to define preferences, and then goals (intentions). Because the explicit preferences cannot be characterized by a formalized system, the in­ tention consequences in the model are not specified. Moreover, no remedial measures to overcome this shortage have been put forward in literature.

As for (SEL), it is usually considered harmless [Linder eta/., 1995]. But from the point of view of bounded ra­ tionality and resource-boundness, (SEL) is inappropriate and harmful: logical equivalencies are not "cognitive equivalencies". For example, from

the side-effect \Jf is introduced. Perhaps one may think the situation could be remedied by demanding that agents always take the "simplest" content of an intention. This requires the specification of "simplest content", the crite­ rion of which has not been established definitely. It fol­ lows from the discussion above that all the models men­ tioned are inadequate. We believe the inadequacy results from the formal tools. We are to deal with these issues in depth.

3 Motivation

For simplicity, in this paper we only consider the formal specification of the intention consequence relation be­ tween the content of two intentions. Hence we assume in the rest of this paper that any formula in our formal lan­ guage ~ represents the content of an intention. For any q>,\JIE~, that \Jf is an intention consequence of q> means that I(\Jf) is an agent's intention whenever l(q>) is the agent's intention. Thus, ~ need not contain the modal operator I. A binary operator '~' is added into ~ and q>~\Jf means that \Jf is an intention consequence of q>.

In all existing theories, the semantic interpretation of an intention I( q>) is based on some set of the intended worlds, where each intended world is a classical possible world [Chellas 1980] satisfying q>, the content of the intention. However, classical possible worlds have fol­ lowing properties that are harmful to the appropriate specification of intention and intention consequences. Suppose q> is the formula representing the content of the intention being considered (and hence being satisfied by all the intended worlds).

(HI) All tautologies are satisfied by each classical possi­ ble world. Thus all tautologies are always intentions of any agent. This is a special case of (SET).

(H2) Any \Jf logically equivalent to q> is satisfied by each of the intended worlds. So \Jf is also an intention when­ ever q> is. This is (SEL).

(H3) Suppose formula \Jf is stronger than q>. Then \Jf may not be satisfied by an intended world, or even specified by a set of the intended worlds. This causes the failure to the specification of"strong consequences" (see below).

To overcome all the drawbacks, we introduce a new sort of possible worlds based on "cognitive abstraction". In our semantics, an intended world about q> is a "mini­ mal model" of q> in the sense that only a possibly smallest number of propositional symbols occurring in q> are as­ signed classical truth values while others are assigned the same abstract value (0 or 1). Any proposition assigned the abstract values are considered to be "abstracted cogni­ tively" (neglected cognitively). A world of this sort is a cognitively finite object, just matching the ability or nature of resource-bounded agents. Based on the set of minimal models, the intention consequence defined in the next section will draw or extract \jl from q> such that \jl is a piece of "partial content" of q>. As a result, the seman­ tics avoids all the harmful properties listed above and fits our purpose well. Most importantly, it supports a well­ defined and decidable inference scheme that can derive both "strong consequences" and "weak consequences" of an intention. If an agent intend that q>A\j/, then both q> and \jl are "partial content" (or "subgoals" as usually called) of the agent's intention. Generally, \jl is called a weak consequence of q>, if q> is stonger than \jl in the classical logic. Sometimes an agent need derive from his/her in­ tention q> some \jl as a "means" to the "end" q>, where \jl is stronger than q>. We call such \jl a strong consequence of q>. The compositions of strong and weak consequences are called hybrid consequences. For example, given in­ tention (x1vx2)AX3, its weak consequences are x1vx2 and x3, strong consequences are X1AX2 and X2AX3, and hybrid consequences are x1 and x2.

We will establish a logic of intention, Lmp4c, and em­ ploy the set of the Lmp4c's valid formulas of the form <p~\jl to provide a formal specification for the intention consequence. Therefore, for any q>,\j/Elt, the problem "if \jl is an intention consequence of q>" is reduced to the problem "if Rp~\j/ holds in Lmp4c"· The three kinds of intention consequence described above will be defined uniformly in Lmp4c· this makes it an uniform mechanism of inferring intention consequences. Moreover, we can also provide an algorithm to decide whether an intention consequence is a strong, weak, or hybrid one. If q> and \jl satisfy the single-level description assumption (SDA), i.e., all items of the primitive intention content (represented by proposition symbols in lt) occurring in \jl also occur in q>, then that Rp~\j/ holds in Lmp4c will guarantee that \jl will realize or elaborate rp without side-effect.

It follows from the discussion above that the validity characterized by our logic should conform to the follow­ ing principles

4 Formalization

Let Lt be the propositional language with a set of propo­ sitional symbols Atom={xt> x 2 , ··· } and logical connec­ tives...,, A, and v. The formulas of Lt are defined as usual. Let L, the language of Lmp4c· be an extension of Lt with only one additional operator ~. Any formula of L has the form q>~\j/ where q>,\j/Elt. The semantic interpreta­ tion of Lt is defined over the set T={t,f,O, I}, where t and f mean truth and falsehood, respectively, and 0 and I represent two states of"cognitive abstraction".

Definition 1 (Assignment) A 0-assignment is a mapping gO: Atom~{t,f,O}.

A 1-assignment is a mapping

gi: Atom~{t,f, I}.

An assignment is either a 0-assignment . or a !- assignment. 0

We will use Mo and M1 to denote the set of 0assignments and the set of !-assignments, respectively, and M to denote M0uM1·

The connectives ...,, A and v are interpreted by opera­ tors -, *, and + on T, respectively. These operators are defined in Figure I .

Definition 2 (Valuation) A valuation on ~ under 7tEM is a mapping V" assigning to each formula in ~ a value in T, such that for all xEAtom and cp,\j/E~

• (I) V ,(x) = 1t(x);
• v ,( -,cp) = -v ,( cp );
• V,(cp/\\jl) = V,(cp)·V,(\jl); and
• ( 4) V ,( cpv\jl) = V ,( cp )+V,(\jl). 0

V" is an extension of 1t and will be abbreviated 1t here­ after. For simplicity, we will use M0(MJ>M) to denote also the set of valuations that are extensions of assign­ ments in M0(M1,M).

Definition 3 (Model) For any 7tEM and cpE~, 1t is a model ofcp if and only if7t(cp)E{t,f}. 0

If 1t is a model of cp and 1t( cp )=t(f), then 1t is called a t­ model (f-model) of cp. Hereafter [cplt([cp]r) denotes the set oft-models (f-models) ofcp and [cp] denotes [cp] 1 u[cp]r.

The key idea to embody the cognitive characteristics of resource bounded agents is to introduce a "cognitive abstraction" relation on M.

Definition 4 (Cognitive abstraction) For any 7t,7t'EM,

1. 1t is a 0-abstraction of 1t', denoted by 1t~1t', iff
2. (i) 7t,7t'EM0; and
3. (ii) VxEAtom: 1t(x)=O or 1t(x)=1t'(x).
4. 1t is a 1-abstraction of 1t', denoted by 1t~ 1 1t', iff
5. (i) 7t,7t'EM1; and
6. (ii) VxEAtom: 1t (x)=l or 1t(x)=1t'(x).
7. 1t is a cognitive abstraction of 1t', denoted by 1t~1t', if and only if 1t~01t' or 1t~ 1 1t'. 0

Definition 5 (Minimal model) For any cpE~ and 7tE[cp], 1t is a minimal model of cp iff there exists no 1t' E [ cp] such that 7t*11:', 1t'~1t and 1t'( cp )=1t( cp ). 0

For any cpE~, [cp] denotes the set of minimal models ofcp.

Definition 6 (Validity) For any cp,\j/E~, 7tEM,

1. cp~\jl is true under 7t, denoted by 7rl=cp~\jl, if 7td\j/P37t'dcp]: 1t~1t' & 7t(\jl)=7t'(cp); otherwise, cp~\jl is false under 1t.
2. cp~\jl is valid in Lmp4c· denoted by ~cp~\jl, if 7rl=cp~\jl for all 7tEM. 0

Theorem 7 (Reflexivity and Transitivity) For any cp,x,\j/E~, (i) ~cp~cp; (ii) if ~cp~x and ~x~"'' then l=cp~\jl. 0

Theorem 8 (Decidability) The intention consequence in Lmp4c is decidable. That is, there exists an algorithm A such that for any cp,\j/E~, A returns "yes" if ~cp~\jl and "no" if Ftcp~\jl. 0

5 Features of Lmp4c

We show the side-effect-free property of Lmp4c by exam­ ining (SEL) and (SET) separately.

5.1 Free from (SEL)

We describe the relative results following the thread of their proofs, but omit these proofs here.

Any cp,\j/E~ are called intention equivalent in Lmp4c· denoted by ~cpB\jl, if ~cp~\jl and ~\jl~cp.

Theorem 9 Lmp4c has properties (P4)-(P10-2). 0

This indicates that all the methods for transferring for­ mulas into normal forms are preserved in Lmp4c· So we have

Corollary 10 For any cpE~, there exists a \j/E~ of normal form such that ~cpB\jl. 0

Any \jl is called a normal form of cp if \jl is in normal form and l=cpB\jl. For any cp,\j/E~, define [cp]=[\jl] as that [cp]=[\jl] and 7t(cp)=7t(\jl) for all 7tEM. And [cp] = [ \jl] is defined similarly.

Theorem 11 For any cp,\j/E~, following assertions are equivalent:

• (I) ~cpB\jl;
• [ cp ]=[ \jl ];

There are two sorts of equivalencies closely relative to (SEL ). A formula cp E ~ is called an absorbent form if cp has a sub-formula of the forms \jl/\(\j/VX) or \j/V(\j/1\X). \jl is called an absorbent normal form of cp if \jl is in absorb­ ent form and is a normal form of cp. \jl is called a strict normal form of cp if \jl is a normal form of cp and Atom(cp)=Atom(\jl), i.e., for all XEAtom, x occurs in \jl iff x occurs in cp.

Theorem 12 (Equivalence) For any cp,\j/E~, where \jl is in normal form, ~cpB\jl iff

• (I) \jl is a strict normal form of cp; or
• \jl is an absorbent normal form of cp. 0

Corollary 13 (Side-effect-free in equivalence under Atom) For any q>,\j/E~ not being of absorbent form, if RpB\jl then Atom(q>)=Atom(\jl). 0

This result can be strengthened further even in situa­ tions where Atom(q>)=Atom(\jl).

Theorem 14 (Side-effect-free in equivalence)

(I) i;z:q>Bq>A( ·\j/V\jl);

The instances of this invalidity can be found next sub­ section, e.g., (Pl-6), (Pl-7) and (P2-6), etc.

Now the feature of intention equivalencies in Lmp4c can be summarized in two aspects. First, intention equivalen­ cies cover all strict and absorbent normal forms. Second, all of the other forms of equivalencies in the standard logic are forbidden. This means that all instances of (SEL), except absorbent equivalencies, are avoided in Lmp4c·

5.2 Free from (SET)

Theorem 15 (Side-effect-free in consequence under Atom) For any q>,\j/E~, if F=q>~\jl and \jl is not in absorbent forms, then Atom(\jlk;;Atom(q>). 0

At the first glance, the property is shared with Bo­ chvar's 3-valued logic, where \jl is a semantic conse­ quence of q> iff it is in the classical logic and Atom(\jlk;;Atom(q>)[Mo, 1954]. However, there are re­ markable differences between Bochvar's and ours, which will become clear in the following discussion.

Theorem 16 Lmp4c has the properties (Pl-l)-(P3). 0

This theorem, together with theorem 9, shows that Lmp4c follows all the principles previously put forward.

It seems from properties (PI-I) and (Pl-3) that Lmp4c is similar to the standard logic in deriving weak conse­ quences: a conjunct of a conjunctive intention is also an intention, or a "sub-intention". (Pl-4) and (Pl-2) reveal that it is not the case. In particular, the inference in Lmp4c is not "driven" only by the surface layer of the syntactic description of formulas, while at least in some extent the standard logic is. Moreover, (Pl-4) also gives an instance that Lmp4c forbids the unnecessary weakening of inten­ tions.

Properties (P2-l) and (P3) indicate other significant dif­ ferences between the intention consequence in Lmp4c and the _logical consequence in the standard logic: Lmp4c can denve strong consequences of a given intention, i.e., sufficient means for the end without side-effects. The difference is made clearer by (P2-3) and (P2-4), where the latter also shows that unnecessary strengthening is not allowed in Lmp4c· Further properties about strong con­ sequences are given as follows.

Properties (P2-5), (P2-6) and (P2-7) are three more in­ stances of prohibiting intention consequences from de­ riving side-effects. These side-effects contain logical contradictions, but they may not contain new atoms. However, a "contingent" intention can be extracted from its compound with a logical contradiction, as (P2-8) shows. It is also forbidden in Lmp4c to infer intention con­ sequences from contradictory intentions, an instance of this property is (Pl-2).

Another kind of side-effects concerns tautological in­ tentions. Fortunately, this kind of side-effects is also refused by Lmp4c-

Theorem 18

(Pl-6) &z:=x 1~X1A(-,X2VX2)

(Pl-7) F=x1A(-,x2vx2)~x1

(P 1-8) &z:=x 1 A( -,X 2 VX2)~( -,X2 VX2)

(Pl-9) P:: (-,x1vx1)vx2~x2

(Pl-10) P:: (-,x1vx1)~x1

From above discussion we can draw the conclusion that Lmp4c avoids all side-effects usually appearing in intention consequences, except ones in absorbent form.

6 Conclusion

Lmp4c is rather simple and powerful. It does provide a formal specification and a decidable inference mecha­ nism of intention consequences. Most strikingly, all and only the instances of side-effects we have identified, except those in absorbent forms, are forbidden in Lmp4c· Meanwhile, all the rules for transferring formulas into normal forms in classical logics are preserved in Lmp4c· This indicates that the logic has a moderate de­ scriptive granularity, lying between that of the standard semantics and that of the syntactic approach [Eberle, 1974; Konolige, 1986]. Perhaps the traditional idea of interpreting intention as an unary modal operator in Kripke's semantics is misleading, although this idea has many advantages. In addition, Lmp4c is not just a subsys­ tem of the classical proposition logic - both weak and strong consequences can be derived in it with a unified mechanism. So it could be used as a new tool of reason­ ing about plans.

We have concentrated on intention consequences in this paper. Some further development is also under con­ sideration. First, Lmp4c need to be extended to languages including action terms and be able to function beyond the SDA (see section 3). Second, we have discovered that Lmp4c provides an interesting definition and mechanism of some kind of non-monotonic reasoning. Third, it is de­ served to consider whether the semantics of Lmp4c can be generalized and employed to treat other kinds of cogni­ tive state such as belief, and to model the interaction among these cognitive operators. Last, the tractability of the decision procedure for Lmp4c is an open problem.

Acknowledgements

This work is supported by the National Natural Science Foundation of China ( 6987 50 17). The first author thanks Yulin Feng, Yutian Wang and Shifu Chen for their helps.