Power (Set) ALC Laura Giordano1 and Alberto Policriti2 1 DISIT - Università del Piemonte Orientale - Alessandria, Italy - laura.giordano@uniupo.it 2 Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine Istituto di Genomica Applicata, Parco Scientifico e Tecnologico “L. Danieli”, Italy - alberto.policriti@uniud.it Abstract. We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Ω, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. The approach is then completed defining ALC Ω , an extension of ALC in which concepts are naturally interpreted as sets living in Ω-models. In ALC Ω not only membership between concepts is allowed—even admitting circularity—but also the power-set construct is exploited to add metamodeling capabilities. We conclude providing a polynomial translation of ALC Ω in ALCOI and proving its basic traits, among which the validity of the finite model property. 1 Introduction Concept and concept constructors in Description Logics (DLs) allow to manage infor- mation built-up and stored as collection of elements of a given domain. In this paper we would like to take the above statement seriously and put forward a DL doubly linked with a (very simple, axiomatic) set theory. Such a theory will be suitable to manipulate concepts (also called classes in OWL [20]) as first-class citizens, in the sense that it will allow the possibility to have concepts as instances (a.k.a. elements) of other concepts. Actually, the idea of enhancing the language of description logics with statements of the form C ∈ D, with C and D concepts is not new, as assertions of the form D(A), with A a concept name, are allowed in OWL-Full [20]. Here, while we do not consider roles, i.e. relations among individuals (also called properties in OWL), as possible instances of concepts, we would like to push the approach a little forward, allowing not only the possibility of stating that an arbitrary concept C can be thought as an instance of another one (C ∈ D), but also opening up our view along two further directions: 1. the possibility of having, as a special case, a concept as an instance of itself: C ∈ C 1 ; 2. the possibility of talking about all possible sub-concepts of a given concept, adding a power-set construct Pow(C). In order to realize our plan we introduce a DL, to be dubbed ALC Ω , whose two parents are ALC and a rudimentary (finitely axiomatized) set theory Ω. 1 Self membership is allowed for concept names in [16], by assertions of the form a(a) 2 Laura Giordano and Alberto Policriti For instance, considering an example taken from [22, 16], using membership axioms, we can represent the fact that eagles are in the red list of endangered species, by the axiom Eagle ∈ RedListSpecies and that Harry is an eagle, by the assertion Eagle(harry). We could further consider a concept notModifiableList, consisting of those lists that cannot be modified (if not by, say, a specifically enforced law) and, for example, it would be reasonable to ask RedListSpecies ∈ notModifiableList but, more interestingly, we would also clearly want notModifiableList ∈ notModifiableList. The power-set concept, Pow(C), allows to capture in a natural way the interactions between concepts and metaconcepts. Considering again the example above, the statement “all the instances of species in the Red List are not allowed to be hunted” can be represented by the concept inclusion axiom: RedListSpecies v Pow(CannotHunt), meaning that all the instances in the RedListSpecies (as the class Eagle) are included in CannotHunt. Motik has shown in [16] that the semantics of metamodeling adopted in OWL-Full leads to undecidability already for ALC-Full, due to the free mixing of logical and metalogical symbols. In [16], limiting this free mixing but allowing atomic names to be interpreted as concepts and to occur as instances of other concepts, two alternative semantics (the Contextual π-semantics and the Hilog ν-semantics) are proposed for metamodeling. Decidability of SHOIQ extended with metamodeling is proved under either of the two proposed semantics. Starting from [16], many other approaches to metamodeling have been proposed in the literature. Most of them [6, 11, 14, 9] are based on a Hilog semantics, while [19, 17] define extensions of OWL DL and of SHIQ (respectively), based on semantics interpreting concepts as well-founded sets. Here, we propose an extension of ALC with power-set concepts and membership axioms among concepts, whose semantics is naturally defined using sets living in Ω- models (not necessarily well-founded). We prove that ALC Ω is decidable by defining, for any ALC Ω knowledge base K, a polynomial translation K T into ALCOI, exploiting the correspondence studied in [5] between the membership relation in the set theory and a normal modality. We show that the translation K T enjoys the finite model property and exploit it in the proof of completeness of the translation. From the translation in ALCOI we also get an E XP T IME upper bound on the complexity of satisfiability in ALC Ω . Interestingly enough, our translation has strong relations with the first-order reductions in [8, 11, 14]. 2 Preliminaries 2.1 The description logics ALC and ALCOI Let NC be a set of concept names, NR a set of role names and NI a set of individual names. The set C of ALC concepts can be defined inductively as follows: - A ∈ NC , > and ⊥ are concepts in C; - if C, D ∈ C and R ∈ NR , then C u D, C t D, ¬C, ∀R.C, ∃R.C are concepts in C. A knowledge base (KB) K is a pair (T , A), where T is a TBox and A is an ABox. The TBox T is a set of concept inclusions (or subsumptions) C v D, where C, D are Power (Set) ALC 3 concepts in C. The ABox A is a set of assertions of the form C(a) and R(a, b) where C is a concept, R ∈ NR , and a, b ∈ NI . An interpretation for ALC [2] is a pair I = h∆, ·I i where ∆ is a domain (a set whose elements are denoted by x, y, z, . . . ) and ·I is an extension function that maps each concept name C ∈ NC to a set C I ⊆ ∆, each role name R ∈ NR to a binary relation RI ⊆ ∆ × ∆, and each individual name a ∈ NI to an element aI ∈ ∆. The function ·I is extended to complex concepts as follows: >I = ∆ ⊥I = ∅ (¬C)I = ∆\C I I I I (C u D) = C ∩ D (C t D)I = C I ∪ DI (∀R.C)I = {x ∈ ∆ | ∀y.(x, y) ∈ RI → y ∈ C I } (∃R.C)I = {x ∈ ∆ | ∃y.(x, y) ∈ RI & y ∈ C I } The notion of satisfiability of a KB in an interpretation is defined as follows: Definition 1 (Satisfiability and entailment). Given an ALC interpretation I = h∆, ·I i: - I satisfies an inclusion C v D if C I ⊆ DI ; - I satisfies an assertion C(a) if aI ∈ C I ; - I satisfies an assertion R(a, b) if (aI , bI ) ∈ RI . Given a KB K = (T , A), an interpretation I satisfies T (resp. A) if I satisfies all inclusions in T (resp. all assertions in A); I is a model of K if I satisfies T and A. Let a query F be either an inclusion C v D (where C and D are concepts) or an assertion C(a). F is entailed by K, written K |= F , if for all models I =h∆, ·I i of K, I satisfies F . Given a knowledge base K, the subsumption problem is the problem of deciding whether an inclusion C v D is entailed by K. The instance checking problem is the problem of deciding whether an assertion C(a) is entailed by K. The concept satisfiability problem is the problem of deciding, for a concept C, whether C is consistent with K (i.e., whether there exists a model I of K, such that C I 6= ∅). In the following we will also consider the description logic ALCOI allowing inverse roles and nominals. For a role R ∈ NR , its inverse is a role, denoted by R− , which can be used in existential and universal restrictions with the following semantics: (x, y) ∈ (R− )I if and only if (y, x) ∈ RI . For a named individual a ∈ NI , the nominal {a} is the concept such that: ({a})I = {aI }. 2.2 The theory Ω The first-order theory Ω consists of the following four axioms in the language with relational symbols ∈ and ⊆, and functional symbols ∪, \, Pow : x ∈ y ∪ z ↔ x ∈ y ∨ x ∈ z; x ∈ y\z ↔ x ∈ y ∧ x 6∈ z; x ⊆ y ↔ ∀z(z ∈ x → z ∈ y); x ∈ Pow (y) ↔ x ⊆ y. 4 Laura Giordano and Alberto Policriti In any Ω-model everything is supposed to be a set. Hence, a set will have (only) sets as its elements and circular definition of sets are not forbidden—i.e., for example, there are models of Ω in which there are sets admitting themselves as elements. Moreover, not postulating in Ω any link between membership ∈ and equality—in axiomatic terms, having no extensionality (axiom)—, there exist Ω-models in which there are different sets with equal collection of elements. The most natural Ω-model—in which different sets are, in fact, S always extensionally different—is the collection of well-founded sets HF = HF0 = n∈N HFn , where: HF0 = ∅; HFn+1 = Pow (HFn ). In HF0 every system of set-theoretic equations of the form:    x1 = {x1,1 , . . . , x1,m1 };  x2 = {x2,1 , . . . , x2,m2 };  . ..  ..   . xn = {xn,1 , . . . , xn,mn },  where xi,j for j = 1, . . . , mi is one among x1 , . . . xi−1 , finds a unique solution. If we drop the index-ordering restriction on variables appearing in the right-hand-side of set-theoretic equations (thereby allowing equations such as x = {x}), in order to guarantee the existence of solutions in the model we need to work with universes larger than HF. The most natural (and minimal) among them is a close relative of HF0 and goes under the name of HF1/2 (see [1, 18]). Finally, a further enrichment of both HF0 and HF1/2 is obtained by adding atoms, that is copies of the empty-set, to be denoted by a1 , a2 , . . . and collectively represented by A = {a1 , a2 , . . .}. The resulting universes will be denoted by HF0 (A) and HF1/2 (A). A complete discussion relative to universes of sets to be used as models of Ω goes beyond the scope of this paper. However, it is convenient to point out that, in all cases of interest for us here, an especially simple view of Ω-models can be given using finite graphs. Actually, HF0 or HF1/2 can be seen as the collection of finite graphs (either acyclic or cyclic, respectively), where sets are represented by nodes and arcs depict the membership relation among sets (see [18]). Given one such membership graph G it is convenient to single out a special node (the point of the graph), to isolate the specific set for which the description is introduced. In the next section, we will regard the domain ∆ of a DL interpretation as a fragment of the universe of an Ω-model, i.e. ∆ will be regarded as a set of sets of the theory Ω rather than as a set of individuals, as customary in description logics. 3 The description logic ALC Ω We start from the observation that in ALC concepts are interpreted as sets (namely, sets of domain elements) and we generalize ALC by allowing concepts to be interpreted as sets of the set theory Ω. In addition, we extend the language of ALC by introducing the power-set as a new concept constructor, and allowing membership relations among concepts in the knowledge base. We call ALC Ω the resulting extension of ALC. Power (Set) ALC 5 As before, let NI , NC , and NR be the set of individual names, concept names, and role names in the language, respectively. In building complex concepts, in addition to the constructs of ALC, we also consider the difference \ and the power-set Pow constructs. The set of ALC Ω concepts are defined inductively as follows: – A ∈ NC , > and ⊥ are ALC Ω concepts; – if C, D are ALC Ω concepts and R ∈ NR , then the following are ALC Ω concepts: C u D, C t D, ¬C, C\D, Pow(C), ∀R.C, ∃R.C While the concept C\D can be easily defined as C u ¬D in ALC, this is not the case for the concept Pow(C). Informally, the instances of concept Pow(C) are all the subsets of the instances of concept C visible in the domain ∆ (see below). Besides ABox assertions of the form C(a) with a ∈ NI , we allow in the ABox concept membership axioms and role membership axioms, respectively, of the form: C ∈ D and (C, D) ∈ R, where C and D are ALC Ω concepts and R is a role name. Considering again the example from the Introduction, the additional expressivity of the language, in which general concepts (and not only concept names) can be instances of other concepts, allows for instance to represent the fact that polar bears are in the red list of endangered species, by the axiom Polar u Bear ∈ RedListSpecies. We can further represent the fact the polar bears are more endangered than eagles by adding a role moreEndangered and the role membership axiom (Polar u Bear , Eagle) ∈ moreEn- dangered . Observe that, as shown in [16], the meaning of the sentence RedListSpecies v Pow(CannotHunt) (i.e. “all the instances of species in the Red List are not allowed to be hunted”), could be captured by combining the ν-semantics with the Semantic Web Rule Language (SWRL) [12], but not by the ν-semantics alone. We define a semantics for ALC Ω by extending the ALC semantics in Section 2.1 to capture the meaning of concepts (including concept Pow(C)) as elements (sets) of the domain ∆, chosen as a transitive set (i.e. a set x satisfying (∀y ∈ x)(y ⊆ x)) in a model of Ω. Roles are interpreted as binary relations over the domain ∆. Individual names are interpreted as elements of a set of atoms A from which the sets in ∆ are built. Definition 2. An interpretation for ALC Ω is a pair I = h∆, ·I i over a set of atoms A where: – the non-empty domain ∆ is a transitive set chosen in a model M of Ω over the atoms in A (we let U be the universe of the model M);2 – the extension function ·I maps each concept name A ∈ NC to an element AI ∈ ∆; each role name R ∈ NR to a binary relation RI ⊆ ∆ × ∆; and each individual name a ∈ NI to an element aI ∈ A ⊆ ∆. The function ·I is extended to complex concepts of ALC Ω , as in Section 2.1 for ALC, but for the two additional cases: (Pow(C))I = Pow (C I ) ∩ ∆ and (C\D)I = (C I \DI ). Observe that A ⊆ ∆ ∈ U. As ∆ is not guaranteed to be closed under union, intersection, etc., the interpretation C I of a concept C is a set in U but not necessarily an element 2 In the following, for readability, we will denote by ∈, Pow , ∪, \ (rather than Pow M , ∪M , \M ) the interpretation in a model M of the predicate and function symbols ∈, Pow , ∪, \. 6 Laura Giordano and Alberto Policriti of ∆. However, given the interpretation of the power-set concept as the portion of the (set-theoretic) power-set visible in ∆, it easy to see by induction that, for each C, the extension of C I is a subset of ∆. Given an interpretation I, the satisfiability of inclusions and assertions is defined as in ALC interpretations (Definition 1). Satisfiability of (concept and role) membership axioms in an interpretation I is defined as follows: I satisfies C ∈ D if C I ∈ DI ; I satisfies (C, D) ∈ R if (C I , DI ) ∈ RI . With this addition, the notions of satisfiability of a KB and of entailment in ALC Ω (denoted |=ALC Ω ) can be defined as in Section 2.1. The problem of instance checking in ALC Ω includes both the problem of verifying whether an assertion C(a) is a logical consequence of the KB and the problem of verifying whether a membership C ∈ D is a logical consequence of the KB (i.e., whether C is an instance of D). In the next section, we define a polynomial encoding of the language ALC Ω into the description logic ALCOI. 4 Translation of ALC Ω into ALCOI To provide a proof method for ALC Ω , we define a translation of ALC Ω into the descrip- tion logic ALCOI, including inverse roles and nominals. In [5] the membership relation ∈ is used to represent a normal modality R of a modal logic. In this section, vice-versa, we exploit the correspondence between ∈ and the accessibility relation of a modality by introducing a new (reserved) role e in NR to represent the inverse of the membership relation: in any interpretation I, (x, y) ∈ eI will stand for y ∈ x. The idea underlying the translation is that each element u of the domain ∆ in an ALCOI interpretation I = h∆, ·I i can be regarded as the set of all the elements v such that (u, v) ∈ eI . The translation of an ALC Ω knowledge base K = (T , A) into ALCOI can be defined as follows. First, we associate each concept C of ALC Ω to a concept C T of ALCOI by replacing all occurrences of the power-set constructor Pow with a concept involving the universal restriction ∀e (see below). More formally, we (inductively) define the translation C T of C by simply recursively replacing every subconcept Pow(D) appearing in C by ∀e.DT , while the translation T commutes with concept constructors in all other cases. Semantically this will result in interpreting any (sub)concept (Pow(D))I by (∀e.D)I = {x ∈ ∆ | ∀y((x, y) ∈ eI → y ∈ DI )}, which, recalling that (x, y) ∈ eI stands for y ∈ x, will characterize the collection of subsets of DI visible in ∆ (i.e. subsets of DI which are also elments of ∆): (∀e.D)I = {x ∈ ∆ | ∀y(y ∈ x → y ∈ DI )}, that is, (∀e.D)I = {x ∈ ∆ | x ⊆ DI )} = Pow(DI ) ∩ ∆ = (Pow(D))I , as expected. 4.1 Translating TBox, ABox, and queries We define a new TBox, T T , by introducing, for each inclusion C v D in T , the inclusion C T v DT in T T . Additionally, for each (complex) concept C occurring in the knowledge base K (or in the query) on the l.h.s. of a membership axiom C ∈ D Power (Set) ALC 7 or (C, D) ∈ R, we extend NI with a new individual name3 eC and we add the concept equivalence: C T ≡ ∃e− .{eC }. (1) in T T . From now on, new individual names such as eC will be called concept individual names. This equivalence is intended to capture the property that, in all the models I = h∆, ·I i of K T , eIC is in relation eI with all and only the instances of concept C T , i.e., for all y ∈ ∆, (eIC , y) ∈ eI if and only if y ∈ (C T )I . As in the case of the power-set constructor, this fact can be verified by analyzing the semantics of ∃e− .{eC }: (∃e− .{eC })I = {x ∈ ∆ | ∃y((x, y) ∈ (e− )I ∧ y ∈ ({eC })I }, which, recalling that e stands for 3 and interpreting the nominal, will stand for (∃e− .{eC })I = {x ∈ ∆ | ∃y(x ∈ y ∧ y ∈ {eIC }} = {x ∈ ∆ | x ∈ eIC }, which, by the concept equivalence C T ≡ ∃e− .{eC }, is as to say that eIC and (C T )I have the same extension. Remark 1. It is important to notice that every concept individual name of the sort eC introduced above—that is, every individual name whose purpose is that of providing a name to the extension of C I —, in general turns out to be in relation e with other elements of the domain ∆ of I (unless C is an inconsistent concept and its extension is empty). This is in contrast with the assumption relative to other “standard” individual names a ∈ NI , for which we will require (¬∃e.>)(a) (see below). We define AT as the set of assertions containing: – for each concept membership axiom C ∈ D in A, the assertion DT (eC ), – for each role membership axiom (C, D) ∈ R in A, the assertion R(eC , eD ), – for each assertion D(a) in A, the assertion DT (a), – for each assertion R(a, b) in A, the assertion R(a, b) and, finally, – for each (standard) individual name a ∈ NI , the assertion (¬∃e.>)(a). As noticed above, the last requirement forces all named individuals (in the language of the initial knowledge base K) to be interpreted as domain elements which are not in relation e with any other element. Let K T = (T T , AT ) be the knowledge base obtained by translating K into ALCOI. Example 1. Let K = (T , A) be the knowledge base considered above: T = {RedListSpecies v Pow(CannotHunt)} and A = {Eagle(harry), Eagle ∈ RedListSpecies, Polar u Bear ∈ RedListSpecies}. By the translation above, we obtain: T T = {RedListSpecies v ∀e.CannotHunt, Eagle ≡ ∃e − .{eEagle }, Polar u Bear ≡ ∃e − .{ePolar uBear } } AT = {Eagle(harry), RedListSpecies(eEagle ), RedListSpecies(ePolar uBear ), (¬∃e.>)(harry) } 3 The symbol eC should remind the e-xtension of C. 8 Laura Giordano and Alberto Policriti K T entails CannotHunt(harry) in ALCOI. In fact, from RedListSpecies(eEagle ) and RedListSpecies v ∀e.CannotHunt, it follows that, in all models of K T , eIEagle ∈ (∀e.CannotHunt)I . Furthermore, from Eagle ≡ ∃e − .{eEagle } and the assertion I Eagle(harry), it follows that (eEagle , harry I ) ∈ e I holds. Hence, harry I ∈ Cannot Hunt I . As this holds in all models of K T , CannotHunt(harry) is a logical consequence of K T . It is easy to see that Eagle v CannotHunt follows from K T as well. Let F be a query of the form C v D, C(a) or C ∈ D We assume that all the individual names, concept names and role names occurring in F also occur in K and we define a translation F T of the query F as follows: – if F is a subsumption C v D, then F T is the subsumption C T v DT ; – if F is an assertion C(a), then F T is the assertion C T (a); – if F is a membership axiom C ∈ D (respectively, (C , D) ∈ R), then F T is the assertion DT (eC ) (respectively, R(eC , eD )). In the following we state the soundness and completeness of the translation of an ALC Ω knowledge base into ALCOI. Proposition 1 (Soundness of the translation). The translation of an ALC Ω knowledge base K = (T , A) into ALCOI is sound, that is, for any query F : K T |=ALCOI F T ⇒ K |=ALC Ω F. For the sake of brevity a proof of the above proposition, which is given along standard lines, is not given here. Before proving the completeness of the translation of ALC Ω into ALCOI, we show that, if the translation K T of a knowledge base K in ALC Ω has a model in ALCOI, then it also has a finite model. Proposition 2. Let K be a knowledge base in ALC Ω and let K T be its translation in ALCOI. If K T has a model in ALCOI, then it has a finite model. Proof. We prove this result by providing an alternative (but equivalent) translation K T (¬) of K in the description logic ALC(¬), using a single negated role ¬e. ALC(¬) extends ALC with role complement operator, where, for any role R, the role ¬R is the negation of role R, where (x, y) ∈ (¬R)I if and only if (x, y) 6∈ RI . In the translation, we exploit ¬e to capture non-membership, where (x, y) ∈ (¬e)I if and only if (x, y) 6∈ eI (i.e., in set terms, y 6∈ x). Decidability of concept satisfiability in ALC(¬) has been proved by Lutz and Sattler in [15]. The finite model property of a language with a single negated role ¬e can be proved as done in [7] (Section 2) for a logic with the “window modality”, by standard filtration, extended to deal with additional K-modalities (for the other roles) as in the proof in [3]. Indeed, as observed in [15], the “window operator” studied in [7] is strongly related to a negated modality, as φ can be written as [¬R]¬φ. The translation K T (¬) can be defined modifying K T by replacing the concept equiv- alence C T ≡ ∃e− .{eC } with the assertions: (∀e.C T )(eC ) and (∀(¬e).(¬C T ))(eC ). One can show that any model I = (∆, ·I ) of K T (¬) is a model of K T in ALCOI, and vice-versa (considering the usual interpretation of negated roles, inverse roles and nominals). In fact, the semantic meaning of the assertion (∀e.C T )(eC ) is the following: Power (Set) ALC 9 for all x ∈ ∆, (eIC , x) ∈ eI ⇒ x ∈ (C T )I , which is equivalent to the meaning of ∃e− .{eC } v C T . The semantic meaning of the assertion (∀(¬e).(¬C T ))(eC ) is: for all x ∈ ∆, (eC , x) 6∈ eI ⇒ x 6∈ (C T )I , i.e., for all x ∈ ∆, x ∈ (C T )I ⇒ (eIC , x) ∈ eI , which is I the semantic meaning of C T v ∃e− .{eC }. We conclude the proof by observing that, if K T has a model, it is a model of K T (¬) . Then, by the finite model property, K T (¬) must have a finite model which is, in turn, a finite model of K T . 2 To conclude our analysis we now prove the completeness of our translation. Proposition 3 (Completeness of the translation). The translation of an ALC Ω knowl- edge base K = (T , A) into ALCOI is complete, that is, for any query F : K |=ALC Ω F ⇒ K T |=ALCOI F T . Proof (sketch). The proof is by contraposition. Assume that K T 6|=ALCOI F T . Then there is a model I = h∆, ·I i of K T in ALCOI such that I falsifies F . We show that we can build a model J = hΛ, ·J i of K in ALC Ω , where the domain Λ is a transitive set in the universe HF1/2 (A) consisting of all the hereditarily finite rational hypersets built from atoms in A = {a0 , a1 , . . .}. We define Λ starting from the graph4 G = h∆, eI i, whose nodes are the elements of ∆ and whose arcs are the pairs (x, y) ∈ eI . Notice that, by Proposition 2, the graph G can be assumed to be finite. Intuitively, an arc from x to y in G stands for the fact that y ∈ x. At this point, let ∆0 = {d1 , . . . , dm } be the elements of ∆ which, in the model I = h∆, ·I i, are not in relation eI with any other element in ∆ and are non equal to the interpretation of any concept individual name eC (that is, dj ∈ ∆0 iff there is no y such that (dj , y) ∈ eI and there is no concept C such that dj = eIC ). For any given d ∈ ∆ we define the following hyperset M (d):  a if d = dk ∈ ∆0 , M (d) = k (2) M (d0 ) | (d, d0 ) ∈ eI otherwise. Observe that, for the concepts C occurring on the l.h.s. of membership axioms, as axiom C T ≡ ∃e− .{eC } is satisfied in the model I of K T , it holds that d0 ∈ (C T )I iff (eIC , d0 ) ∈ eI . Therefore, for d = eIC , M (d) = M (eIC ) = M (d0 ) | (eIC , d0 ) ∈ eI = M (d0 ) | d0 ∈ (C T )I . The above definition uniquely determines hypersets in HF1/2 (A). This follows from the fact that all finite systems of (finite) set-theoretic equations have a solution in HF1/2 (A). As a matter of fact, whenever the graph G is acyclic, the definition of M (d) identifies a standard (recursively given) hereditarily finite set5 . 4 Strictly speaking the graph G introduced here is not really necessary: it is just mentioned to single out the membership relation ∈ from eI more clearly. 5 More generally, when eI is a well-founded relation, M (·) is a set-theoretic “rendering” of eI : the so-called Mostowski collapse of eI (see [13]). 10 Laura Giordano and Alberto Policriti Our task now is to complete the definition of J = hΛ, ·J i in such a way to prove that J is a model of K in ALC Ω falsifying F . The definition is completed as follows: – Λ = {M (d) | d ∈ ∆}; – for all B ∈ NC , B J = {M (d) | d ∈ B I }; – for all roles R ∈ NR such that R 6= e, RJ = {(M (d), M (d0 )) | (d, d0 ) ∈ RI }; – for all standard name individuals a ∈ NI such that aI = dk , let aJ = M (dk ) = ak ∈ A. To complete the proof it can be shown that, for all d ∈ ∆, M (d) ∈ C J if and only if d ∈ (C T )I , which is used to show that J is a model of K that falsifies F. 2 As the translation of ALC Ω into ALCOI is polynomial (actually, linear) in the size of the knowledge base (and of the query) the following complexity result follows. Proposition 4. Concept satisfiability in ALC Ω is an E XP T IME-complete problem. The hardness comes from the E XP T IME-hardness of ALC concept satisfiability w.r.t. a set of inclusions [21]; the upper bound from the E XP T IME upper bound for SHOI [10]. 5 Conclusions and related work In this paper we have shown that the similarities between description logics and set theory can be exploited to introduce in DLs the new power-set construct and to allow for (possibly circular) membership relationships among arbitrary concepts. We have defined the description logic ALC Ω , combining ALC with the set theory Ω, and defined its semantics whose interpretation domains are fragments of the domains of Ω-models. ALC Ω allows membership axioms among concepts as well as the power-set construct which, up to our knowledge, has not been considered for description logics before. We have shown that an ALC Ω knowledge base can be polynomially translated into an ALCOI knowledge base. Soundness and completeness of the translation provide, besides decidability, an E XP T IME upper bound for satisfiability in ALC Ω . The power-set construct allows to capture in a very natural way the interactions between concepts and metaconcepts, adding to the language of ALC the expressivity of metamodelling. The issue of metamodelling has been analysed by Motik in [16], proving that metamodelling in ALC-Full is already undecidable due to free mixing of logical and metalogical symbols. Two decidable semantics, a contextual π semantics and a Hilog ν-semantics, are introduced in [16] for a language extending SHOIQ with metamodelling, where concept names, role names and individual names are not disjoint. This possibility of using the same name in different contexts is introduced in OWL 1.1 and then in OWL 2 through punning6 . As a difference, in this paper, we consider concept names, role names and individual names to be disjoint, we allow concepts (and not only concept names) to be instances of other concepts, by membership axioms, while we do not allow role names as instances. As in [16], DeGiacomo et al. [6] and Homola et al. [11] employ an Hilog-style semantics to define Hi (SHIQ) and T H(SROIQ), respectively. While [16] and [6] 6 https://www.w3.org/2007/OWL/wiki/Punning Power (Set) ALC 11 define untyped higher-order languages which, as ALC Ω , allow a concept to be an instance of itself, [11] defines a typed higher-order extension of SROIQ allowing for a hierarchy of concepts, where concept names of order t can only occur as instances of concepts of order t + 1. In T H(SROIQ) [11] there is a strict separation between concepts and roles (as in ALC Ω ) and decidability is proved by a polynomial first-order reduction into SROIQ, which generalizes the reduction in [8] to an arbitrary number of orders. The translation in [11] introduces axioms A0 ≡ ∃instanceOf .{cA0 }, for each atomic concept A0 , axioms which are quite similar to our axiom (1), that we need for the concepts C occurring in the knowledge base on the left hand side of membership axioms. In Hi (SHIQ) [6], complex concept and role expressions can occur as instances of other concepts as in ALC Ω . A polynomial translation of Hi (SHIQ) into SHIQ is defined and a study of the complexity of higher-order query answering is provided. Kubincova et al. in [14] propose a Hylog-style semantics by dropping the ordering requirement in [11] and allowing the instanceOf role, with a fixed interpretation, to be used in axioms as any other role. The interpretation of role instanceOf does not correspond exactly to the interpretation of e− in our translation, as we do not introduce axiom (1) for all the concept names in NC , while we introduce it for all the (possibly complex) concepts occurring as instances in some membership axiom. Pan and Horrocks in [19] and Motz et al. in [17] define extensions of OWL DL and of SHIQ (respectively), based on semantics interpreting concepts as well-founded sets. In particular, [17] adds to SHIQ meta-modelling axioms equating individuals to concepts, without requiring that the instances of a concept need to stay in the same layer, and develop a tableau algorithm as an extension of the one for SHIQ. In [9] Gu introduces the language Hi(Horn-SROIQ), an extension of Horn-SROIQ which allows classes and roles to be used as individuals based on the ν-semantics [16]. ν-satisfiability and conjunctive query answering are shown to be reducible to the corresponding problems in Horn-SROIQ. A set-theoretic approach in DLs has been adopted by Cantone et al. in [4] for deter- mining the decidability of higher order conjunctive query answering in the description logic DL4,×D (where concept and role variables may occur in queries), as well as for developing a tableau based procedure for calculating the answer sets from a DL4,× D knowledge base, thus providing means for dealing with several well-known ABox reasoning tasks. We expect that the approach of extending ALC with Ω can be adopted as well for more expressive DLs, which do not enjoy the finite model property. However, when the finite model property does not hold, there may be models of the translated knowledge base K T containing domain elements being in the relation e with infinitely many elements, and corresponding to infinite sets. The completeness proof of Proposition 3 does not apply to this case and we leave the study of this case for future investigation. Other possible directions for future investigation concern: the treatment of roles as individuals, which has not been considered as an option in ALC Ω ; restricting the semantics to well-founded sets to avoid circular definitions of sets; translating ALC Ω into the set theory Ω, which may open to the possibility of exploiting proof methods developed for set theories in reasoning with DLs, as an alternative to translating to DLs. 12 Laura Giordano and Alberto Policriti Acknowledgement: This research is partially supported by INDAM-GNCS Project 2018 “Metodi di prova orientati al ragionamento automatico per logiche non-classiche”. References 1. P. Aczel. Non-Well-Founded Sets, volume 14. CSLI Lecture Notes, Stanford, CA, 1988. 2. F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi, and P.F. Patel-Schneider. The Descrip- tion Logic Handbook - Theory, Implementation, and Applications. Cambridge, 2007. 3. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. 4. D. Cantone, M. Nicolosi Asmundo, and D.F. Santamaria. A set-theoretic approach to abox reasoning services. In Rules and Reasoning - International Joint Conference, RuleML+RR 2017, London, UK, July 12-15, 2017, Proceedings, pages 87–102, 2017. 5. G. D’Agostino, A. Montanari, and A. Policriti. A set-theoretic translation method for poly- modal logics. J. Autom. Reasoning, 15(3):317–337, 1995. 6. G. De Giacomo, M. Lenzerini, and R. Rosati. Higher-order description logics for domain metamodeling. In Proc. AAAI 2011, San Francisco, California, USA, August 7-11, 2011. 7. G. Gargov, S. Passy, and T. Tinchev. Modal environment for Boolean speculations. In Mathematical Logic and Its Applications, pages 253–263. Plenum Press, 1987. 8. B. Glimm, S. Rudolph, and J. Völker. Integrated metamodeling and diagnosis in OWL 2. In ISWC 2010, Shanghai, China, November 7-11, 2010, pages 257–272, 2010. 9. Z. Gu. Meta-modeling extension of Horn-SROIQ and query answering. In Proceedings of the 29th Int. Workshop on Description Logics, Cape Town, South Africa, April 22-25, 2016. 10. J. Hladik. A tableau system for the description logic SHIO. In Contributions to the Doctoral Programme of IJCAR 2004, volume 106 of CEUR Workshop Proc., pages 21–25, 2004. 11. M. Homola, J. Kluka, V. Svátek, and M. Vacura. Typed higher-order variant of SROIQ - why not? In Proc. 27th Int. Workshop on Description Logics, Vienna, Austria, July 17-20, pages 567–578, 2014. 12. I. Horrocks and P.F. Patel-Schneider. A Proposal for an OWL Rule Language. In Proc.WWW 2004. ACM, 2004. 13. T. Jech. Set Theory. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, Third Millennium edition, 2003. 14. P. Kubincová, J. Kluka, and M. Homola. Towards expressive metamodelling with instantiation. In Proc. of the 28th Int. Workshop on Description Logics, Athens, June 7-10, 2015. 15. C. Lutz and U. Sattler. The complexity of reasoning with Boolean modal logics. In Proc. 3rd Int. Conf. on Advances in Modal Logic (AiML 2000), pages 329–348, 2002. 16. B. Motik. On the properties of metamodeling in OWL. In Proc. ISWC 2005, 4th International Semantic Web Conference, Galway, Ireland, November 6-10, 2005, pages 548–562, 2005. 17. R. Motz, E. Rohrer, and P. Severi. The description logic SHIQ with a flexible meta-modelling hierarchy. J. Web Sem., 35:214–234, 2015. 18. E.G. Omodeo, A. Policriti, and A.I. Tomescu. On Sets and Graphs. Perspectives on Logic and Combinatorics. Springer, DOI 10.1007/978-3-319-54981-1, 2017. 19. J.Z. Pan, I. Horrocks, and G Schreiber. OWL FA: A metamodeling extension of OWL DL. In Proc.OWLED 2005 Workshop, Galway, Ireland, November 11-12, 2005. 20. P.F. Patel-Schneider, P.H. Hayes, and I. Horrocks. OWL Web Ontology Language; Semantics and Abstract Syntax. In http: //www.w3.org/TR/owl-semantics/, 2002. 21. M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1):1–26, 1991. 22. C. Welty and D. Ferrucci. What’s in an instance? Technical Report 94-18, Max-Plank-Institut, 1994, RPI computer Science, 1994.