Terminological Logics with Modal Operators

1 Introduction

Terminological knowledge representation langua~es in the style ofKL-ONE [Brachman and Schmolze, 1985] have been developed as a structured formalism to describe the relevant concepts of a problem domain and the inter­ actions between these concepts. Various terminological systems have been designed and implemented that are based on the ideas underlying KL-ONE (see [Woods and Schmolze, 1992] for an overview). Representing know­ ledge of an application domain with such a kind of sy­ stem amounts to introducing the terminology of this do­ main via concept definitions, and then describing (an abstraction of) the relevant part of the "world" by li­ sting the facts that hold in this part of the world. In a traditional terminological system, such a description is rigid in the sense that it does not allow for the represen­ tation of notions like time, or beliefs of different agents . In systems modeling aspects of intelligent agents , howe­ ver, intentions, beliefs, and time-dependent facts play an important role.

Modal logics with possible worlds semantics is a for­ mally well-founded and well-investigated framework for the representation of such notions. The present paper is concerned with integrating modal operators (for time, belief, etc.) into a terminological formalism. The first task is to find an appropriate semantics for the combi­ ned language. In addition, if such a language should be used in a system, one must design algorithms for the im­ portant inference problems (such as consistency of kno­ wledge bases) for the language.

Several approaches have been proposed for the com­ bination of terminological formalisms with notions like time or beliefs. A very ·simple possibility to represent beliefs of agents is realized in the partition hierarchy SB­ PART [Kobsa, 1989], which is an extension of the SB­ ONE system. In this approach, each agent may have its own set of terminological axioms ( TBox), and these TBoxes can be ordered hierarchically. However, this ex­ tension lacks a formal semantics and it does not allow for representing properties of belief, such as introspec­ tion, or interactions between beliefs of different agents. A more formal approach is used in M-KRYPTON [Saf­ fiotti and Sebastiani, 1988], where a sub-language of the KRYPTON representation language is extended by modal operators B;, which can be used to represent the beliefs of agent i. Properties of beliefs are taken into consideration by using the well-known modal logic KD45. Due to the undecidable base language, however, . [Saffiotti and Sebastiani, 1988] just introduces a formal semantics, without giving any inference algorithms for the extended language. In [Schild, 1991], it has been shown that terminological systems already have a strong connection to modal logic. In fact, the concept langu­ age A.CC is nothing but a syntactic variant of the pro­ positional multi-modal logic K(m). Building upon this observation, [Schild, 1993] augments A.CC by tense ope­ rators. The two approaches that come next to the one we shall introduce below are described in [Laux, 1994a; 1994b] and in [Ohlbach and Baader , 1993]. Both extend A.CC by modal operators, but with different emphasis. The differences between these approaches and ours are clarified in the next section.

2 Classification

When extending a terminological knowledge representa­ tion language by modalities for belief, time, etc. one has various degrees of freedom. Before describing the specific choices made in this article, we shall informally explain the different alternatives.

For simplicity, assume that we are interested in time and belief operators only. Thus, in addition to the ob­ jects we have time points and belief worlds. This means that the domain of an interpretation is the Cartesian product D = Dobject X Dtime X Dbelief of the set of ob­ jects, the set of time points, and the set of belief worlds. Concepts are no longer just sets of objects; their inter­ pretation also depends on the actual belief world and time point. Thus, they can be seen as subsets of D, and not just as subsets of Dobject· Roles operate on objects, whereas modalities for time (like future or tomorrow) operate on time points, and modalities for belief (like bel-John) operate on belief worlds . As for concepts, ho­ wever, the interpretation of roles and modalities depends on all dimensions. Thus, a role loves is interpreted as a function from D into 2D object, which relates any indivi­ dual in Dobject (say John) with a set of individuals (the individuals John loves), but this set depends on the ac­ tual time point and belief world. Modalities like future are treated analogously. Modal operators can now be used both inside of concept expressions and in front of concept definitions and assertions . For example, we can describe the set of individuals that love a woman that­ according to John's belief-is pretty by the concept ex­ pression 3loves.(Womann [bel-John]Pretty), and we can express that-according to John's belief-a happy hus­ band is one married to a woman whom he (John) believes to be pretty by the terminological axiom

[bel-John](Happy-husband = 3 married-to.(Woman n [bel-John]Pretty)) .

The assertion [bel-John](future) (Peter married-to Mary) says that John believes that, at some point in the future, Peter will be married to Mary.

With the usual interpretation of the Boolean opera­ tors, of value and exists restrictions on roles, and of box and diamond operators for the modalities, this yields a multi-dimensional version of the multi-modal logic Km. As described until now, this logic is a strict sub-language of the one introduced in [Ohlbach and Baader, 1993]. The restriction lies in the fact that, unlike in [Ohlbach and Baader, 1993], we do not consider roles and modali­ ties that have a complex structure (such as [ wants]own, where the modality wants is used to modify the role own) . There are several reasons why this approach is not yet satisfactory. First, the object and the other dimen­ sions are treated analogously. This means, for example, that the interpretation of the modality future depends not only on the actual time point, but also on the current object and the belief world. Whereas the dependence from the belief world may seem to be quite reasonable, it is rather counterintuitive that the future time points reached from time t 0 are different, depending on whether we are interested in the individual Sue or Mary. Thus, it seems to be more appropriate to treat the object dimen­ sion in a special way: whereas the interpretation of roles should depend on the actual time point etc., the inter­ pretation of modalities should not depend on the object under consideration.

The need for a special treatment of the object dimen­ sion can also be motivated by considering the semantics of concept definitions (and assertions). In [Ohlbach and Baader, 1993], concept definitions are required to hold for all objects, time points, and belief worlds. This is a straightforward generalization of the treatment of de­ finitions in terminological languages, where a definition C = D must hold for all objects, i.e., in a model of C = D all objects o must satisfy that o belongs to the interpretation of C iff it belongs to the interpretation of D. For the other dimensions, however, this differs from the usual definition of models in modal logics, where a formula is only required to hold in one world.

Another problem is that not only the roles, but also all the other modalities are just interpreted in the ba­ sic logic K, i .e., they are not required to satisfy speci­ fic axioms for belief or time. In the present paper, we shall not take into account this last aspect, but we shall treat the object dimension in a special way, thus elimi­ nating; the problems mentioned above. In [Laux, 1994a; 1994bj both aspects are considered. However, modal operators are not allowed to occur inside of concept ex­ pressions, which considerably simplifies the al~orithmic treatment of the formalism. The difference to lOhlbach and Baader, 1993] is, on the one hand, the special tre­ atment of the object dimension. In addition, [Ohlbach and Baader, 1993j does not consider assertions, and even though concept definitions are introduced, they are not handled by the satisfiability algorithm. On the other hand, [Ohlbach and Baader, 1993] allows for very com­ plex roles and modalities, which are not considered here.

3 Syntax and Semantics of A.CCM

First, we present the syntax of our multi-dimensional modal extension of the concept language A.CC. As for A.CC, we assume a set of concept names, a set of role names, and a set of object names to be given. Beside the object dimension (which will be treated differently from the other dimensions), we assume that there are v 2: 1 additional dimensions (such as time points, epistemic alternatives, or intensional states). In each dimension, there can be several modalities, which can be used in box and diamond operators . For example, in the dimension time points we could have future and tomorrow, and in the dimension belief worlds we could have belief-John and belief-Mary. If o is a modality of dimension i we write dim(o) = i. In this case, [o] and (o) are modal operators of dimension i.

Definition 3.1 (Syntax) Concepts of A.CCM are in­ ductively defined as follows. Each concept name is a concept, and T and .l are concepts. If C and D are concepts, R is a role name, and o is a modality then C n D (concept conjunction), CUD (concept disjunc­ tion), ...,c (concept negation), 'V R.C (value restriction), 3 R.C (exists restriction), [o]C (box operator), and (o)C (diamond operator) are concepts.

Terminological axioms of A.CCM are of the form m (C = D) where C and D are concepts of A.CCM and m is a (possibly empty) sequence of modal operators. As­ sertional axioms of A.CCM are of the form m (xRy) or m (x : C) where x and y are object names, R is a role name, C is a concept, and m is a (possibly empty) se­ quence of modal operators. An A.CCM-formula is either a terminological or an assertional axiom.

Traditional terminological systems impose severe re­ strictions on the admissible sets of terminological axioms: (1) The concepts on the left-hand sides of axioms must be concept names, (2) concept names oc­ cur at most once as left-hand side of an axiom (unique definitions), and (3) there are no cyclic definitions. The effect of these restrictions is that terminological axioms are just macro definitions (introducing names for large descriptions), which can simply be expanded before star­ ting the reasoning process. Unrestricted terminological axioms are a lot harder to handle algorithmically (see, e.g., [Buchheit et al., 1993]), but they are very useful for expressing constraints on concepts that are required to hold in the application domain. In the presence of modal operators, the requirement of having unique definitions is not appropriate anyway. For example, Peter may have a definition of Happy-husband that is quite different from John's definition. Thus, it is desirable to have different definitions m 1 (A = C) and m2 (A = D) of the same concept name A for different modal sequences m1 and m 2 . Even though m 1 and m 2 are different, there can be interactions between these definitions . For example, m1 could be of the form (o) and m2 of the form [o] . Thus, it is not a priori clear how the requirement of "unique definitions" can be adapted to the case of terminological axioms with modal prefix. To avoid these problems, we consider the more general case where arbitrary axioms are allowed.

Let us now turn to the semantics of A.CCM. The mo­ dal operators will be interpreted by a Kripke-style pos­ sible worlds semantics . Thus, for each dimension i we need a set of possible worlds D; . Modalities of dimen­ sion i correspond to accessibility relations on D;, which may, however , depend on the other dimensions as well . Concepts and roles are interpreted in an object domain, but this interpretation also depends on the modal di­ mensiOns .

Definition 3.2 (Semantics) A Kripke structure I<= (W, r, K1) consists of a set W of possible worlds, a set of accessibility relations r , and a I< -interpretation I<1 over W, which are given as follows . First, the set of possible worlds W is the Cartesian product of non-empty domains D1 , ... , Dv, one for each dimension. Second, r contains for each modality o of dimension i an accessibility rela­ tion "{0 , which is a function 'Yo : W -+ 2D'. We also write ((dl, .. . ,d;, . .. , dv),(dl ,···,d;, . .. ,dv)) E 'Yo for d; E 'Yo ( d1, ... , d;, ... , d11 ) . Finally, the /{-interpretation I<1 consists of a domain D,.KI and an interpretation fun­ ction · KI. The domain is the union of non-empty do­ mains 6. K I ( w) for all worlds w E W. The interpre­ tation function associates ( i) with each object name x an element xK I E 6. I< I , ( ii) with each concept name A and world wE W a set (A , w)KI ~ D,.KI(w) , (iii) with the top concept and the bottom concept the sets (T, w)KI = D,.KI (w) and (.l , w)KI = 0 (for each world w), and (iv) with each role name Rand world wE W a binary relation (R,w)K 1 ~ D,.KI(w) x D,.KI(w) .

Note that the interpretation of object names does not depend on the particular world (i .e., we are using so­ called "rigid designators"), whereas the interpretation of concept and role names depends on the world. For a given world w, the interpretation of a concept A (resp. of a role R) in w is a subset of (resp. a binary relation on) the domain D,.KI(w) associated with w . The inter­ pretation of concept names and roles is expanded to the concept forming operators as follows: If C and D are concepts, R is a role, and w is a world, then

Observe that, for each concept C and world w , we have (C, w)KI ~ D,.KI (w) . Two A.CCM concepts C and D are called equivalent iff for all Kripke structures I< = (W,f,I<J) and all worlds .w E W we have (C,w)KI = (D, w)KI .

Now we can define under which conditions an A.CCM­ formula F is satisfied in a I<ripke structure I< = (W, r, I<1) and a world w E W, written as I<, w f= F, by inductwn on the length of the modal prefix:

Here G is an A.CCM-formula, C, D are concepts, x, y are object names, R is a role name , and o is a modality. A set {F1 , . .. , Fn} of A.CCM-formulas is satisfiable iff there exists a Kripke structure I< = (W, r , I<1) and a world w0 E W such that K , w0 f= F; for i = 1, . .. , n . In this case we write I< f= F1, ... , Fn .

Even though we have introduced a domain D,.KI(w) for each world w, we have not yet said anything ab­ out the relationship between the domains of different worlds. In the simplest approach, the domains D,.KI(w!) and 6. K I ( w2 ) of each pair w1 , w2 of worlds are indepen­ dent of each other . This approach is known as varying domain assumption. In most cases, however, it is more reasonable to assume certain relationships between the domains of different worlds. The most commonly used approach is the so-called increasing domain assumption, where D,.KI(w) ~ D,.KI(w') if the world w' is accessible from the world w , i .e., there exists a modality o such that (w, w') E 'Yo· The advantage of this approach is that domain elements that have been introduced in w can also be referred to in all worlds that are accessible from w, i .e., domain elements do not "vanish" when we move from one world to another . As a special case, the constant domain assumption is sometimes used , where the domains LlK 1 (wl) and LlK 1 (w2) are identical for all worlds w1 and w2. Finally, the decreasing domain assumption can be used to express that new domain elements cannot arise when moving from one world to another one. In Section 5 we shall see that changing the requirements on the relationship between domains of worlds considerably changes the set of satisfiable for­ mulas .

With the exception of Section 5, however, we shall restrict our attention to increasing domains in the fol­ lowing. Furthermore, we assume that all terminological axioms are of the form m ( C = T), where C is a concept and m is a (possibly empty) sequence of modal opera­ tors. As in the case of A.CC without modalities, it is easy to verify that this can be done without loss of generality.

4 Testing Satisfiability of A.CCM-formulas

We present an algorithm for testing satisfiability of a fi­ nite set { F1, .. . , Fn} of A.CCM-formulas.1 To keep not­ ation simple we assume (without loss of generality) that concepts are in negation normal form, i.e., negation signs occur immediately in front of concept names only. Our calculus for testing satisfiability of A.CCM-formulas is based on the notions of labeled A.CCM-formulas and of world constraint systems. A labeled A.CCM -formula con­ sists of an A.CCM-formula F together with a label l , written as F Ill . The Iabell is a syntactic representa­ tion of a world in which F is required to hold. A world constraint is either a labeled A.CCM-formula or a term l l><l 0 l', where l, l' are labels and l><l 0 is a syntactic re­ presentation of the accessibility relation of modality o. A world constraint system is a finite, non-empty set of world constraints.

A Kripke structure /{ = (W' r' /{I) satisfies a world constraint system W iff there is a mapping a that maps labels in W to worlds in W such that (i) I<, a(l) f= F for each world constraint FIll in W, and (ii) (a(l), a(l')) E /o for each world constraint ll><l 0 l' in W. A world con­ straint system W is satisfiable iff there exists a Kripke structure satisfying W. In order to test satisfiability of a set {F1, .. . , Fn} of A.CCM-formulas we translate this set into the world constraint system W0 = { x 0 : T lllo, F1 lllo, .. . , Fn lllo}, where xo is a new object name not occurring in { F1, .. . , Fn}, and 10 is an ar­ bitrary label (which is intended to represent the real world). We say the world constraint system W0 is indu­ ced by {F1, ... , Fn}· It is easy to verify that {F1, ... , Fn} is satisfiable iff W0 is satisfiable. The world constraint xo : T lllo can obviously be satisfied by any Kripke struc­ ture. This constraint is necessary to guarantee that the domains Ll K 1 ( w) of the canonical Kripke structure con­ structed in the proof of completeness are non-empty (see the full paper [Baader and Laux, 1994]).

The A.CCM-satisfiability algorithm takes as input a world constraint system W0 that is induced by a finite set of A.CCM-formulas. It successively adds new world constraints to W0 by applying several propagation rules, which will be defined later. A world constraint system that is induced by a finite set of A.CCM-formulas, or that is obtained by a finite sequence of applications of propagation rules to an induced system, will be called derived system.

1 It is easy to see that all the other interesting inference problems (like the subsumption or the instance problem) can be reduced to this problem.

In the following, we use the letters x, y, z to denote object names, l to denote labels, A, B to denote con­ cept names, C, D to denote concepts, and R to denote role names. If necessary, these letters will have an ap­ propriate subscript . Before introducing the propagation rules in a formal way (in Figure 1), let us first describe the underlying ideas on an intuitive level. The rules that handle the usual A.CC concept forming operators are well-known and rather straightforward (see, e.g., [Baa­ der and Hollunder, 1991]) . In order to illustrate the rules that handle modalities and world constraints of the form C =TIll, suppose that the A.CCM-formula (o) (B = T) is given, where o is a modality of some dimension. In or­ der to test satisfiability of this A.CCM-formula, we start with the induced world constraint system W0 = { x0 : T lllo, (o) (B = T) lllo} . By definition, W0 is satis­ fiable iff there is a Kripke structure /{ = (W, r, KI) , a mapping a , and a world wo = a(lo) E W such that x{! 1 E LlK 1 (w0 ) and K , w0 f= (o) (B = T) . Since I<, wo f= (o) (B = T) iff I<, w1 f= B = T for some world w1 with (wo, w!) E /o, the -+o rule adds the world con­ straints lo 1><1 0 It and B = T lll1 to Wo, where l1 is a new label. This yields the new world constraint system W1 = Wo U {lo l><lo it, B = T 1111}. Because of these­ mantics of A.CCM-formulas, we furthermore know that I<, w1 F B = Tiff 6 E (B, wl)Kr for all 6 E ~K1 (w1 ). By the increasing domain assumption, x{; 1 E ~K1 (w0 ) implies x{! 1 E ~K 1 (w!) . Summing up, we must guaran­ tee that x{; 1 E (B, w!)Kr and therefore must add the world constraint x0 : B 1111 to W.

More generally, we say that an object name x is re­ levant for label l (in a world constraint system W) iff there is a label l' occurring in W such that ( i) W con­ tains a world constraint of the form x : C Ill', x Ry Ill', or yRx Ill', and ( ii) l is accessible from l', i.e., either l is l' or there are world constraints l' 1><1 01 l1, ... , ln-1 l><lon l in W for some modalities o1, ... , On . Now, if x is relevant for l and there is a world constraint C = T Ill in W for some concept C, then the -+= rule adds x : C 111 to W (unless this world constraint is already contained in W) . In our example, this rule applies to W1, and it yields the world constraint system W2 = W1 U {x0 : B 1111}. To W2 no more propagation rules are applicable, and­ as shown in [Baader and Laux, 1994]- we can use this system to construct a Kripke structure that satisfies the A.CCM-formula (o) (B = T) . A world constraint system to which no more propagation rules are applicable will be called complete.

Termination of the propagation rule applications can only be guaranteed if applicability of the usual rule for handling exists restrictions is restricted in an appropriate way. This is due to the presence of axioms of the form C = T . To illustrate this problem, consider the world constraint system W= {x:AII1,3R.C= Till}. Sincex is relevant for l, the -+= rule adds x : 3 R. C Ill . Now, the usual propagation rule --+3 that treats exists restrictions would add xRy Ill andy: C Ill to W, where y is a new object. However, y is again relevant for l, and thus we must add y : 3 R.C Ill. The --+3 rule would thus be ap­ plicable to y: 3 R. C Ill, generating new world constraints yRz Ill and z:C Ill, etc.

In order to avoid such infinite chains of rule applica­ tion, we introduce the notion of blocked objects . 2 In­ tuitively, an object x is blocked w.r.t. label/ if we need not introduce a new object in order to be sure that the exists restrictions on x can be satisfied. Consider, for in­ stance, the world constraint system W = { x: 3 R. C Ill, x: DIll, xRy Ill, y: 3 R.C Ill}. In this case, it is sufficient to apply the --+3 rule just to x. In fact, since all constraints for y are also constraints for x, any contradiction that could be obtained by applying this propagation rule to y can already be obtained by applying it to x. The idea is thus to say that y is blocked by x with respect to a label/ if { C I y : C Ill E W} ~ { D I x : D Ill E W} . In the above example, y would thus be blocked by x, and the --+3 rule would only be applied to x. In general, this no­ tion of blocking is too strong, though. In fact, consider the system W' that is obtained from W by deleting the constraint x : DIll. In this system, x would be blocked by y and vice versa. Such cyclic blocking is clearly not ap­ propriate since contradictions that are possibly hidden in C would never be detected.

In order to avoid cyclic blocking, we assume that the (countably infinite) set of all object names is given by an enumeration Yl, Y2, Ya, ... We write y < x if y comes before x in this enumeration. This ordering is used as follows. Whenever a new object y is introduced by ap­ plying the --+3 rule to a world constraint system W, y is chosen such that all objects in W are smaller than y w.r.t. this ordering. In addition, only smaller objects can block a given object .

Definition 4.1 An object y is blocked by an object x w. r. t. label l in a world constraint system W iff { C I y : C Ill E W} ~ {D I x: DIllE W} and x < y.

Now, the --+3 rule is applicable to a world constraint x : 3 R.C Ill in a world constraint system W only if x is not blocked by some object z w.r.t. l in W. A for­ mal description of the propagation rules is given in Fi­ gure 1. Given a set {F1 , ... , Fn} of A.CCM-formulas the A.CCM -satisjiability algorithm proceeds as follows. Star­ ting with the world constraint system Wa that is induced by {F1, ... , Fn}, propagation rules are applied as long as possible.

The transformation rules are sound in the sense that, if W is a satisfiable world constraint system, each ap­ plicable propagation rule can be applied in such a way that the obtained derived system is satisfiable (see [Baa­ der and Laux, 1994] for a proof). For the "don't-know" non-deterministic --+u rule there are two alternative suc­ cessor systems, and soundness means that one of them is satisfiable if the original system is satisfiable. 3 For the other rules (which are deterministic), soundness just means that application of the rule transforms a satisfia­ ble system into a new satisfiable system. Furthermore, given an arbitrary induced world constraint system Wa, only a finite number of propagation rules can successi­ vely be applied, starting with Wa (see also [Baader and Laux, 1994] for a proof). This termination property me­ ans that, after a finite number of propagation rule ap­ plications to Wa we obtain a complete world constraint system (i.e., a system to which no more rules apply), say W'. If W' is satisfiable we can conclude that Wa is sa­ tisfiable (since Wa is a subset of W'). Otherwise, if W' is unsatisfiable, we can possibly derive another complete world constraint system from Wa by another choice for the non-deterministic --+u rule. If all the (finitely many) choices lead to an unsatisfiable complete system then so­ undness of the rules implies that the original system Wa was unsatisfiable.

2 This idea was already used in [Buchheit et al., 1993; Baader et al., 1994], with slightly differing definitions of blocked objects.

3 Note that the choice of an applicable rule is "don't-care"

Thus, it remains to be explained how satisfiability of a complete world constraint system can be decided. For this purpose, we say that a world constraint system W contains an obvious contradiction (or clash for short) if it contains either a pair of labeled A.CCM-formulas of the form x : A Ill and x : ...,A Ill or a labeled A.CC M-formula x: l.. Ill (for some object x, concept name A, and label l). Obviously, a world constraint system containing a clash is unsatisfiable. On the other hand, if a system is clash-free and complete then it is satisfiable (see [Baader and Laux, 1994] for a proof of this property, which shows completeness of the propagation rules). Summing up, we obtain the following theorem.

Theorem 4.2 Satisfiability of a finite set of A.CCM­ formulas is decidable if we assume increasing domains.

5 The Constant Domain Assumption

Up to now we have investigated increasing domains only. In this section we will consider the algorithmic conse­ quences of assuming that the domains of all worlds are identical. Since this constant domain assumption is a special case of assuming increasing domains, an appro­ priate extension of the presented A.CCM-satisfiability al­ gorithm might seem to be rather easy. The goal of this section is to point out why developing such an extended algorithm requires more than a straightforward modifi­ cation of the existing approach. In fact, until now we did not succeed in finding an appropriate modification. Nevertheless we think that pointing out the problems we have observed can be useful for anyone trying to solve this problem.

In a first attempt one could try to use the presented A.CCM-satisfiability algorithm for the case of constant domains as well. However, not surprisingly, this does not always yield the correct answers. For example, con­ sider the A.CCM-formulas ([o]-,A) = T and (o) (x: A) where o is a modality, x an object, and A a concept name. It is easy to see that an application of the A.CCM-satisfiability algorithm to the induced system {xa : T lila, ([o]-,A) = T lila, (o) (x : A) lila} yields

non-deterministic, i.e., we need not try different orders of rule applications.

W-+o {ll><lol',~.p'lll'}UW if <pIll is in W, where <pis (o) F (resp. x: (o) C), <p 1 is F (resp. x: C), there is no label/" in W such that the world constraints l 1><1 0 l" and <p 1 Ill" are in W, and l' is a new label. W-+o{~.p'lll'}UW if <pIll and 11><1 0 l' are in W, where <pis [o] F (resp. x : [o] C) , <p 1 is F (resp. x :C), and <p 1 Ill' is not in W. W-+n {x :Ctlll,x:C2IIl}uW if X : Ct n c2 Ill is in w and w does not contain both world constraints X: Ct Ill and X: c2 Ill. W-+u {x :DIIl}uW if X :Cl u C2lll is in w, neither X : Ct Ill nor X: C2lll is in w, and Dis either cl or c2 . w -+3 { xRy Ill, y: c Ill} u w if x: 3 R.C Ill is in W, x is not blocked in W, and y is a new object such that y > z for all objects z occurring in W . w -+'v' {y:C Ill} u w if x : V R. C Ill and x Ry Ill are in W and W does not contain the world constraint y: C Ill . W -+: {x : C Ill} U W if x is relevant for l, C = T Ill is in W, and x : C Ill is not in W.

a complete and clash-free derived system. The reason is that the object name x is not relevant for lo . This shows that the above A.CCM-formulas are satisfiable if we as­ sume increasing domains. On the other hand, assuming constant domains causes unsatisfiability .. Suppose, to the contrary, that I<= (W, r, I<r) is a Kripke structure such that I<, w I= ([o]...,A) = T and I<, w I= (o)(x :A) for some world w in W. Because of I<, w I= (o) (x : A) there exists a world w' with (w, w') E 'Yo and I<, w' I= x : A, i.e. xKr E (A, w')Kr . On the other hand, however , we have xKr E (-,A, w')Kr because of (i) xKr E ~K 1 (w) (con­ stant domain assumption) and (ii) I<, w I= ([o]--,A) = T.

In the A.CCM-satisfiability algorithm we took the in­ creasing domain assumption into consideration by an ap­ propriate definition of the notion of "relevant objects," which was then used in the -+: rule: given a labeled A.CCM-formula C = TIll in a derived system W, the -+: rule adds the labeled A.CCM-formula x: C Ill to W whenever x is relevant for l . Recall that an object x is said to be relevant for label l if there is a label l' occur­ ring in W such that ( i) W contains a world constraint of the form x : C Ill', xRy Ill', or yRx Ill', and (ii) lis accessible from l'. Now, if we want to deal with constant domains, a promising approach seems to be a modifi­ cation of the -+: rule according to the following idea. Suppose W to be a derived system and l , l' to be labels in W . Furthermore, let I< = (W, r, I<r) be a Kripke structure that satisfies W. Because of the constant do­ main assumption we know that xKr E ~K 1 (w) for each world w in W, whenever there is a world constraint of the form x: DIll, xRy Ill, or yRx Ill in W. In this case we say that x is a top-level object in W (to distinguish it from objects occurring only inside assertional axioms with leading modal operators) . If x is a top-level ob­ ject in W , and if the world constraint C = T Ill' occurs in W, then the -+: rule must add X : c Ill' to windependently from the fact whether or not x is relevant for l' (where "relevant" is defined as in the increasing domain approach) . This consideration leads us to a mo­ dified rule -+=' to handle world constraints of the form C =TIll, which is given by

This apparently "slight" modification of the -+: rule may, however, cause infinite chains of propagation rule applications. As an example, consider the world con­ straint system W that consists of the two labeled A.CCM­ formulas xo: T lllo and ( (o) 3 R.C) = T lllo, where o is an arbitrary modality. An application of the -+=' rule yields the derived system W1 = WU{xo: (o)3 R.CIIlo}, and, by one application of the -+o and of the -+3 rule each, we obtain W2 = WtU{lo l><lo lt,xo:3R.CIIlt,xoRxtlllt,xt: C lilt} where x1 is a new object and l1 is a new la­ bel. Because of the newly introduced object x1 and the world constraint ( ( o) 3 R. C) = T lllo in W2, the -+=' rule is again applicable, and yields W3 = W2 U { Xt : (o) 3 R.C lllo} . However, to x1: (o) 3 R.C lllo the same propagation rules are applicable as to xo : (o) 3 R.C lllo before. This means, another new label and a new object are introduced, and so on. Note that none of the ne­ wly generated objects is ever blocked since they all have different world labels. In order to avoid such infinite chains of propagation rule applications, the definition of blocked objects must be modified such that assertions with other labels are taken into account as well.

To sum up, we have seen that the problem of how to avoid infinite chains of propagation rule applications is more complicated if we are dealing with constant do­ mains. In particular , the above example shows that, for testing whether or not an object is blocked w.r.t . some labell, it is not sufficient to consider only A.CCM-formulas that are' labeled with l . A straightforward generaliza­ tion of the notion of blocked objects (called cd-blocked) is obtained by allowing for different labels l and l' when considering the sets of concept assertions for the objects x andy.

Although this modification can handle the above ex­ ample correctly, it is not sufficient in general. On the one hand, it can become necessary to consider A.CCM­ formulas with more than two different labels as well as information about role-successors in the current world constraint when testing whether or not an object should be blocked. On the other hand, the test whether or not the -+3 rule must be applied in a world constraint sy­ stem W may depend on the information W (implicitly) contains about the accessibility relations of Kripke struc­ tures satisfying W . The full paper [Baader and Laux, 1994] contains examples that illustrate these problems. Due to these rather complex interactions, we did not yet succeed in finding an appropriate definition of cd­ blocked objects in world constraints. We thus leave this definition as an open problem for the moment. 4

6 Conclusion

The framework for integrating modal operators into ter­ minological knowledge representation languages presen­ ted in this paper should be seen as the starting point for developing more elaborate hybrid languages of this type. Extensions in at least two directions will be necessary.

First, for the adequate representation of notions like belief and time, the basic modal logic K is not sufficient . Instead, one must consider modalities that satisfy appro­ priate modal axioms. Second, the multi-dimensionality of our language has not really been made use of. In fact, it is easy to see that with respect to satisfiabi­ lity there is no difference between the v-dimensional and the corresponding !-dimensional case (see [Baader and Laux, 1994] for details) . We have introduced a multi­ dimensional framework since it is more flexible . In an extended language, different dimensions could satisfy dif­ ferent modal axioms (e.g., KD45 in the belief dimension, and at least 54 in the time dimension) . 5 In addition, one might want to specify certain interactions between diffe­ rent dimensions such as independence of one dimension from certain other dimensions.

The reason for considering a simplified framework without any of these extensions in the present paper is that in this context it is possible to design a rather intuitive calculus for satisfiability. Also, the proof of soundness, termination and completeness of this calcu­ lus is still relatively short and comprehensible. For this reason, we claim that this calculus can serve as a basis for satisfiability algorithms for more complex languages.

4 [Donini et al., 1992] use constant domain assumption in their epistemic extension of A.CC. However, since they consi­ der a nonmonotonic version of SS, the algorithmic problems are quite different.

5 ln the propositional case, the combination of different modal logics obtained this way corresponds to what Gabbay calls "dove-tailing of propositional modal logics" [Gabbay, 1994].

Another topic of future research will be investigating the constant domain assumption and its algorithmic ramifi­ cations. The answer to the question whether constant domain assumption or increasing domain assumption is more appropriate from the semantic point of view stron­ gly depends on the intended interpretation of the modalities (belief, knowledge, time, etc.) . ·