What's in an Aggregate: Foundations for Description Logics with Tuples and Sets

1 Introduction

Description logics are AI formalisms that allow one to represent domain knowledge by focusing on classes of ob­ jects [Brachman, 1977] and their relationships [Woods, 1975], and by offering specialized inferences on the class structure.

The research developed in the last decade offers a quite complete picture of several issues related to the expres­ sive power of the logics and the computational complex­ ity of the reasoning tasks (see [Woods and Schmolze, 1992]) . Based on the outcome of this research, attempts have been made to propose description logics as unifying formalisms for the various class-based representation lan­ guages used in different areas, such as semantic networks, feature logics, conceptual and object-oriented database models, type systems, and other formalisms used in software engineering [Bergamaschi and Sartori, 1992; Piza et al., 1992; Bor~ida, 1992; Calvanese et al., 1994; Schreiber et al., 1993]. However, these attempts have made apparent that description logics that are equipped with sound, complete, and terminating reasoning pro­ cedures still suffer from several limitations that are not acceptable when representing complex domains in the different fields mentioned above. Here is a list of the most important limitations.

• The domain of interpretation is flat, in the sense that the logics consider the world as constituted by elemen­ tary objects (grouped in concepts) and binary relations between them. One consequence of this property is that N-ary relations are not supported (an exception is the logic proposed in [Schmolze, 1989], for which no com­ plete decision procedure was proposed). In fact , N-ary relations have been shown to be important in several contexts (see [Catarci and Lenzerini, 1993]) , especially in databases and in natural language. For example, exam is correctly modeled as a ternary relation over student , professor and course. Note that supporting N-ary rela­ tions means that the logic offers suitable mechanisms for their definition and their characterization. For example, one has to ensure that no pair of instances of exam ex­ ist connecting the same triple of objects; also, one may want to assert that students linked to graduate courses by the relation exam are graduate students. These kinds of properties cannot be represented by simply modeling the N-ary relation in terms of N binary relations.
• Usually, general inclusion axioms are not supported. Although inclusion axioms are essential when we want to assert properties of classes and relations, as required in complex domains, most of the research on descrip­ tion logics either deals with class descriptions only, or impose severe restrictions, such as acyclicity, on axioms. Exceptions are, for example, [Nebel, 1991; Baader, 1991; Schild, 1991~ De Giacomo and Lenzerini, 1994; Buchheit et al., 1993J. An important outcome of this research is that reasoning with axioms is computationally hard, even for the simplest description logics (weaker than :Fe- [Woods and Schmolze, 1992]). All these works, however, limit their attention to axioms on concepts, and do not consider the problem of expressing inclusion axioms on relations.
• Relationships between classes are generally described by means of poor representation mechanisms. Indeed, when trying to use description logics for capturing repre­ sentation formalisms used in different fields, one realizes that three features are essential: the ability of navigat­ ing relationships (say of a semantic network or of an entity-relationship schema) in both directions. The abil­ ity of stating cardinality constraints of general forms on relationships. The possibility of conceiving a relation­ ship like a set , thus applying set theoretic operators on

them (including the notorious role value map [Woods and Schmolze, 1992]}.

The aim of the present work is to devise a description logic, called CATS, that finally addresses the above is­ sues. The basic ingredients of CATS are classes and links. Differently from traditional description logics, classes are abstractions not only for a set of individu­ als (corresponding to the usual notion of concept, called simple class here), but also for sets that have aggregates as instances (called aggregate classes). There are two types of aggregates: property aggregates and instance aggregates. A property aggregate is an abstraction for an object that is considered as an aggregation of other objects, one for each attribute belonging to a specified set [Smith and Smith, 1977]. A typical example of such an aggregate is a date, which is seen as an aggregation of three objects, one for the attribute day, one for the at­ tribute month, and one for the attribute year. Another example of property aggregate is an exam, which again is seen as an aggregation of three objects (one professor, one student and one course) . This makes it clear that N­ ary relations can be modeled as classes whose instances are aggregates. An instance aggregate is an abstraction of a group of other objects belonging to a certain class [Brodie and Ridjanovic, 1984]. A typical example of such an aggregate is a team, which can be seen as a group of players. Like any other description logics, CATS allows one to form complex classes by applying suitable con­ structors to both simple and aggregate classes. Notably, CATS includes a form of role value map, and the most general form of number restrictions (called qualified).

Links are abstractions for atomic, basic, and complex relationships between classes. An atomic link (denoted simply by a name, and also called attribute) is the most elementary mean for establishing a relationship between classes. A basic link is formed by applying certain con­ structors (like inverse, union, intersection and difference) to atomic links, and a complex link is formed by apply­ ing more complex constructors (like chaining, transitive closure, and identity) to basic links.

A knowledge base in CATS is simply a set of inclu­ sion axioms. We point out that CATS allows inclusion assertions to be stated on classes of all kinds (simple, aggregate, and complex), and on basic links, with no limitation (for example on cycles). A particular care is put in devising CATS so that its reasoning tasks remain decidable and even with the same computational com­ plexity as the simplest description logics where inclusion axioms are allowed. Indeed, we describe a technique for computing logical implication in CATS, and show that this problem is both EXPTIME-hard, and decid­ able with exponential time in the worst case.

The paper is organized as follows. Section 2 briefly re­ calls the description logics CI:F [De Giacomo and Lenz­ erini, 1994], which is the basis of the present work. Sec­ tion 3 presents our logic CATS, which adds to CI:F suit­ able constructors for representing aggregations, complex links, and qualified number restrictions. In Section 4, we show examples of knowledge bases built using CATS, and compare the expressive power of the logic with other similar formalisms for knowledge representation. Section 5 illustrates the salient features of the technique we use for computing logical implication in CATS, and discusses the computational complexity of this problem. Finally, conclusions are drawn in Section 6.

2 Preliminaries

Traditionally, description logics allow one to represent a domain of interest in terms of concepts and roles. Con­ cepts model classes of individuals, while roles model bi­ nary relations between classes. Starting with atomic con­ cepts and atomic roles, which are concepts and roles de­ scribed simply by a name, complex concepts and roles can be build by means of suitable constructors.

In the following, we focus on the description logic CI:F studied in [De Giacomo and Lenzerini, 1994], whose lan­ guage has the following syntax:

where A denotes an atomic concept, C (possibly with subscript) a generic concept, P an atomic role, R (pos­ sibly with subscript) a generic role.

In description logics, an interpretation I = (~I, 'J consists of a nonempty .domain of interpretation ~ , and an interpretation function .I satisfying the follow­ ing conditions (U{} denotes the cardinality of a set, and a= pIp-):

AI c ~I (C1 flC2)I = Cf nC~ (-,C)I =~I_ CI ("'R.C)I ={dE ~I I "'d'.(d, d') E RI :::> d' E CI} (:S 1 a)I ={dE ~I I U{d' I (d, d') E ai}::; 1} piC ~I X ~I (R1 U R2)I = RJ U R} (R1 o R2)I = R1 o R2 (R*)I = (RI)· (R-)I = {(d1, d2) E ~I x ~I I (d2, dl) E RI} id(C)I = {(d, d) E ~I X ~I IdE CI}.

Note that CI:F has a very expressive language, compris­ ing all usual concept constructs, and a rich set of role constructs, namely: union of roles R1 U R2 , chaining of roles R1 o R2, reflexive-transitive closure of roles R*, in­ verse roles R-, and the identity role id( C) projected on C. Moreover CI:F supports the simplest form of cardi­ nality constraints, namely functional restrictions of the form (:S 1 P), interpreted as the set of individuals for which the role P is functional. Notably, functional re­ strictions can be applied to both atomic roles and inverse of atomic roles. In fact, in CI:F there is a perfect symme­ try between roles and inverse roles, that will be the basis for the extensions of the logic discussed in this paper.

Let C be any description logic. An C TBoxl JC is a finite set of axioms of the form C1 ~ C2 , called inclu­ sion assertions, where C1 and C2 are C concepts. An interpretation I satisfies an inclusion assertion C1 ~ C2

1 TBox is the term traditionally used for naming the set of axioms constituting the intensional level (schema level) of a knowledge base.

if Cf ~ Cf. An interpretation I is a model of a TBox K if I satisfies each inclusion assertion inK.

The most important form of reasoning in a TBox is logical implication: a TBox IC logically implies an asser­ tion C1 [;:; C2, written IC f= C1 [;:; C2, if C1 [;:; C2 is satisfied by every model of K . It is well known that all basic reasoning tasks can be ~linearly) reformulated as logical implication in a TBox.

In [De Giacomo and Lenzerini, 1994], it is shown that logical implication in CI:F TBoxes, is an EXPTIME­ complete problem. This result was devised in the set­ ting of the correspondence between description logics and propositional dynamic logics, originally pointed out in [Schild, 1991]. One consequence is that logical im­ plication in CI:F can be decided by means of the deci­ sion procedures designed for satisfiability checking in dy­ namic logics. This is the first decidability result for a de­ scription logic including axioms, inverse roles, and func­ tional restrictions, a fundamental combination as seen in the introduction, and also contributed to the research on modal logics of programs, since the decidability of the propositional dynamic logic corresponding to CI:F was not known. Note that, CI:F is one of the very few description logics that lacks the finite model property, which means that certain CI:F TBoxes admit only in­ finite models. This is one of reasons why proving the above result required a quite sophisticated technique.

In the following, we will refer to a further descrip­ tion logic, called CI Q, which is obtained from CI:F by extending functional restrictions to qualified number re­ strictions (~ k a.C), whose meaning in an interpretation I is (k is any integer 3 ;::: 1):

3 The description logic CATS

In this section, we provide the formal definition of CATS. As we said in the introduction, the language of CATS supports classes and links. Classes are parti­ tioned into simple classes and aggregate classes, which are further distinguished in property aggregate and in­ stance aggregate classes. Links are partitioned into atomic (also called attributes), basic, and complex.

Let a nonempty finite alphabet A of atomic classes (classes denoted simply by a name, no matter if simple ·or aggregate) and a nonempty finite alphabet U of at­ tributes be available. We use A for a generic element of A, U (possibly with subscript) for a generic element of U, C (possibly with subscript) for a generic class, b (possibly with subscript) for a generic basic link, and L (possibly with subscript) for a generic complex link. The language of CATS has the following syntax (n, k;::: 1) :

2 Actually, in description logics having a. language rich enough, logical implication ca.n in turn be (polynomia.lly) re­ duced to sa.tisfia.bility of a. single concept . This is basically due to the ability of expressing reflexive-transitive closure of roles, together with the "connected model property" , i.e. if a TBox has a model, it has a. model which is connected (see [Schild, 1991; De Giacomo a.nd Lenzerini, 1994]).

3 We assume that integers a.re coded in unary.

c ::= A I r(U1, ... , Un) I x(C, u1 , ... , Un) I cr(C) I c1 n c2 1 ...,c 1 v L.c 1 (~ k b.C) 1 (~ kb- .c) 1 (b1 ~ b2) I (b1 ~ b2)

b

L

u 131 b1 u b2 I b1 \ b2

biL1oL2IL1UL2IL* IL-Iid(C)

We use a (possibly with subscript) forb and b-, and we adopt the following abbreviations: T :::::: AU-,A, l.. :::::: -, T, T :::::: r(UI) U · · · U r(Um) (where {U1, ... , Um} = U) , cr:::::: cr(T), C1 U C2:::::: ...,(...,C1 n -,C2), 3L.C:::::: -,'f£.-,C, 0 ::::::3 \ 3 , (;::: ka.C) = -,(~ k + 1a.C), a1 n a2 :::::: a1 \ (a1 \ a2), and (a1 = a2) = (a1 ~ a2) n (a2 ~ a1). Parentheses are used to disambiguate expressions.

The semantics for the lanp,uage of CATS is based on an interpretation I = ( oz, · ) , where (]I is the universe of the interpretation, and .I is the interpretation func­ tion over such a universe. Differently from the usual notion of interpretation, oz is a nonempty set of poly­ morphic objects, which means that every object in oz has none, one, or both of the following two forms :

• L The form of tuple: when an object has this form, it can be considered as a property aggregation, which is formally defined as a partial function from U to oz. We use the term tuple to denote an object in oz that has the form of tuple, and we write (U1 : 01, . . . , Un : on) 4 to denote any tuple t such that , for each i E {1, ... , n} , t(Ui) is defined and equal to Oi (which is called the Ui-component oft) . Note that the tuple t may have other components as well , besides the Ui-components.
• The form of set: when an object o has this form, it can be considered as an instance aggregate, which is formally defined as a nonempty finite collection of objects in oz, with the following proviso: the view of o as a set is unique, in the sense that there is only one finite collection of objects of which o can be considered an aggregation, and no other object o' is the aggregation of the same collection. We use the term set to denote an object in oz that has the form of set, and we write ~o1 , ... , On~ to denote the collection whose members are exactly o1, ... , On .

Objects having none of these forms are called elementary objects- i.e., individuals with no structure.

The interpretation function .I is defined as follows:

• It assigns to 3 a subset of oz x oz such that for each ~ ... , o, ... ~ E oz, we have that (~ .. . ,o, ... ~,o) E 3I .
• It assigns to every attribute U a subset of oz x oz such that, for each ( . .. , U : o, ... ) E or, (( . . . ,U : o, ... ), o) E uz , and there is no o' E oz different from o such that(( ... , U : o, . .. ), o') E uz. Note that this implies that every U in a tuple is functional for the tuple.

4 This notation makes it clear that a tuple is indeed a function assigning one element of oz to some of the elements ofU.

• It assigns to every basic link a subset of oz x oz such that the following conditions are satisfied:
• It assigns to every complex link a subset of oz x oz such that the usual conditions for o, U, *, -, and id are satisfied (see Section 2).
• It assigns to every class a subset of oz in such a way that the following conditions are satisfied:
• -AI~ oz

bf ubf bf- bf {(o,o') I (o',o) E bz}.

- r(Ul, ... ,Unt = {(Ul: Ol,···,Un: On) E OI I 01, ... , OnE 0 } - x(C, U1, ... , Un)z = S ~ r(U1, ... , Un) n cz and no distinct s, s' E S have the same U1, ... , Un­ components - u(C)I = { ~ol, ... ' On~E oz I 01, ... ' OnE cz} - (C1 n C2)z = Cf n Cf - ( ...,c)z = oz - cz - (VL.C)I = {o E oz I Vo'.(o, o') E RI :::> o' ELI} - (~ ka.C)I = {o E oz I H(o,o') E ai/\0 1 E cz} ~ k} - (a1 ~ a~I = {o E oz I {o' I (o, o') E af} ~ {o' I (o,o') E a2 }}.

A CATS TBox JC is a finite set of inclusion assertions of the form cl ~ c2, where cl and c2 are classes in CATS (we write C1 = C2 for C1 ~ C2, C2 ~ C1). As usual, an interpretation I satisfies C1 ~ C2 if Cf ~ C{, and JC F c1 ~ c2, if c1 ~ c2 is satisfied by every model of JC, i.e. by every interpretation that satisfies all assertions in JC.

4 Examples and discussion

The goal of this section is to discuss, by means of exam­ ples, the most important modeling capabilities of CATS, and to compare our logic with other representation for­ malisms.

Example 1: Propositional formulae

Figure 1 shows a simple TBox 1l defining several well known classes of propositional conjunctive normal form formulae. This example basically shows the power of instance aggregates and qualified number restrictions. None of the decidable description logics that we are aware of is rich enough to express the TBox in the figure. Note that PosLit ~ x(PosLit, letter) imposes that no two positive literals have the same variable (the same for NegLit). As an example of inference, 1l correctly classi­ fies u(Clause) n '</ 3 .((~ 2 3 . T) n 3 3 .NegLit) under both Horn and Krom.

Example 2: Families, persons, and cities

Figure 2 shows a TBox JC modeling a world with persons, families and cities. The following observations help un­ derstanding the expressive power of CATS.

Formula= u(Clause) Clause= EmptyCl U u(Li teral) EmptyCl !; V 3 ,...,Literal Literal:= (PosLit U NegLit) n r(letter) n Vletter.Var PosLit !; x(PosLi t, letter) n -.NegLi t NegLit !;x(NegLit,letter) Var!; (3letter- .NegLit) n (3letter- .PosLit)n (:5 2letter-. T) HornCl =:Clausen($ 1 3 .PosLit) TwoClause =:Clausen (:52 3 · T) Horn := Formula n V 3 .HornCl Krom := Formula n V 3 · TwoClause

T!; (father n mother<; 0)n (fathern children<; 0)n ( childrenn mother<; 0) T!; Vfather- U mother- U children- .Family Date:= x(Date, day, month, year) 3date-. T!; Date 3day-. T !; Day 3month-.T!;Month 3year-. T !; Year 3city-.T!; City Day U Month U Year !; ...,T n -.u Mayor = 3mayor-. T 3mayor. T !; City City!; r(name,state,country,mayor)n x(City, name, state, country) n x(City, mayor) Family!; u(Person) n r(father, mother, date, ci ty)n x(Family,father,mother,date)n (3= father U mother U children) StillFamily!; Family n x(StillFamily, father, mother) PhdFamily := (2:: 3 3 .PhdPerson) n (:5 1 3 .-.PhdPerson) Person!; (3children-. T) n (:5 1 children-. T) ChildOfMayor = 3children- o father.Mayor VeryPhd = V( children- o (father U mother))* .PhdPerson

• Objects are polymorphic. For example, every in­ stance of Family (representing families resulting from a marriage) can be seen both as a set of per­ sons, and as a tuple with attributes father, mother, date (of marriage) and city (of marriage). Note, however, that assertions can be used to impose that the instances of a certain class (Day, Month and Year in our example) can only be seen as elementary ob­ jects.
• Inclusion assertions on classes are used with no lim­ itation. In particular, they can be stated for all kinds of classes, and cycles are allowed in the TBox. Notably, inclusion assertions can also be stated for basic links: indeed, T ~ (b1 ~ b2) forces b1 to a subset of b2 in every model of JC. Inclusion asser­ tions of this kind are used in the example to specify the properties of the attributes father, mother and children.
• N-ary relations are supported. Any instance of

Family can indeed be considered as a relation with four arguments. The x constructor is used to de­ fine keys for (N-ary) relations: for example, the fact that every instance of Family is an instance of x(Family, father, mother, date) implies that the three attributes form a key for the class. On the other hand, StillFamily, representing families whose father and mother are still married, has a more specialized key, constituted by the attributes father and mother. Observe that several keys can be defined for a class (see City) .

• Qualified number restrictions and role value maps on basic links can be used without any limitation. Indeed, (3= fatherUmotherU children) is a role value map on basic links.
• Complex links can be used for modeling interest­ ing relationships. For example, ~he relationship hasfather between a person and her/his father is captured in K by children- o father (sim­ ilarly for hasmother) . Also, ancestor is cap­ tured by (hasfather U hasmother) o (hasfather U hasmother)· (see the definition of VeryPhd).

As an example of inference that can be draw from K, observe that:

Indeed, note that every instance of 3children-. T is also an instance of 3father- Umother- U children-. T and therefore is an instance of Family. This means that K F= 3children-. T ~ 3children- .Family. Ob­ serve that K F= Family ~ (children ~3), and, since K F= Family ~ V 3 .Person (because K F= Family ~ u(Person)), we have that K F= 3children-. T ~ 3children- .(Vchildren.Person), which implies that K F= 3children-. T ~ Person. The fact that K F= 3children-. T ~ 3 3- .3father. T easily follows from the fact that every Family is a tuple with attribute father.

Relationship with other formalisms

It is easy to see that we obtain CIQ from CATS by simply ignoring tuples, sets, and basic links (other than atomic ones) . As another example of description logic supporting general inclusion assertions, the logic A£C.Nn, studied in [Buchheit et al., 1993], can be ob­ tained from CATS by ignoring tuples, sets, complex links, the (a1 ~ a2) constructs, and by allowing only basic links of the form b1 n b2 , and number restrictions of the form (:S k b. T) . Also the formalism in [Schmolze, 1989] supporting N-ary terms can be easily expressed in our logic. More generally, it can be shown the vast majority of decidable description logics proposed in the literature are captured by CATS.

Space limitation prevents us from showing how database models can be captured by CATS. We simply observe that we obtain the Entity-Relationship model by allowing one level of nesting in tuples, and by partition­ ing elementary classes in entities and attributes. Anal­ ogously, the nested relational model, as well as complex objects data models are expressed in CATS by imposing suitable limitations on tuples and sets.

As a final observation, we would like to note that CATS can also be used for expressing knowledge bases that go beyond classes and links. In [De Giacomo and Lenzerini, 1995], we show that a weak version of CATS can be used as a sort of monotonic propositional sit­ uation calculus extended with complex and concurrent actions. Roughly speaking, states are modeled by el­ ementary objects, and atomic actions are modeled by atomic links . A propositional fluent then simply becomes a class (whose instances are those states where the flu­ ent is true) , and preconditions, postconditions, effects of actions, as well as frame axioms are expressed by inclu­ sion assertions. Finally, basic links, complex links, and qualified number restrictions are used to model complex properties of actions, including concurrency. For exam­ ple, a1 n a2 denotes the concurrent execution of the ac­ tions a1 and a2), while an inclusion assertion of the form T ~ (:S 1 (U1 U · · · U Un)-. T) (where U1, ... , Un are all the atomic actions) can be used to impose that the past is backward linear -i.e., that every state as at most one predecessor.

5 Decision procedure for CAIS

We investigate the decidability and the complexity of CATS, showing that logical implication in CATS is polynomially reducible to logical implication in CI:F, which is decidable and EXPTIME-complete. The re­ duction is done in two steps: first, we "reify" basic links, tuples and sets, so that objects in the interpretations are elementary objects; then, we reduce qualified number re­ strictions to functional restrictions.

We define a mapping {/' form CATS basic links to CI Q concepts defined as ( T u, T 3 are new atomic con­ cepts) :

a mapping 8' form CATS links to CIQ roles defined as (V1, V2 are new atomic roles):

and a mapping 8 form CATS classes to CI Q concepts de­ fined as (T r(U1 , ·.· ,Un), T x(C,U1 , ··. ,Un), T u are new atomic concepts) :

o(A) =A o(r(Ul, . . . ,Un)) = Tr(U 1 , . . . ,Un) o(u(C)) =Tun V(V1- o id(T 3 ) o V2).8(C) o(x(C, ul, . .. ' Un)) = T x(C,Ul, ... ,Un) o(C1 n C2) = o(Cl) n o(C2) 8(--.C) = --.o(C) o(VL.C) = Vo'(L).o(C) o((:S k b.C)) = (:S k v1- .(o"(b) n vv2.o(C))) o((:S k b- .c))= (:S k v2- .(o"(b) n vv1.o(C))) o((b1 ~ b2)) = vv1.(--.o"(bl) u o"(b2)) o((b1 ~ b2)) = vv2.(--.o"(bl) u o"(b2)).

Making use of fJ, we define the so called reified coun­ terpart of a CATS TBox, which is, in fact , a CIQ TBox. We use the following abbreviations: Pu = V 1 - o id(T u) o V2, memb ::::: V 1 - o id(T 3) o V2, (~ k Pu.C) ::::: (~ k V1- .(Tun 'v'V2.C)) and (~ k Pu .C) ::::: (~ k V 2 - .(Tun 'v'V1.C)).

Definition Let K- be a CATS TBox. We call its reifled counterpart the TBox p(K) defined as p(K) = Pl (K) U P2(K) U P3(K), where:

• r1(K) = {a(C1) ~ a(C2) 1 c1 ~ c2 E K};
• p2(K) is the set constituted by:
• Tr(U,, ... ,U,.) := 3Pu,.T n (~ 1Pu,.T) n ... n 3Pu,..T n (~ 1Pu,..T) for each Tr(U, , ... ,u,.), with n ~ 1, in Pl(K)
• Tx(C,U) ~ 3Pu.T n (~ 1Pu.T) n ('v'Pu.(~ 1Pu.fJ(C))) nfJ(C) for each Tx(c,u) in r1(K)
• T x(c,u, , ... ,U,.) ~ T r(U,, ... ,U,.) n fJ(C) for each T x(c,u, , ... ,u,.), with n ~ 2, in Pl(K)
• T 17 = 3memb.T
• T 17 n (~ 1 memb. T) ~ 'v'memb.(~ 1 memb- .(~ 1 memb.T));
• p3(K) is the set constituted by (T c, T c are new atomic concepts): T ~ T c U Tc, T c ~ 'v'V1 . .l. n 'v'V2 · .l.., Tc ~ 3Vl.Tcn(~ 1Vl.T)n3V2.Tcn(~ 1 V2. T), one T u ~ T c for each T u in Pl (K)Up2(K), T 3 ~ Tc, one A~ Tc for each A in Pl (K) U r2(K), one Tr(U,, ... ,U,.) ~ Tc for each A in Pl(K) Up2(K), and T 17 ~ Tc. 0

Observe that p(K) has size which is polynomially related to the size of K-± and is interpreted over usual interpre­ tations I = (.6. , .I), where .6,I is a set of individuals. However, to represent the intended meaning of the con­ structs x(C, U1, .. . , Un) and O'(C), p(K) must be inter­ preted over a special kind of interpretations.

Definition We call a model I of a p(K) an aggregate­ descriptive model, if for all distinct individuals d, d' the following conditions hold:

Theorem 1 Let K- be a CATS TBox, and p(K-) its rei­ fled counterpart. Then there is a mapping from the mod­ e~s of K- to the aggregate-descriptive models of p(K-) and vzce versa.

A consequence of Theorem 1 is that K- F cl ~ C2 5 is equivalent to r(K) F r( { cl ~ C2} ). However, this does not directly yields a reasoning procedure for CATS, since it is not known how to reason with a p(K) inter­ preted over aggregate-descriptive models.

Theorem 2 below is the first substantial step towards devising such a reasoning procedure. It guarantees that on one hand we can interpret p(K) on aggregate­ descriptive models only, and on the other hand, we can forget about aggregate-descriptive models when comput­ ing logical consequence in p(K) . The proof of Theorem 2 is based on the disjoint union model property: let K- be a CIQ TBox and I = (~I, .I) and .J = (.6..7, . .7) be two models of K-, then also the interpretation I l:!:J .1 = (.6.Il:!:J.6..7 , .Il:!:J · .7) made up by the disjoint union of I and .1, is a model of K. We remark that most description logics have such a property, which is, in fact, typical of Modal Logics.

Theorem 2 Let K- be a CATS TBox and p(K-) its rei­ fled counterpart. If p(K-) has a model, then it has an aggregate-descriptive model.

The reified counterpart p(K) of a CATS TBox K- is not yet a CI:F TBox, because it contains qualified number restrictions. In order to deal with them, we represent the role Vi- (i = 1, 2), which is not functional (while v; is so) , by the role Fv, o F'~,, where Fv,, F' v, are new functional roles. The main point of such transformation is that now qualified number restrictions can be encoded as constraints on the chain Fv;oF'~,. Formally, we define the CI:F counterpart of a CATS TBox as follows .

Definition Let K- be a CATS TBox and p(K) its reified counterpart. We define the CI:F counterpart v(K-) of K, as v(K-) = v1(K-) /1. v2(K-), where:

• v1 (K-) is obtained from p(K) by recursively replac­ ing:
• every occurrence of V; with (Fv, o F'~J-, where Fv;, F'v, are new atomic roles,
• -every(~ 1 V;.T) with T,
• every (~ k Vi- .C) with 'v'(Fv, oF'~; o (id(C) o F'tJk .·C, where r+ stands for r; r* and rk stands for r o ... or (k times);
• v2 (K-) is the set constructed by one T ~ (~ 1 Fv.) n (~ 1 F'v;) n (~ 1 FV,) n (~ 1 F''VJ n ·(3FV,.T n 3F'v,. T) for each Fv, oF'~; in vl(K) . o

Note that , the inclusion assertions in v2 (K-) constrain the roles Fv;,F'v,,FV,,F'v; to be functional, and im­ pose that each individual cannot be linked to other indi­ viduals through both FV, and F'v;, thus implying that (Fv, o F'~J- is functional. Observe also that the size of v(K-) is polynomially related to the size of K.

Theorem 3 Let K- be a CATS TBox, p(K-) its reifled counterpart, and v(K-) its CI:F counterpart. Then there is a mapping from the models of p(K) to the models of v(K), and vice versa.

5 Without loss of generality, we assume that in a logical implication JC F= o1 !;;;;; o2, the atomic concepts and links, as well as the r(U1, ... ,Un) and x(O,U1, ... ,Un) occurring in 01 !;;;;; 02 ' also occur in /C.

Now we can establish the decidability and the com­ putational complexity of logical implication in CATS TBoxes. Indeed, by Theorem 3, K F cl ~ c2 is reducible to ~(K) F v({C1 ~ C2}). Since the size of v(K) U v({C1 ~ C2}) is polynomially related to K U {C1 ~ C2}, we get the following result.

Theorem 4 Logical implication m CATS zs EXPTIME-complete.

6 Conclusions

It is our opinion that the work described in this paper makes description logics accomplish the necessary leap in order to be well equipped for the new challenging appli­ cations they are faced with. Our first investigations show that CATS can indeed capture and extend most class­ based representation formalisms used in different areas as AI, databases, software engineering, etc.. One main issue still remains to be addressed, namely, the possibil­ ity of adding to CATS suitable constructs for express­ ing finiteness of nested aggregates, and, correspondingly, suitable techniques for reasoning in finite models (in the style of [Calvanese et al., 1994]). This will be the subject of further research.