# Elaborating domain descriptions (ECAI 2006)

Andreas Herzig, Laurent Perrussel, Ivan Varzinczak

► To cite this version:

Andreas Herzig, Laurent Perrussel, Ivan Varzinczak. Elaborating domain descriptions (ECAI 2006). 17th European Conference on Artificial Intelligence (ECAI 2006), Aug 2006, Riva del Garda, Italy. pp.397-401. hal-03537160

HAL Id: hal-03537160

https://hal.science/hal-03537160

Submitted on 4 Feb 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Elaborating domain descriptions

Andreas Herzig and Laurent Perrussel and Ivan Varzinczak<fnref n="1" />

**Abstract.** In this work we address the problem of elaborating domain descriptions (alias action theories), in particular those that are expressed in dynamic logic. We define a general method based on contraction of formulas in a version of propositional dynamic logic with a solution to the frame problem. We present the semantics of our theory change and define syntactical operators for contracting a domain description. We establish soundness and completeness of the operators w.r.t. the semantics for descriptions that satisfy a principle of modularity that we have defined in previous work.

## 1 INTRODUCTION

Suppose a situation where an agent has always believed that if the light switch is up, then the room is light. Suppose now that someday, she observes that even if the switch is up, the light is off. In such a case, the agent must change her beliefs about the relation between the propositions "the switch is up" and "the light is on". This is an example of changing propositional belief bases and is largely addressed in the literature about belief change [10] and update [24].

Next, let our agent believe that whenever the switch is down, after toggling it, the room is light. This means that if the light is off, in every state of the world that follows the execution of toggling the switch, the room is lit up. Then, during a blackout, the agent toggles the switch and surprisingly the room is still dark.

Imagine now that the agent never worried about the relation between toggling the switch and the material it is made of, in the sense that she ever believed that just toggling the switch does not break it. Nevertheless, in a stressful day, she toggles the switch and then observes that she had broken it.

Completing the wayside cross our agent experiments in discovering the world's behavior, suppose she believed that it is always possible to toggle the switch, given some conditions e.g. being close enough to it, having a free hand, the switch is not broken, etc. However, in an April fool's day, she discovers that someone has glued the switch and, consequently, it is no longer possible to toggle it.

The last three examples illustrate situations where changing the beliefs about the behavior of the action of toggling the switch is mandatory. In the first one, toggling the switch, once believed to be deterministic, has now to be seen as nondeterministic, or alternatively to have a different outcome in a specific context (e.g. if the power station is overloaded). In the second example, toggling the switch is known to have side-effects (ramifications) one was not aware of. In the last example, the executability of the action under concern is questioned in the light of new information showing a context that was not known to preclude its execution. Carrying out such modifications is what we here call elaborating a domain description, which has to do with the principle of elaboration tolerance [28].

Such cases of theory change are very important when one deals with logical descriptions of dynamic domains: it may always happen that one discovers that an action actually has a behavior that is different from that one has always believed it had.

Up to now, theory change has been studied mainly for knowledge bases in classical logics, both in terms of revision and update. Only in a few recent works it has been considered in the realm of modal logics, viz. in epistemic logic [12] and in action languages [7]. Recently, several works [31, 21] have investigated revision of beliefs about facts of the world. In our examples, this would concern e.g. the current status of the switch: the agent believes it is up, but is wrong about this and might subsequently be forced to revise her beliefs about the current state of affairs. Such revision operations do not modify the agent's beliefs about the action laws. In opposition to that, here we are interested exactly in such modifications. The aim of this paper is to make a step toward that issue and propose a framework that deals with the contraction of action theories.

Propositional dynamic logic (PDL [13]), has been extensively used in reasoning about actions in the last years [2, 36, 8]. It has shown to be a viable alternative to situation calculus approaches because of its simplicity and existence of proof procedures for it. In this work we investigate the elaboration of domain descriptions encoded in a simplified version of such a logical formalism, viz. the multimodal logic $K_n$. We show how a theory expressed in terms of static laws, effect laws and executability laws is elaborated: usually, a law has to be changed due to its generality, i.e., the law is too strong and has to be weakened. It follows that elaborating an action theory means contracting it by static, effect or executability laws, before expanding the theory with more specific laws.

## 2 BACKGROUND

Following the tradition in the reasoning about actions community, action theories are collections of statements of the form: "if *context*, then *effect* after *every execution of action*" (effect laws); and "if *pre-condition*, then *action executable*" (executability laws). Statements mentioning no action at all represent laws about the world (static laws). Besides that, statements of the form "if *context*, then *effect after some execution of action*" will be used as a causal notion to solve the frame and the ramification problems.

### 2.1 Logical preliminaries

Let $Act = \{a_1, a_2, ...\}$ be the set of all *atomic actions* of a given domain, an example of which is *transition*. To each atomic action *a* there is associated a modal operator [*a*]. $Prop = \{p_1, p_2, ...\}$ denotes all the *propositional constants* (alias * fluents* or *atoms*). Examples of those are *light* ("the light is on") and *up* ("the switch is up"). The set of all literals is $Lit = Prop \cup \{-p : p \in Prop\}$.

<footnote n="1">¹ The authors are with the Institut de Recherche en Informatique de Toulouse (IRIT), Toulouse, France. e-mail: {herzig, perrusse, ivan}@irit.fr</footnote>
Formal is the set of all classical formulas. They are denoted by small Greek letters $\varphi, \psi, \dots$. An example is $\mathit{up} \to \mathit{light}$. By $\mathit{val}(\varphi)$ we denote the set of valuations making $\varphi$ true. We view a valuation as a maximally-consistent set of literals. For $\mathfrak{Prop} = \{\mathit{light}, \mathit{up}\}$, there are four valuations: $\{\mathit{light}, \mathit{up}\}$, $\{\mathit{light}, \neg \mathit{up}\}$, $\{\neg \mathit{light}, \mathit{up}\}$ and $\{\neg \mathit{light}, \neg \mathit{up}\}$. Given a set of formulas $\Sigma$, by $\mathit{lit}(\Sigma)$ we denote the set of all literals appearing in formulas of $\Sigma$.

We denote complex formulas (with modal operators) by $\Phi, \Psi, \dots$ ($\langle a \rangle \Phi$ is the dual operator of $[a]$, defined as $\langle a \rangle \Phi =_{\mathrm{def}} \neg[a] \neg \Phi$. An example of a complex formula is $\neg \mathit{up} \to [\mathit{ toggle}] \mathit{up}$. The semantics is that of multimodal logic K [29].

A K<sub>n</sub>-model is a tuple $\mathcal{M} = \langle W, R \rangle$ where W is a set of valuations, and R a function mapping action constants a to accessibility relations $R_a \subseteq W \times W$. Given a K<sub>n</sub>-model $\mathcal{M} = \langle W, R \rangle$, $\mathbb{F}_w^\mathcal{M} p$ ($p$ is true at world $w$ of model $\mathcal{M}$) if $p \in w$; $\mathbb{F}_w^\mathcal{M} [a] \Phi$ if for every $w'$ such that $wR_a w'$, $\mathbb{F}_w^\mathcal{M} \Phi$. Truth conditions for other connectives are as usual.

$\mathcal{M}$ is a model of $\Phi$ (noted $\mathbb{F}_w^{\mathcal{M}} \Phi$) if for all $w \in W$, $\mathbb{F}_w^{\mathcal{M}} \Phi$. $\mathcal{M}$ is a model of a set of formulas $\Sigma$ (noted $\mathbb{F}_w^{\mathcal{M}} \Sigma$) if $\mathbb{F}_w^{\mathcal{M}} \Phi$ for every $\Phi \in \Sigma$. $\Phi$ is a consequence of the set of global axioms $\Gamma$ in the class of all K<sub>n</sub>-models (noted $\Gamma \models_{\mathcal{K}_n} \Phi$) if for every K<sub>n</sub>-model $\mathcal{M}$, $\mathbb{F}_w^{\mathcal{M}} \Gamma$ implies $\mathbb{F}_w^{\mathcal{M}} \Phi$.

## 2.2 Describing the behavior of actions in K<sub>n</sub>

$K_n$ allows for the representation of statements describing the behavior of actions. They are called action laws. Here we distinguish several types of them. The first kind of statement represents the static laws, formulas that must hold in every possible state of the world.

**Definition 1** A static law is a formula $\varphi \in \mathfrak{F} \mathit{ml}$.

An example of a static law is $\mathit{up} \to \mathit{light}$: if the switch is up, then the light is on. $\mathcal{S} \subseteq \mathfrak{F} \mathit{ml}$ denotes all the static laws of a domain.

The second kind of law we consider are the effect laws. They are formulas relating an action to its effects, which can be conditional.

**Definition 2** An effect law for action $a$ has the form $\varphi \to [a]\psi$, where $\varphi, \psi \in \mathfrak{F} \mathit{ml}$.

The consequent $\psi$ is the effect always obtained when $a$ is executed in a state where the antecedent $\varphi$ holds. $\mathcal{E}$ denotes the set of all effect laws of a domain, an example of which is $\neg \mathit{up} \to [\mathit{ toggle}] \mathit{light}$: whenever the switch is down, after toggling it, the room is lit up. If $\psi$ is inconsistent, we have a special kind of effect law that we call an inexecutability law. For example, broken $\to$ [ toggle ] $\perp$ says that toggle cannot be executed if the switch is broken.

Finally, we also define executability laws, which stipulate the context for an action to be executable. In $K_n$, we use $\langle a \rangle$ to express executability. $\langle a \rangle^\top$ thus reads “the execution of $a$ is possible”.

**Definition 3** An executability law for action $a$ is of the form $\varphi \to \langle a \rangle^\top$, where $\varphi \in \mathfrak{F} \mathit{ml}$.

For instance, $\neg$broken $\to$ $\langle$ toggle $\rangle^\top$ says that toggling can be executed whenever the switch is not broken. The set of all executability laws of a given domain is denoted by $\mathcal{N}$.

# 3 MODELS OF CONTRACTION

When an action theory has to be changed, the basic operation is that of contraction. (In belief-base update [33, 24] it has also been called erasure.) In this section we define its semantics.

In general we might contract by any formula $\Phi$. Here we focus on contraction by one of the three kinds of laws. We therefore suppose that $\Phi$ is either $\varphi$, where $\varphi$ is classical, or $\varphi \to [a]\psi$, or $\varphi \to \langle a \rangle^\top$.

For the case of contracting static laws we resort to existing approaches to change the set of static laws. In the following, we consider any belief change operator like Forbus' update method [9], the possible models approach [33, 34], WSS [14] or MPMA [6].

Contraction by $\varphi$ corresponds to adding new possible worlds to W. Let $\ominus$ be a given contraction operator for classical logic.

**Definition 4** Let $\langle W, R \rangle$ be a K<sub>n</sub>-model and $\varphi$ a classical formula. The model resulting from contracting by $\varphi$ is $\langle W, R \rangle_{\varphi}^{-} = \{\langle W', R \rangle\}$ such that $W' = W \ominus \mathit{val}(\varphi)$.

Observe that R should, a priori, change as well, otherwise contracting a classical formula may conflict with $\mathcal{X}$.<fnref n="2" /> For instance, if $\neg \varphi \to \langle a \rangle^\top \in \mathcal{X}$ and we contract by $\varphi$, the result may make $\mathcal{X}$ untrue. However, given the amount of information we have at hand, we think that whatever we do with R (adding or removing edges), we will always be able to find a counter-example to the intuitiveness of the operation, since it is domain dependent. For instance, adding edges for a deterministic action may render it nondeterministic. Depending on what changes to carry out on R when contracting static laws depends on the user's intuition, and unfortunately this information cannot be generalized and established once for all. We here opt for a priori doing nothing with R and postponing correction of executability laws.

Action theories being defined in terms of effect and executability laws, elaborating an action theory will mainly involve changes in these two sets of laws. Let us consider now both these cases.

Suppose the knowledge engineer acquires new information regarding the effect of action $a$. Then it means that the law under consideration is probably too strong, i.e., the expected effect may not occur and thus the law has to be weakened. Consider e.g. $\neg \mathit{up} \to [\mathit{ toggle}] \mathit{light}$, and suppose it has to be weakened to the more specific $(\neg \mathit{up} \wedge \neg \mathit{blackout}) \to [\mathit{ toggle}] \mathit{light}$.<fnref n="3" /> In order to carry out such a weakening, first the designer has to contract the set of effect laws and second to expand the resulting set with the weakened law.

Contraction by $\varphi \to [a]\psi$ amounts to adding some 'counterexample' arrows from $\varphi$-worlds to $\neg \psi$-worlds. To ease such a task, we need a definition. Let $\mathit{PI}(\varphi)$ denote the set of prime implicates of $\varphi$. If $\varphi_1, \varphi_2 \in \mathfrak{F} \mathit{ml}$, $\mathit{NewCons}_{\varphi_1}(\varphi_2) = \mathit{PI}(\varphi_1 \wedge \varphi_2) \setminus \mathit{PI}(\varphi_1)$ computes the new consequences of $\varphi_2$ w.r.t. $\varphi_1$: the set of strongest clauses that follow from $\varphi_1 \wedge \varphi_2$, but do not follow from $\varphi_1$ alone (cf. e.g. [20]). For example, the set of prime implicates of $p_1$ is just $\{p_1\}$, that of $p_1 \wedge (\neg p_1 \vee p_2) \wedge (\neg p_1 \vee p_3 \vee p_4)$ is $\{p_1, p_2, p_3 \vee p_4\}$, hence $\mathit{NewCons}_{p_1}((\neg p_1 \vee p_2) \wedge (\neg p_1 \vee p_3 \vee p_4)) = \{p_2, p_3 \vee p_4\}$.

**Definition 5** Let $\langle W, R \rangle$ be a K<sub>n</sub>-model and $\varphi \to [a]\psi$ an effect law. The set of models that result from contracting by $\varphi \to [a]\psi$ is $\langle W, R \rangle_{\varphi \to [a]}^{-} = \{\langle W, R \cup R'_a \rangle : R'_a \subseteq \{\langle w, w' \rangle : \mathbb{F}_w^{\mathcal{M}} \varphi, \mathbb{F}_{w'}^{\mathcal{M}} \neg \psi \text{ and } w' \setminus w \subseteq \mathit{lit}(\mathit{NewCons}_S(\neg \psi))\}\}$.

In our context, $w' \setminus w \subseteq \mathit{lit}(\mathit{NewCons}_S(\neg \psi))$ means that for all the added arrows, the new/extra effects of action $a$ are limited to

<footnote n="2">² We are indebted to the anonymous referees for pointing this out to us.</footnote>

<footnote n="3">³ Replacing the law by $\neg \mathit{up} \to [\mathit{ toggle}](\mathit{light} \vee \neg \mathit{light})$ looks silly.</footnote>
the consequences of the static laws combined with $\neg\psi$, i.e., all the ramifications that action *a* can produce.

Suppose now the knowledge engineer learns new information about the executability of *a*. This usually occurs when some executabilities are too strong, i.e., the condition in the theory guaranteeing the executability of *a* is too weak and should be made more restrictive. Let e.g. $\langle\text{ toggle}\rangle^\top$ be the law to be contracted, and suppose it has to be weakened to the more specific $\neg\text{broken} \to \langle\text{ toggle}\rangle^\top$. To do that, the designer first contracts the executability laws and then expands the resulting set with the weakened law.

Contraction by $\varphi \to \langle a \rangle^\top$ corresponds to removing some arrows leaving worlds where $\varphi$ holds. Removing such arrows has as consequence that *a* is no longer always executable in context $\varphi$.

**Definition 6** Let $\langle W, R \rangle$ be a $K_n$-model and $\varphi \to \langle a \rangle^\top$ an executability law. The set of models that result from the contraction by $\varphi \to \langle a \rangle^\top$ is $\langle W, R \rangle^-_{\varphi \to \langle a \rangle^\top} = \{\langle W, R' \rangle : R' = R \setminus R_a'', R_a'' \subseteq \{\langle w, w' \rangle : wR_a w' \text{ and } \models_w^{\langle W, R \rangle} \varphi\}\}$.

# 4 CONTRACTING AN ACTION THEORY

Having established the semantics of action theory contraction, we can turn to its syntactical counterpart. Nevertheless, before doing that we have to consider an important issue. As the reader might have expected, $K_n$ alone does not solve the frame problem. For instance,

$$ \left\{ \begin{array}{l} \text{up} \to \text{light}, \neg \text{up} \to [\text{ toggle}]_{\text{up}}, \\ \text{up} \to [\text{ toggle}] \neg \text{up}, \langle \text{ toggle} \rangle^\top \end{array} \right\} \nvDash_{\mathcal{R}_n} \text{broken} \to [\text{ toggle}]_{\text{broken}}. $$

We need thus a consequence relation powerful enough to deal with the frame and ramification problems. Hence the deductive power of $K_n$ has to be augmented to ensure that all the relevant frame axioms apply. Following the framework developed in [2], we consider logical information given in the form of dependence:

**Definition 7 (Dependence relation [2])** A dependence relation is a binary relation $\rightsquigarrow \subseteq \mathcal{A}ct \times \mathcal{L}it$.

The expression $a \rightsquigarrow l$ denotes that the execution of action *a* may change the truth value of the literal *l*. On the other hand, $\langle a, l \rangle \notin \rightsquigarrow$ (written $a \prec \lhd l$) means that *l* can never be caused by *a*. In our example we have *trigger* $\rightsquigarrow$ *light* and *trigger* $\rightsquigarrow$ $\neg$*light*, which means that action *trigger* may cause a change in literals *light* and $\neg$*light*. We do not have *trigger* $\rightsquigarrow$ $\neg$*broken*, for toggling the switch never repairs it.

**Definition 8** A model of a dependence relation $\rightsquigarrow$ is a $K_n$-model $\mathcal{M}$ such that $\models^\mathcal{M} \{\neg l \to [a] \neg l : a \prec l\}$.

We assume $\rightsquigarrow$ is finite. Given a dependence relation $\rightsquigarrow$, the associated consequence relation in the set of models for $\rightsquigarrow$ is noted $\models_{\rightsquigarrow}$. For our example we obtain

$$ \left\{ \begin{array}{l} \text{up} \to \text{light}, \neg \text{up} \to [\text{ toggle}]_{\text{up}}, \\ \text{up} \to [\text{ toggle}] \neg \text{up}, \langle \text{ toggle} \rangle^\top \end{array} \right\} \nvDash_{\rightsquigarrow} \text{broken} \to [\text{ toggle}]_{\text{broken}}. $$

We have *trigger* $\rightsquigarrow$ $\neg$*broken*, i.e., $\neg$*broken* is never caused by *trigger*. Hence in all contexts where *broken* is true, after every execution of *trigger*, *broken* still remains true. This independence means that the frame axiom *broken* $\to [\text{ toggle}]_{\text{broken}}$ is valid in the models of $\rightsquigarrow$.

Such a dependence-based approach has been shown [5] to subsume Reiter's solution to the frame problem [30] and moreover treats the ramification problem, even when actions with both indeterminate and indirect effects are involved [3, 16].

**Definition 9** An action theory is a tuple of the form $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle$.

In our running example, the corresponding action theory is

$$ S = \{\text{up} \to \text{light}\}, \mathcal{E} = \{\neg \text{up} \to [\text{ toggle}]_{\text{up}}, \text{up} \to [\text{ toggle}] \neg \text{up}\} $$

$$ \mathcal{X} = \{\langle \text{ toggle} \rangle^\top\}, \rightsquigarrow = \left\{ \begin{array}{l} \langle \text{ toggle}, \text{light} \rangle, \langle \text{ toggle}, \neg \text{light} \rangle, \\ \langle \text{ toggle}, \text{up} \rangle, \langle \text{ toggle}, \neg \text{up} \rangle \end{array} \right\} $$

And we have $S, \mathcal{E}, \mathcal{X} \nvDash_{\rightsquigarrow} \neg \text{up} \to [\text{ toggle}]_{\text{light}}$. (For parsimony's sake, we write $S, \mathcal{E}, \mathcal{X} \nvDash_{\rightsquigarrow} \Phi$ instead of $S \cup \mathcal{E} \cup \mathcal{X} \nvDash_{\rightsquigarrow} \Phi$.)

Let $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle$ be an action theory and $\Phi$ a $K_n$-formula. $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle^-_{\Phi}$ denotes the action theory resulting from the contraction of $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle$ by $\Phi$.

Contracting a theory by a static law $\varphi$ amounts to using any existing contraction operator for classical logic. Let $\ominus$ be such an operator. Moreover, based on [19], we also need to guarantee that $\varphi$ does not follow from $\mathcal{E}, \mathcal{X}$ and $\rightsquigarrow$. We define contraction of a domain description by a static law as follows:

**Definition 10** $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle^-_{\varphi} = \langle S^-, \mathcal{E}, \mathcal{X}^-, \rightsquigarrow \rangle$, where $S^- = S \ominus \varphi$ and $\mathcal{X}^- = \{(\varphi_i \wedge \varphi) \to \langle a \rangle^\top : \varphi_i \to \langle a \rangle^\top \in \mathcal{X}\}$.

We now consider contraction by an executability law $\varphi \to \langle a \rangle^\top$. For every executability in $\mathcal{X}$, we ensure that *a* is executable only in contexts where $\neg\varphi$ is true. The following operator does the job.

**Definition 11** $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle^-_{\varphi \to \langle a \rangle^\top} = \langle S, \mathcal{E}, \mathcal{X}^-, \rightsquigarrow \rangle$, where $\mathcal{X}^- = \{(\varphi_i \wedge \neg\varphi) \to \langle a \rangle^\top : \varphi_i \to \langle a \rangle^\top \in \mathcal{X}\}$.

For instance, contracting $\text{glued} \to \langle \text{ toggle} \rangle^\top$ in our example would give us $\mathcal{X}^- = \{\neg \text{glued} \to \langle \text{ toggle} \rangle^\top\}$.

Finally, to contract a theory by $\varphi \to [a]\psi$, for every effect law in $\mathcal{E}$, we first ensure that *a* still has effect $\psi$ whenever $\varphi$ does not hold, second we enforce that *a* has no effect in context $\neg\varphi$ except on those literals that are consequences of $\neg\psi$. Combining this with the new dependence relation also linking *a* to literals involved by $\neg\psi$, we have that *a* may now produce $\neg\psi$ as outcome. In other words, the effect law has been contracted. The operator below formalizes this:

**Definition 12** $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle^-_{\varphi \to [a]\psi} = \langle S, \mathcal{E}^-, \mathcal{X}, \rightsquigarrow^- \rangle$, where $\rightsquigarrow^- = \rightsquigarrow \cup \{\langle a, l \rangle : l \in \text{lit}(\text{NewCons}_S(\neg\psi))\}$ and $\mathcal{E}^- = \{(\varphi_i \wedge \neg\varphi) \to [a]\psi : \varphi_i \to [a]\psi \in \mathcal{E}\} \cup \{(\neg\varphi \wedge \neg l) \to [a] \neg l : \langle a, l \rangle \in (\rightsquigarrow^- \setminus \rightsquigarrow)\}$.

For instance, contracting the law $\text{blackout} \to [\text{ toggle}]_{\text{light}}$ from our theory would give us $\mathcal{E}^- = \{(\neg \text{up} \wedge \neg \text{blackout}) \to [\text{ toggle}]_{\text{up}}, (\text{up} \wedge \neg \text{blackout}) \to [\text{ toggle}] \neg \text{up}\}$.

# 5 RESULTS

We here present the main results that follow from our framework. These require the action theory under analysis to be modular [19]. An action theory is modular if a formula of a given type entailed by the whole theory can also be derived solely from its respective module (the set of formulas of the same type) with the static laws $S$. As shown in [19], to make a domain description satisfy such a property it is enough to guarantee that there is no classical formula entailed by the theory that is not entailed by the static laws alone.

**Definition 13 (Implicit static law [17])** $\varphi \in \mathfrak{F}ml$ is an implicit static law of $\langle S, \mathcal{E}, \mathcal{X}, \rightsquigarrow \rangle$ if and only if $S, \mathcal{E}, \mathcal{X} \nvDash_{\rightsquigarrow} \varphi$ and $S \nvDash \varphi$.
A theory is *modular* if it has no implicit static laws. Modularity of theories was originally defined in [19], but similar notions have also been addressed in the literature [4, 1, 35, 25]. A modularity-based approach for narrative reasoning about actions is given in [22].

To witness how implicit static laws can show up, consider the simple theory below, depicting the walking turkey scenario [32]:

$$ 
\begin{align*}
S &= \{ \text{walking} \to \text{alive} \}, \quad \mathcal{E} = \left\{ \begin{array}{l} [\text{tease}]\text{walking}, \\ \text{loaded} \to [\text{shoot}]\neg\text{alive} \end{array} \right\} \\
\mathcal{X} &= \left\{ \begin{array}{l} \langle\text{tease}\rangle^\top, \\ \langle\text{shoot}\rangle^\top \end{array} \right\}, \quad \nabla \Leftrightarrow \left\{ \begin{array}{l} \langle\text{shoot}, \neg\text{loaded}\rangle, \langle\text{shoot}, \neg\text{alive}\rangle, \\ \langle\text{shoot}, \neg\text{walking}\rangle, \langle\text{tease}, \text{walking}\rangle \end{array} \right\}
\end{align*}
$$

With this description we have $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \text{alive}$.<fnref n="4" /> As $S \models \text{alive}$, the formula alive is an implicit static law of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$.

Modular theories have several advantages [17, 15]. For example, consistency of a modular action theory can be checked by just checking consistency of S: if $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ is modular, then $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \bot$ if and only if $S \models \bot$. Deduction of an effect of a sequence of actions $a_1; \dots; a_n$ (prediction) needs not to take into account the effect laws for actions other than $a_1, \dots, a_n$. This applies in particular to plan validation when deciding whether $\langle a_1; \dots; a_n \rangle \varphi$ is the case.

Throughout this work we use multimodal logic $K_n$. For an assessment of the modularity principle in the Situation Calculus, see [18].

Here we show that our operators are correct w.r.t. the semantics. The first theorem establishes that the semantical contraction of models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ by $\Phi$ produces models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$.

**Theorem 1** Let $\langle W, R \rangle$ be a model of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$, and let $\Phi$ be a formula that has the form of one of the three laws. For all models $\mathcal{M}$, if $\mathcal{M} \in \langle W, R \rangle_{\bar{\Phi}}$, then $\mathcal{M}$ is a model of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$.

It remains to prove that the other way round, the models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$ result from the semantical contraction of models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ by $\Phi$. This does not hold in general, as shown by the following example: suppose there is only one atom $p$ and one action $a$, and consider the theory $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ such that $S = \emptyset$, $\mathcal{E} = \{p \to [a]\bot\}$, $\mathcal{X} = \{(a)^\top\}$, and $\nabla \Leftrightarrow \emptyset$. The only model of that action theory is $\mathcal{M} = \{{\neg p}\}, \{{(\neg p)}, \{\neg p\}}\}$. By definition, $\mathcal{M}_{p \to \langle a \rangle^\top} = \{\mathcal{M}\}$. On the other hand, $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{p \to \langle a \rangle^\top} = \langle \emptyset, \{p \to [a]\bot\}, \{\neg p \to \langle a \rangle^\top\}, \emptyset \rangle$. The contracted theory has two models: $\mathcal{M}$ and $\mathcal{M}' = \{{\langle p \rangle}, \{\neg p\}\}, \{{\neg p}\}, \{\neg p\}\}$. While $\neg p$ is valid in the contraction of the models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$, it is invalid in the models of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{p \to \langle a \rangle^\top}$.

Fortunately, we can establish a result for those action theories that are modular. The proof requires three lemmas. The first one says that for a modular theory we can restrict our attention to its 'big' models.

**Lemma 1** Let $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ be modular. Then $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \Phi$ if and only if $\models_{\mathcal{F}_\infty} \Phi$ for every model $\langle W, R \rangle$ of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ such that $W = \text{val}(S)$.

Note that the lemma does not hold for non-modular theories (the set $\{\langle W, R \rangle : \langle W, R \rangle$ is a model of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ and $W = \text{val}(S)\}$ is empty then).

The second lemma says that contraction preserves modularity.

**Lemma 2** Let $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ be modular, and let $\Phi$ be a formula of the form of one of the three laws. Then $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$ is modular.

The third one establishes the required link between the contraction operators and contraction of 'big' models.

**Lemma 3** Let $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ be modular, and let $\Phi$ be a formula of the form of one of the three laws. If $\mathcal{M}' = \langle \text{val}(S), R' \rangle$ is a model of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$, then there is a model $\mathcal{M}$ of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ such that $\mathcal{M}' \in \mathcal{M}_{\bar{\Phi}}$.

Putting the three above lemmas together we get:

**Theorem 2** Let $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ be modular, $\Phi$ be a formula of the form of one of the three laws, and $\langle S^-, \mathcal{E}^-, \mathcal{X}^-, \nabla^- \rangle$ be $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$. If $S^-, \mathcal{E}^-, \mathcal{X}^- \models_{\mathcal{F}_\infty} \neg \Psi$, then for every model $\mathcal{M}$ of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ and every $\mathcal{M}' \in \mathcal{M}_{\bar{\Phi}}$ it holds that $\models_{\mathcal{M}'} \Psi$.

Our two theorems together establish correctness of the operators:

**Corollary 1** Let $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ be modular, $\Phi$ be a formula of the form of one of the three laws, and $\langle S^-, \mathcal{E}^-, \mathcal{X}^-, \nabla^- \rangle$ be $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$. Then $S^-, \mathcal{E}^-, \mathcal{X}^- \models_{\mathcal{F}_\infty} \neg \Psi$ if and only if for every model $\mathcal{M}$ of $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ and every $\mathcal{M}' \in \mathcal{M}_{\bar{\Phi}}$, $\models_{\mathcal{M}'} \Psi$.

We give a sufficient condition for contraction to be successful.

**Theorem 3** Let $\Phi$ be an effect or an executability law such that $S \models_{\mathcal{F}_\infty} \Phi$, and let $\langle S^-, \mathcal{E}^-, \mathcal{X}^-, \nabla^- \rangle$ be $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}}$. If $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ is modular, then $S^-, \mathcal{E}^-, \mathcal{X}^- \models_{\mathcal{F}_\infty} \neg \Phi$.

# 6 DISCUSSION AND CONCLUSION

In this work we have presented a general method for changing a domain description (alias action theory) given any formula we want to contract. We have defined a semantics for theory contraction and also presented its syntactical counterpart through contraction operators. Soundness and completeness of such operators with respect to the semantics have been established (Corollary 1).

We have also shown that modularity is a sufficient condition for a contraction to be successful (Theorem 3). This gives further evidence that the notion of modularity is fruitful.

What is the status of the AGM-postulates for contraction in our framework? First, contraction of static laws satisfies all the postulates, as soon as the underlying classical contraction operation $\ominus$ satisfies all of them.

In the general case, however, our constructions do not satisfy the central postulate of preservation $\langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle_{\bar{\Phi}} = \langle S, \mathcal{E}, \mathcal{X}, \nabla \rangle$ if $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \Phi$. Indeed, suppose we have only one atom $p$, and a model $\mathcal{M}$ with two worlds $w = \{p\}$ and $w' = \{\neg p\}$ such that $wR_a w', w'R_a w$, and $w'R_a w'$. Then $\models_{\mathcal{M}} p \to [a]\neg p$ and $\models_{\mathcal{M}'} [a]\neg p$, i.e., $\mathcal{M}$ is a model of the effect law $p \to [a]\neg p$, but not of $[a]\neg p$. Now the contraction $\mathcal{M}_{[a]\neg p}$ yields the model $\mathcal{M}'$ such that $R_a = W \times W$. Then $\models_{\mathcal{M}'} p \to [a]\neg p$, i.e., the effect law $p \to [a]\neg p$ is not preserved. Our contraction operation thus behaves rather like an update operation.

Now let us focus on the other postulates. Since our operator has a behavior which is close to the update postulate, we focus on the following basic erasure postulates introduced in [23]. Let $Cn(\mathcal{T})$ be the set of all logical consequences of a theory $\mathcal{T}$.

<footnote n="4">⁴ Because first $\{\text{walking} \to \text{alive}, [\text{tease}]\text{walking}\} \models_{\mathcal{F}_\infty} [\text{tease}]\text{alive}$, second $\models_{\mathcal{F}_\infty} \neg \text{alive} \to [\text{tease}]\neg \text{alive}$ (from the independence $\text{tease} \nrightarrow \text{alive}$), and then $S, \mathcal{E} \models_{\mathcal{F}_\infty} \neg \text{alive} \to [\text{tease}]\bot$. As long as $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \langle \text{tease} \rangle^\top$, we must have $S, \mathcal{E}, \mathcal{X} \models_{\mathcal{F}_\infty} \text{alive}$.</footnote>
$$
\mathbf{KM1} \quad \mathrm{Cn}(\langle\mathcal{S}, \mathcal{E}, \mathcal{X}, \mathcal{N} \rangle_{\bar{\Phi}}) \subseteq \mathrm{Cn}(\langle\mathcal{S}, \mathcal{E}, \mathcal{X}, \mathcal{N} \rangle)
$$

Postulate **KM1** does not always hold because it is possible to make
the formula $\varphi \rightarrow [a] \perp$ valid in the resulting theory by removing
elements of $R_a$ (cf. Definition 6).

$$
\mathbf{KM2} \quad \Phi \notin \mathrm{Cn}(\langle\mathcal{S}, \mathcal{E}, \mathcal{X}, \mathcal{N} \rangle_{\bar{\Phi}})
$$

Under the condition that $\langle S, \mathcal{E}, \mathcal{X}, \mathcal{N} \rangle$ is modular, Postulate **KM2** is satisfied (cf. Theorem 3).

$$
\begin{array}{l}
\mathbf{KM3} \quad \text{If } \mathrm{Cn}(\langle S_1, \mathcal{E}_1, \mathcal{X}_1, \mathcal{N}_1 \rangle) = \mathrm{Cn}(\langle S_2, \mathcal{E}_2, \mathcal{X}_2, \mathcal{N}_2 \rangle) \\
\qquad \text{and } \vdash_{\mathbb{R}_n} \Phi_1 \leftrightarrow \Phi_2, \text{ then } \mathrm{Cn}(\langle S_1, \mathcal{E}_1, \mathcal{X}_1, \mathcal{N}_1 \rangle_{\bar{\Phi}_2}) = \\
\qquad \qquad \mathrm{Cn}(\langle S_2, \mathcal{E}_2, \mathcal{X}_2, \mathcal{N}_2 \rangle_{\bar{\Phi}_1}).
\end{array}
$$

**Theorem 4** If $\langle S_1, \mathcal{E}_1, \mathcal{X}_1, \mathcal{N}_1 \rangle$ and $\langle S_2, \mathcal{E}_2, \mathcal{X}_2, \mathcal{N}_2 \rangle$ are modular and the propositional contraction operator $\ominus$ satisfies Postulate **KM3**, then Postulate **KM3** is satisfied for every $\Phi_1, \Phi_2 \in \mathfrak{F}ml$.

Following [26, 27], Eiter et al. [7] have investigated update of ac-
tion theories in a fragment of the action description language $\mathcal{C}$ [11]
and given complexity results showing how hard such a task can be.

Update of action descriptions in their sense is always relative to
some conditions (interpreted as knowledge possibly obtained from
earlier observations and that should be kept). This characterizes a
constraint-based update, like ours.

Even though they do not explicitly state postulates for their kind of theory update, they establish conditions for the update operator to be successful. Basically, they claim for consistency of the resulting theory; maintenance of the new knowledge and the invariable part of the description; satisfaction of the constraints; and minimal change.

With their method we can also contract by a static and an effect
law. Contraction of executabilities are not explicitly addressed.

A main difference between the approach in [7] and ours is that
we do not need to add new fluents at every elaboration stage: we
still work on the same set of fluents, refining their behavior w.r.t.
an action *a*. In Eiter *et al.*'s proposal an update forces changing all
the variable rules appearing in the action theory by adding to each
one a new update fluent. This is a constraint when elaborating action
theories.

Here we have presented the case for contraction, but our defini-
tions can be extended to revision, too. Our results can also be gener-
alized to the case where learning new actions or fluents is involved.
This means in general that more than one simple formula should be
added to the belief base and must fit together with the rest of the the-
ory with as little side-effects as possible. We are currently defining
algorithms based on our operators to achieve that.

ACKNOWLEDGEMENTS

We are grateful to the anonymous referees for useful comments on
an earlier version of this paper. Ivan Varzinczak has been supported
by a fellowship from the government of the FEDERATIVE REPUBLIC
OF BRAZIL. Grant: CAPES BEX 1389/01-7.

REFERENCES

[1] E. Amir, ‘(De)composition of situation calculus theories’, in Proc. AAAI’2000, pp. 456–463. AAAI Press/MIT Press, (2000).

[2] M. A. Castilho, O. Gasquet, and A. Herzig, ‘Formalizing action and change in modal logic I: the frame problem’, *J. of Logic and Computation*, 9(5), 701–735, (1999).

[3] M. A. Castilho, A. Herzig, and I. J. Varzinczak, ‘It depends on the context! a decidable logic of actions and plans based on a ternary dependence relation’, in NMR’02, pp. 343–348, (2002).

[4] L. Cholvy, 'Checking regulation consistency by using SOL-resolution', in Proc. Int. Conf. on AI and Law, pp. 73–79, Oslo, (1999).

[5] R. Demolombe, A. Herzig, and I. Varzinczak, 'Regression in modal logic', *J. of Applied Non-Classical Logics*, **13**(2), 165–185, (2003).

[6] P. Doherty, W. Łukaszewicz, and E. Madalinska-Bugaj, 'The PMA and relativizing change for action update', in Proc. KR'98, pp. 258–269. Morgan, (1998).

[7] T. Eiter, E. Erdem, M. Fink, and J. Senko, 'Updating action domain descriptions', in Proc. IJCAI'05, pp. 418–423. Morgan, (2005).

[8] N. Y. Foo and D. Zhang, ‘Dealing with the ramification problem in the extended propositional dynamic logic’, in *Advances in Modal Logic*, volume 3, 173–191, World Scientific, (2002).

[9] K. D. Forbus, 'Introducing actions into qualitative simulation', in Proc. IJCAI'89, pp. 1273–1278. Morgan, (1989).

[10] P. Gärdenfors, *Knowledge in Flux: Modeling in Dynamics of Epistemic States*, MIT Press, 1988.

[11] M. Gelfond and V. Lifschitz, 'Action languages', *ETAI*, **2**(3–4), 193–210, (1998).

[12] S. O. Hansson, *A Textbook of Belief Dynamics: Theory Change and Database Updating*, Kluwer, 1999.

[13] D. Harel, 'Dynamic logic', in *Handbook of Philosophical Logic*, volume II, 497–604, D. Reidel, Dordrecht, (1984).

[14] A. Herzig and O. Rifi, 'Propositional belief base update and minimal change', *Artificial Intelligence*, **115**(1), 107–138, (1999).

[15] A. Herzig and I. Varzinczak. Metatheory of actions: beyond consistency. To appear.

[16] A. Herzig and I. Varzinczak, 'An assessment of actions with indeterminate and indirect effects in some causal approaches', Technical Report 2004-08-R, IRIT - Université Paul Sabatier, (May 2004).

[17] A. Herzig and I. Varzinczak, 'Domain descriptions should be modular', in Proc. ECAI'04, pp. 348–352. IOS Press, (2004).

[18] A. Herzig and I. Varzinczak, 'Cohesion, coupling and the meta-theory of actions', in Proc. IJCAI'05, pp. 442–447. Morgan, (2005).

[19] A. Herzig and I. Varzinczak, 'On the modularity of theories', in Advances in Modal Logic, volume 5, 93–109, King's College, (2005).

[20] K. Inoue, 'Linear resolution for consequence finding', *Artificial Intelligence*, **56**(2–3), 301–353, (1992).

[21] Y. Jin and M. Thielscher, 'Iterated belief revision, revised', in Proc. IJCAI'05, pp. 478–483. Morgan, (2005).

[22] A. Kakas, L. Michael, and R. Miller, 'Modular-E: an elaboration tolerant approach to the ramification and qualification problems', in Proc. LPNR'05, pp. 211–226. Springer, (2005).

[23] H. Katsuno and A. O. Mendelzon, 'Propositional knowledge base revision and minimal change', *Artificial Intelligence*, **52**(3), 263–294, (1991).

[24] H. Katsuno and A. O. Mendelzon, 'On the difference between updating a knowledge base and revising it', in *Belief revision*, ed., P. Gärdenfors, 183–203, Cambridge, (1992).

[25] J. Lang, F. Lin, and P. Marquis, 'Causal theories of action – a computational core', in Proc. IJCAI'03, pp. 1073–1078. Morgan, (2003).

[26] R. Li and L.M. Pereira, 'What is believed is what is explained', in Proc. AAAI'96, pp. 550–555. AAAI Press/MIT Press, (1996).

[27] P. Liberatore, 'A framework for belief update', in Proc. JELIA'2000, pp. 361–375, (2000).

[28] J. McCarthy, *Mathematical logic in artificial intelligence*, Daedalus, 1988.

[29] S. Popkorn, *First Steps in Modal Logic*, Cambridge, 1994.

[30] R. Reiter, 'The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression', in *Artificial Intelligence and Mathematical Theory of Computation: Perspectives in Honor of John McCarthy*, 359–380, Academic Press, (1991).

[31] S. Shapiro, M. Pagnucco, Y. Lespérance, and H. J. Levesque, 'Iterated belief change in the situation calculus', in Proc. KR'2000, pp. 527–538. Morgan, (2000).

[32] M. Thielscher, 'Computing ramifications by postprocessing', in Proc. IJCAI'95, pp. 1994–2000. Morgan, (1995).

[33] M.-A. Winslett, 'Reasoning about action using a possible models approach', in Proc. AAAI'88, pp. 89–93. Morgan, (1988).

[34] M.-A. Winslett, 'Updating logical databases', in *Handbook of Logic in AI and Logic Programming*, volume 4, 133–174, Oxford, (1995).

[35] D. Zhang, S. Chopra, and N. Y. Foo, 'Consistency of action descriptions', in Proc. PRICAI'02. Springer, (2002).

[36] D. Zhang and N. Y. Foo, 'EPDL: A logic for causal reasoning', in Proc. IJCAI'01, pp. 131–138. Morgan, (2001).