Extending $\mathcal {ALC}$ with the Power-Set Construct

Abstract

We continue our exploration of the relationships between Description Logics and Set Theory, which started with the definition of the description logic $\mathcal {ALC}^\varOmega$. We develop a set-theoretic translation of the description logic $\mathcal {ALC}^\varOmega$ in the set theory $\varOmega$, exploiting a technique originally proposed for translating normal modal and polymodal logics into $\varOmega$.

We first define a set-theoretic translation of $\mathcal {ALC}$ based on Schild’s correspondence with polymodal logics. Then we propose a translation of the fragment $\mathcal {LC}^{\varOmega }$ of $\mathcal {ALC}^\varOmega$ without roles and individual names. In this—simple—case the power-set concept is mapped, as expected, to the set-theoretic power-set, making clearer the real nature of the power-set concept in $\mathcal {ALC}^\varOmega$. Finally, we encode the whole language of $\mathcal {ALC}^\varOmega$ into its fragment without roles, showing that such a fragment is as expressive as $\mathcal {ALC}^\varOmega$. The encoding provides, as a by-product, a set-theoretic translation of $\mathcal {ALC}^\varOmega$ into the theory $\varOmega$, which can be used as basis for extending other, more expressive, DLs with the power-set construct.

1 Introduction

In this paper we continue our investigation of the relationships between Description Logics and Set Theory, starting from the description logic $\mathcal {ALC}^\varOmega$, introduced in [5], which extends the language of $\mathcal {ALC}$ with the power set concept and with membership axioms. In $\mathcal {ALC}^\varOmega$ concepts are interpreted as sets living in a model of a simple theory $\varOmega$, a very rudimentary axiomatic set theory (introduced in Sect. 2.2), consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. Hence, concepts are interpreted as sets of sets (which are not necessarily well-founded), and membership among concepts has the obvious semantic interpretation as a natural generalization of DL assertions C(a).

The idea of enhancing the language of description logics with statements of the form $C \in 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 [15], and, starting from [11], where two alternative semantics (the Contextual $\pi$-semantics and the Hilog $\nu$-semantics) are proposed for metamodeling, many approaches to metamodeling have been proposed in the literature including membership among concepts. Most of them [4, 8,9,10] are based on a Hilog semantics, while [12, 14] define extensions of OWL DL and of $\mathcal {SHIQ}$ (respectively), based on semantics interpreting concepts as well-founded sets. None of these proposals includes the power-set concept in the language.

Considering an example taken from [11, 17], using membership axioms, we can represent the fact that eagles are in the red list of endangered species, by the axiom $Eagle \in 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 \in NotModifiableList$. However, much more interestingly, we would also clearly want $NotModifiableList \in NotModifiableList$.

The power-set concept, $\texttt {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”, observe that it can be naturally represented by the concept inclusion axiom: $RedListSpecies \sqsubseteq$ $\texttt {Pow}(CannotHunt)$, meaning that all the instances in the $RedListSpecies$ (as the class $Eagle$) are collections of individuals of the class $CannotHunt$. Notice, however, that $\texttt {Pow}(CannotHunt)$ is not limited to include $RedListSpecies$ but can include a much larger universe of sets (e.g. anything belonging to $\texttt {Pow}( Humans )$).

In [5] we proved that $\mathcal {ALC}^{\varOmega }$ is decidable by defining, for any $\mathcal {ALC}^{\varOmega }$ knowledge base K, a polynomial translation $K^T$ into $\mathcal {ALCOI}$, exploiting a technique—originally proposed and studied in [3]—consisting in identifying the membership relation $\in$ with the accessibility relation of a normal modality. Such an identification naturally leads to a correspondence between the power-set operator and the modal necessity operator $\Box$. We showed that the translation has the finite model property and concept satisfiability in $\mathcal {ALC}^{\varOmega }$ is in ExpTime.

In this paper we exploit the correspondence between $\in$ and the accessibility relation of a normal modality in another direction, to provide a polynomial set-theoretic translation of $\mathcal {ALC}^\varOmega$ in the set theory $\varOmega$. Our aim is to understand the real nature of the power-set concept in $\mathcal {ALC}^\varOmega$, as well as showing that a description logic with just the power-set concept, but no roles and no individual names, is as expressive as $\mathcal {ALC}^\varOmega$.

We proceed step by step by first defining a set-theoretic translation of $\mathcal {ALC}$ based on Schild’s correspondence result [16] and on the set-theoretic translation for normal polymodal logics in [3]. Then, we consider the fragment of $\mathcal {ALC}^\varOmega$ containing union, intersection, (set-)difference, complement, and power-set (but neither roles nor named individuals) and we show that this fragment, that we call $\mathcal {LC}^\varOmega$, has an immediate set-theoretic translation into $\varOmega$, where the power-set concept is translated as the power-set in $\varOmega$. Finally, we provide an encoding of the whole $\mathcal {ALC}^\varOmega$ into $\mathcal {LC}^\varOmega$. This encoding shows that $\mathcal {LC}^\varOmega$ is as expressive as $\mathcal {ALC}^\varOmega$. The full path leads to a set-theoretic translation of both the universal restriction and power-set concept of $\mathcal {ALC}^\varOmega$ in the theory $\varOmega$ using the single relational symbol $\in$. We refer to [6] for the proofs of the results.

2 Preliminaries

2.1 The Description Logic $\mathcal {ALC}$

Let ${N_C}$ be a set of concept names, ${N_R}$ a set of role names and ${N_I}$ a set of individual names. The set $\mathcal{C}$ of $\mathcal {ALC}$ concepts can be inductively defined as follows:

• $A \in N_C$, $\top$ and $\bot$ are concepts in $\mathcal{C}$;

• if $C, D \in \mathcal{C}$ and $R \in N_R$, then $C \sqcap D, C \sqcup D, \lnot C, \forall R.C, \exists R.C$ are concepts in $\mathcal{C}$.

A knowledge base (KB) K is a pair $(\mathcal{T}, \mathcal{A})$, where $\mathcal{T}$ is a TBox and $\mathcal{A}$ is an ABox. The TBox $\mathcal{T}$ is a set of concept inclusions (or subsumptions) $C \sqsubseteq D$, where C, D are concepts in $\mathcal{C}$. The ABox $\mathcal{A}$ is a set of assertions of the form C(a) and R(a, b) where C is a concept, $R \in N_R$, and $a, b \in N_I$.

An interpretation for $\mathcal {ALC}$ (see [2]) is a pair $I=\langle \varDelta , \cdot ^I \rangle$ where:

• $\varDelta$ is a domain—a set whose elements are denoted by $x, y, z, \dots$—and

• $\cdot ^I$ is an extension function that maps each concept name $C\in N_C$ to a set $C^I \subseteq \varDelta$, each role name $R \in N_R$ to a binary relation $R^I \subseteq \varDelta \times \varDelta$, and each individual name $a\in N_I$ to an element $a^I \in \varDelta$.

The function $\cdot ^I$ is extended to complex concepts as follows: $\top ^I=\varDelta$, $\bot ^I=\emptyset$, $(\lnot C)^I=\varDelta \backslash C^I$, $(C \sqcap D)^I =C^I \cap D^I$, $(C \sqcup D)^I=C^I \cup D^I$, and

• $(\forall R.C)^I =\{x \in \varDelta \mid \forall y. (x,y) \in R^I \rightarrow y \in C^I\}$,

• $(\exists R.C)^I =\{x \in \varDelta \mid \exists y.(x,y) \in R^I \ \& \ y \in C^I\}$.

The notion of satisfiability of a KB in an interpretation is defined as follows:

Definition 1

(Satisfiability and entailment). Given an $\mathcal {ALC}$ interpretation $I=\langle \varDelta , \cdot ^I \rangle$:

• I satisfies an inclusion $C \sqsubseteq D$ if $C^I \subseteq D^I$;

• I satisfies an assertion C(a) if $a^I \in C^I$ and an assertion R(a, b) if $(a^I,b^I) \in R^I$.

Given a KB $K=(\mathcal{T}, \mathcal{A})$, an interpretation I satisfies $\mathcal{T}$ (resp. $\mathcal{A}$) if I satisfies all inclusions in $\mathcal{T}$ (resp. all assertions in $\mathcal{A}$); I is a model of K if I satisfies $\mathcal{T}$ and $\mathcal{A}$.

Letting a query F be either an inclusion $C \sqsubseteq D$ (where C and D are concepts) or an assertion C(a), F is entailed by K, written $K\,\models \,F$, if for all models $I=\langle \varDelta , \cdot ^I\rangle$ of K, I satisfies F.

Given a KB K, the subsumption problem is the problem of deciding whether an inclusion $C \sqsubseteq 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, that is, whether there exists a model I of K, such that $C^I \ne \emptyset$.

2.2 The Theory $\varOmega$

The first-order theory $\varOmega$ consists of the following four axioms in the language with relational symbols $\in$ and $\subseteq$, and functional symbols $\cup$, $\backslash$, $Pow$:

$$\begin{aligned} x \in y \cup z&\leftrightarrow x \in y \vee x \in z; \\ x \in y \backslash z&\leftrightarrow x \in y \wedge x \not \in z; \\ x \subseteq y&\leftrightarrow \forall z (z \in x \rightarrow z \in y); \\ x \in Pow (y)&\leftrightarrow x \subseteq y. \end{aligned}$$

In an $\varOmega$-model everything is supposed to be a set. Hence, a set will have (only) sets as its elements and circular definition of sets are allowed (such as a set admitting itself as one of its elements). Moreover, not postulating in $\varOmega$ any link between membership $\in$ and equality—in axiomatic terms, having no extensionality (axiom)—$\varOmega$-models in which there are different sets with equal collection of elements, are admissible.

The most natural $\varOmega$-model—in which different sets are, in fact, always extensionally different—is the collection of well-founded sets $\mathsf {HF}=\mathsf {HF}^0=\bigcup _{n\in \mathbb {N}} \mathsf {HF}_n$, where: $\mathsf {HF}_0 =\emptyset$ and $\mathsf {HF}_{n+1} = Pow (\mathsf {HF}_n)$. A close relative of $\mathsf {HF}^0$, in which sets are not required to be well-founded, goes under the name of $\mathsf {HF}^{1/2}$ (see [1, 13]). $\mathsf {HF}^0$ or $\mathsf {HF}^{1/2}$ can be seen as the collection of finite (either acyclic or cyclic) graphs where sets are represented by nodes and arcs depict the membership relation among sets (see [13]).

A further enrichment of both $\mathsf {HF}^0$ and $\mathsf {HF}^{1/2}$ is obtained by adding atoms, that is copies of the empty-set, to be denoted by $\mathbf {a}_1, \mathbf {a}_2, \ldots$ and collectively represented by $\mathbb {A}= \{\mathbf {a}_1, \mathbf {a}_2, \ldots \}$. The resulting universes will be denoted by $\mathsf {HF}^0(\mathbb {A})$ and $\mathsf {HF}^{1/2}(\mathbb {A})$.

We will regard the domain $\varDelta$ of an $\mathcal {ALC}^\varOmega$ interpretation as a fragment of the universe of an $\varOmega$-model, i.e. as a set of sets of the theory $\varOmega$ rather than as a set of individuals, as customary in description logics.

2.3 The Description Logic $\mathcal {ALC}^\varOmega$

In [5] $\mathcal {ALC}$ has been extended by allowing concepts to be interpreted as sets in a universe of the set theory $\varOmega$, introducing the power-set as a new concept constructor, and admitting membership relations among concepts to occur in the knowledge base. The resulting extension of $\mathcal {ALC}$ has been called $\mathcal {ALC}^\varOmega$. We recap its definition.

Let $N_I$, $N_C$, and $N_R$ be as in Sect. 2.1. We extend the language of $\mathcal {ALC}$ by allowing, for all $\mathcal {ALC}^{\varOmega }$ concepts C, D:

• the difference concept $C\backslash D$ and

• the power-set concept $\texttt {Pow}(C)$.

While the concept $C\backslash D$ can be easily defined in $\mathcal {ALC}$ as $C \sqcap \lnot D$, this is not the case for the concept $\texttt {Pow}(C)$. Informally, the instances of concept $\texttt {Pow}(C)$ are all the subsets of the instances of concept C, which are “visible” in (i.e. which belong to) $\varDelta$.

Besides usual assertions of the forms C(a) and R(a, b) with $a,b \in N_I$, $\mathcal {ALC}^{\varOmega }$ allows in the ABox concept membership axioms and role membership axioms of the forms $C \in D$ and $(C,D) \in R$, respectively, where C and D are $\mathcal {ALC}^{\varOmega }$ concepts and R is a role name.

Considering again the example from the Introduction, the additional expressivity of the language allows for instance to represent the fact that polar bears are in the red list of endangered species, by the axiom $Polar \ \sqcap \ Bear \in RedListSpecies$. We can further represent the fact the polar bears are more endangered than eagles by the role membership axiom $( Polar \sqcap Bear, Eagle ) \in moreEndangered$.

We define a semantics for $\mathcal {ALC}^\varOmega$ extending the $\mathcal {ALC}$ semantics in Sect. 2.1 to capture the meaning of concepts (including concept $\texttt {Pow}(C)$) as elements (sets) of the domain ${\varDelta }$, chosen as a transitive set (i.e. a set x satisfying $(\forall y \in x) (y \subseteq x)$) in a model of $\varOmega$. Individual names are (essentially) interpreted as elements of a set of atoms $\mathbb {A}$, i.e. pairwise distinct copies of the empty-set from which the remaining sets in $\varDelta$ are built.

Definition 2

An interpretation for $\mathcal {ALC}^\varOmega$ is a pair $I=\langle \varDelta , \cdot ^I \rangle$ over a set of atoms $\mathbb {A}$ where: (i) the non-empty domain $\varDelta$ is a transitive set chosen in the universe $\mathcal{U}$ of a model $\mathcal {M}$ of $\varOmega$ over the atoms in $\mathbb {A}$;¹ (ii) the extension function $\cdot ^I$ maps each concept name $A\in N_C$ to an element $A^I \in \varDelta$; each role name $R \in N_R$ to a binary relation $R^I \subseteq \varDelta \times \varDelta$; and each individual name $a \in N_I$ to an element $a^I \in \mathbb {A} \subseteq \varDelta$. The function $\cdot ^I$ is extended to complex concepts of $\mathcal {ALC}^\varOmega$, as in Sect. 2.1 for $\mathcal {ALC}$, but for the two additional cases: $(\texttt {Pow}(C))^I = Pow (C^I) \cap \varDelta$ and $(C \backslash D)^I= (C^I \backslash D^I)$.

Observe that $\mathbb {A} \subseteq \varDelta \in \mathcal{U}$. As $\varDelta$ is not guaranteed to be closed under union, intersection, etc., the interpretation $C^I$ of a concept C is a set in $\mathcal U$ but not necessarily an element of $\varDelta$. However, given the interpretation of the power-set concept as the portion of the (set-theoretic) power-set visible in $\varDelta$, it easy to see by induction that, for each C, the extension of $C^I$ is a subset of $\varDelta$.

Given an interpretation I, the satisfiability of inclusions and assertions is defined as in $\mathcal {ALC}$ interpretations (Definition 1). Satisfiability of (concept and role) membership axioms in an interpretation I is defined as follows: I satisfies $C \in D$ if $C^I \in D^I$; I satisfies $(C,D) \in R$ if $(C^I, D^I) \in R^I$. With this addition, the notions of satisfiability of a KB and of entailment in $\mathcal {ALC}^\varOmega$ (denoted $\models _{\mathcal {ALC}^\varOmega }$) can be defined as in Sect. 2.1.

The problem of instance checking in $\mathcal {ALC}^\varOmega$ 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 \in D$ is a logical consequence of the KB (i.e., whether C is an instance of D).

A translation of the logic $\mathcal {ALC}^\varOmega$ into the description logic $\mathcal {ALCOI}$, including inverse roles and nominals, has been defined in [5], based on the correspondence between $\in$ and the accessibility relation of a modality explored in [3]. There, the membership relation $\in$ is used to represent a normal modality R. In [5], vice-versa, a new (reserved) role e in $N_R$ is introduced to represent the inverse of the membership relation, restricted to the sets in $\varDelta$: in any interpretation I, $(x,y) \in e^I$ will stand for $y \in x$. The idea underlying the translation is that each element u of the domain $\varDelta$ in an $\mathcal {ALCOI}$ interpretation $I=\langle \varDelta , \cdot ^I \rangle$ can be regarded as the set of all the elements v such that $(u,v) \in e^I$.

Soundness and completeness of this polynomial translation (see [5, 6]) provide, besides decidability, an ExpTime upper bound for satisfiability in $\mathcal {ALC}^\varOmega$. In [5] it was also proved that if the translation $K^T$ has a model in $\mathcal {ALCOI}$, then it has a finite model. From the soundness and completeness of the translation, it follows that $\mathcal {ALC}^\varOmega$ has the finite model property.

3 A Set Theoretic Translation of $\mathcal {ALC}^\varOmega$

We define a set-theoretic translation of $\mathcal {ALC}^\varOmega$ in the set theory $\varOmega$, exploiting the correspondence between $\in$ and the accessibility relation of a normal modality studied in [3]. In Sect. 3.1, we define a set-theoretic translation of $\mathcal {ALC}$, based on the translation introduced by D’Agostino et al. for normal, complete finitely axiomatizable polymodal logics [3]. Here, according to the well known correspondence between description logics and modal logics studied by Schild [16], concepts (sets of elements) play the role of propositions (sets of worlds) in the polymodal logic, while universal and existential restrictions $\forall R$ and $\exists R$ play the role of universal and existential modalities $\Box _i$ and $\Diamond _i$.

In Sect. 3.2 we focus on the fragment of $\mathcal {ALC}^\varOmega$ admitting no roles, no individual names and no existential and universal restrictions, that we call $\mathcal {LC}^\varOmega$. We show that $\mathcal {LC}^\varOmega$ can be given a simple set-theoretic translation in $\varOmega$. Finally, in Sect. 3.3, we see that this set-theoretic translation can be naturally extended to the full $\mathcal {ALC}^\varOmega$. In particular, we encode $\mathcal {ALC}^\varOmega$ into its fragment $\mathcal {LC}^\varOmega$, showing that $\mathcal {LC}^\varOmega$ is as expressive as $\mathcal {ALC}^\varOmega$ and providing a set-theoretic translation of $\mathcal {ALC}^\varOmega$ in which $\forall R_i.C$ and the power-set concept $\texttt {Pow}(C)$ are encoded in a uniform way.

3.1 A Set Theoretic Translation of $\mathcal {ALC}$ with Empty ABox

Let $R_1,\ldots ,R_k$ be the roles occurring in the knowledge base $K= (\mathcal{T}, \mathcal{A})$ and let $A_1, \ldots , A_n$ be the concept names occurring in K. Given a concept C of $\mathcal {ALC}$, built from the concept names and role names in K, its set-theoretic translation is a set-theoretic term $C^S(x,y_1,\ldots , y_k, x_1,\ldots , x_n)$, where $x,y_1,\ldots , y_k, x_1,\ldots , x_n$ are set-theoretic variables, inductively defined as follows:

$(\exists R_i.C)^S$ is translated to the set-theoretic term $(\lnot \forall R_i. \lnot C)^S$. Each $\mathcal {ALC}$ concept C is represented by a set-theoretic term $C^S$ and interpreted as a set in each model of $\varOmega$. Membership is used to give an interpretation of roles, as for modalities in the polymodal logics in [3].

For a single role R, by imitating the relation $R^I$ with $\in$ (where $v \in u$ corresponds to $(u,v) \in R^I$), we naturally obtain that $\texttt {Pow}(C)$ corresponds to the universal restriction $\forall R.C$. For multiple roles, in order to encode the different relations $R_1,\ldots ,R_k$, k sets $U_i$ are considered. Informally, each set $U_i$ (represented by the variable $y_i$) is such that $(v,v') \in R_i^I$ iff there is some $u_i \in U_i$ such that $u_i \in v$ and $v' \in u_i$.

Given an $\mathcal {ALC}$ knowledge base $K=(\mathcal{T}, \mathcal{A})$ with $\mathcal{A}= \emptyset$, we define the translation of the TBox axioms as follows:

$$\begin{aligned} { TBox _\mathcal{T}(x,y_1,\ldots ,y_k, x_1, \ldots , x_k)= \{ C_1^S \cap x \subseteq C_2^S \mid C_1 \sqsubseteq C_2 \in \mathcal{T} \}} \end{aligned}$$

We can then establish a correspondence between subsumption in $\mathcal {ALC}^\varOmega$ and derivability in the set theory $\varOmega$, instantiating the result of Theorem 5 in [3] as follows:

Proposition 1

For all concepts C and D on the language of the theory K:

where $Trans^2(x)$ stands for $\forall y \forall z (y \in z \wedge z \in x \rightarrow y \subseteq x)$, that is, $x \subseteq \texttt {Pow}(\texttt {Pow}(x))$.

The property $Trans^2(x)$ on the set x, which here represents the domain $\varDelta$ of an $\mathcal {ALC}^\varOmega$ interpretation (a transitive set), is needed, as in the polymodal case in [3], to guarantee that elements accessible through $R_i$ turn out to be in x. The set $Axiom_H(x,y_1,\ldots ,y_k)$, which in [3] contains the translation of the specific axioms of a polymodal logic, here is empty, as in $\mathcal {ALC}^\varOmega$ roles do not have any specific additional properties, and they correspond to the modalities of the normal polymodal logic $K_m$.

Roughly speaking, the meaning of Proposition 1 is that, for all the instances of x representing the domain $\varDelta$, for all the instances $U_1, \ldots , U_k$ of the set variables $y_1,\ldots ,y_k$, any choice for the interpretation $x_1, \ldots , x_n$ of the atomic concepts $A_1, \ldots , A_n$ in K which satisfies the TBox axioms over the elements in x (i.e., over the domain $\varDelta$), also satisfies the inclusion $C^S\subseteq D^S$ over $\varDelta$.

From the correspondence of the logic $\mathcal {ALC}$ with the normal polymodal logic $K_m$ in [16] and from the soundness and completeness of the set-theoretic translation for normal polymodal logics (Theorems 17 and 18 in [3]), we can conclude that, for $\mathcal {ALC}$, the set-theoretic translation above is sound and complete.

This set-theoretic translation can be naturally extended to more expressive description logics adding in $Axiom_H(x,\overline{y})$ the set-theoretic encoding of the semantic properties of the DL constructs. For instance, role hierarchy axioms, $R_j \sqsubseteq R_i$, with semantic condition $R_j^I \subseteq R_i^I$, can be simply captured by adding in $Axiom_H(x,y_1,\ldots ,y_k)$ the condition $y_j \subseteq y_i$. The inverse role $R_j$ of a role $R_i$ (i.e., $R_j= R_i^-$) can be captured by encoding the semantic condition $(v,y) \in R_j$ if and only if $(y,v) \in R_i$ by the axiom: $\forall y, v (y \in x \wedge v \in x \rightarrow ( \exists u (u\in y \wedge u \in y_j \wedge v \in u ) \leftrightarrow \exists u'( u'\in v \wedge u' \in y_i \wedge y \in u' )))$.

3.2 Translating the Fragment $\mathcal {LC}^\varOmega$

In this section we focus on the fragment $\mathcal {LC}^\varOmega$ of $\mathcal {ALC}^\varOmega$ without roles, individual names, universal and existential restrictions and role assertions, and we show that it can be given a simple set-theoretic translation in the set theory $\varOmega$. This translation provides some insight in the nature of the power-set construct in $\mathcal {ALC}^\varOmega$.

Let us consider a fragment of $\mathcal {ALC}^\varOmega$ which does neither allow existential and universal restrictions nor role assertions. We call $\mathcal {LC}^\varOmega$ such a fragment, whose concepts are defined inductively as follows:

• $A \in N_C$, $\top$ and $\bot$ are $\mathcal {LC}^{\varOmega }$ concepts;

• if C, D are $\mathcal {LC}^{\varOmega }$ concepts, then the following are $\mathcal {LC}^{\varOmega }$ concepts:

  $$\begin{aligned} C \sqcap D, C \sqcup D, \lnot C, C\backslash D, \texttt {Pow}(C) \end{aligned}$$

An $\mathcal {LC}^\varOmega$ knowledge base K is a pair $(\mathcal{T}, \mathcal{A})$, where the TBox $\mathcal{T}$ is a set of concept inclusions $C \sqsubseteq D$, and the ABox $\mathcal{A}$ is a set of membership axioms $C \in D$.

Given an $\mathcal {LC}^\varOmega$ knowledge base $K= (\mathcal{T}, \mathcal{A})$, let $A_1, \ldots , A_n$ be the concept names occurring in K. We define a translation of an $\mathcal {LC}^\varOmega$ concept C over the language of K to a set-theoretic term $C^S(x, x_1,\ldots , x_n)$, where $x, x_1,\ldots , x_n$ are set-theoretic variables, by induction on the structure of concepts, as follows:

Given a knowledge base $K=(\mathcal{T}, \mathcal{A})$, the translation for the TBox $\mathcal{T}$ and ABox $\mathcal{A}$ is defined as follows:

$$\begin{aligned} TBox _\mathcal{T}(x, x_1, \ldots , x_n) =&\{ C_1^S \cap x \subseteq C_2^S \mid C_1 \sqsubseteq C_2 \in \mathcal{T} \} \cup \{ A_i^S \in x \mid i=1, \ldots , n \} \\ ABox _\mathcal{A}(x,x_1, \ldots , x_n) =&\{C_1^S \in C_2^S \cap x \mid (C_1 \in C_2) \in \mathcal{A} \} \end{aligned}$$

We can now establish a correspondence between subsumption in $\mathcal {LC}^\varOmega$ and derivability in the set theory $\varOmega$.

Proposition 2

(Soundness and Completeness of the Translation of $\mathcal {LC}^\varOmega$). For all concepts C and D on the language of the knowledge base K:

$$\begin{aligned}&K\,\models _{\mathcal {LC}^\varOmega }\,C \sqsubseteq D \text { if and only if } \\&\varOmega \,\models \, \forall x ( Trans(x) \rightarrow \forall x_1, \ldots , \forall x_n ( \bigwedge ABox _\mathcal{A} \wedge \bigwedge TBox _\mathcal{T} \rightarrow C^S \cap x \subseteq D^S)) \end{aligned}$$

where Trans(x) stands for $\forall y (y \in x \rightarrow y \subseteq x)$, that is, $x \subseteq \texttt {Pow}(x)$, and $Axiom_H(x,$ $y_1,\ldots ,y_k)$ has been omitted as it is empty.

We refer to [6] for the proof. A similar correspondence result can be proved for instance checking, by replacing the inclusion $C^S \cap x \in D^S$ in Proposition 2 with $C^S \in D^S \cap x$.

As we can see from the translation above, the power-set construct in $\mathcal {LC}^\varOmega$ is defined precisely as the set-theoretic power-set. From the translation it is clear that only the part of the power-set which is in x (the domain $\varDelta$) is relevant when evaluating the axioms in K or a query, as all the axioms in the knowledge base are only required to be satisfied over the elements of the transitive set x. Notice that it is the same as in the set-theoretic translation of $\mathcal {ALC}$. Observe also that, in both $\mathcal {ALC}$ and $\mathcal {LC}^\varOmega$, $\top$ is interpreted as the transitive set x. It would not be correct to interpret $\top$ as the universe $\mathcal{U}$ of a model of $\varOmega$, as $\mathcal{U}$ might not be a set. Furthermore, $\texttt {Pow}(\top )$ is in the language of concepts and the interpretation of $\texttt {Pow}(\top )$ must be larger than the interpretation of $\top$.

3.3 Translating $\mathcal {ALC}^\varOmega$ by Encoding into $\mathcal {LC}^\varOmega$

It can be shown that $\mathcal {LC}^\varOmega$ has the same expressive power as $\mathcal {ALC}^\varOmega$, as universal and existential restrictions of the language $\mathcal {ALC}^\varOmega$ (as well as role assertions) can be encoded into $\mathcal {LC}^\varOmega$. The encoding, together with the set-theoretic translation of $\mathcal {LC}^\varOmega$ given in the previous section, determines a set-theoretic translation for $\mathcal {ALC}^\varOmega$, in which both the roles and the power-set construct are translated in a similar fashion, according to the polymodal translation in [3]. For space limitations, here we omit the treatment of role assertions and role membership axioms in the translation, and refer to [6].

Given an $\mathcal {ALC}^\varOmega$ knowledge base $K= (\mathcal{T}, \mathcal{A})$, let $R_1,\ldots ,R_k$ be the role names occurring in K, $A_1, \ldots , A_n$ the concept names occurring in K, and $a_1, \ldots , a_r$ the individual names occurring in K. We introduce k new concept names $U_1, \ldots , U_k$ in the language, one for each role $R_i$. These concepts (that are not in $N_C$) will be used to encode universal restrictions $\forall R_i. C$ as well as the power-set concept $\texttt {Pow}(C)$ of $\mathcal {ALC}^\varOmega$ into $\mathcal {LC}^\varOmega$. We further introduce a new concept name $B_i$ for each individual name $a_i$ occurring in K².

For an $\mathcal {ALC}^\varOmega$ concept C, the encoding $C^E$ in $\mathcal {LC}^\varOmega$ can be defined by recursively replacing: every named individual $a_i$ with the new concept name $B_i$, every subconcept $\forall R_i.C$ with $(\forall R_i.C)^E$ and every subconcept $\texttt {Pow}(C)$ with $(\texttt {Pow}(C))^E$, as defined below, while the encoding E commutes with concept constructors in all other cases:

• $a_i^E= B_i$

• $(\forall R_i.C)^E= \texttt {Pow}(\lnot U_i \sqcup \texttt {Pow}(C^E))$

• $(\texttt {Pow}(C))^E = \texttt {Pow}( U_1 \sqcup \ldots \sqcup U_k \sqcup C^E)$

For the encoding of the power-set, the idea is the same underlying the encoding of $\forall R_i.C$, as described in Sect. 3.1. For each $(\texttt {Pow}(C))^E$-element y, we require that all its elements $y' \in y$, which are not $U_1\,\sqcup \,\ldots \sqcup \,U_k$-elements, are $C^E$-elements. This is needed to keep the encoding of $\forall R_i.C$ and $\texttt {Pow}(C)$ (both based on the set-theoretic power-set) independent of each other.

Given an $\mathcal {ALC}^\varOmega$ knowledge base K, and a query F (over the language of K), the encoding $K^E$ of K, and the encoding $F^E$ of the query F in $\mathcal {LC}^\varOmega$ are defined as follows. $K^E$ contains: an inclusion axiom $C^E \sqcap \lnot (U_1 \sqcup \ldots \sqcup U_k) \sqsubseteq D^E$ for each $C \sqsubseteq D \in K$; a membership axiom $C^E \in D^E \sqcap \lnot (U_1 \sqcup \ldots \sqcup U_k)$ for each $C\in D$ in K; an axiom $a_i^E \in C^E \sqcap \lnot (U_1 \sqcup \ldots \sqcup U_k)$ for each $C(a_i)$ in K; an axioms $A_i \in \lnot (U_1 \sqcup \ldots \sqcup U_k)$, for all $A_i$ in K. Finally, axiom $\lnot (U_1 \sqcup \ldots \sqcup U_k) \sqsubseteq \texttt {Pow}(\texttt {Pow}(\lnot (U_1 \sqcup \ldots \sqcup U_k) ))$. The last one enforces the property $Trans^2( \varDelta \backslash (U_1 \sqcup \ldots \sqcup U_k)^I$.

For a query F, if F is an inclusion $C \sqsubseteq D$, its translation is $C^E \sqsubseteq D^E$; if F is an assertion $C(a_i)$, its translation is $a_i^E \in C^E$; if F is a membership axioms $C\in D$, its translation is $C^E \in D^E$. It can be proved that the encoding above is sound and complete, that is: $K\,\models _{\mathcal {ALC}^\varOmega }\,F \text { if and only if } K^E\,\models _{\mathcal {LC}^\varOmega }\,F^E$.

Combining this encoding with the set-theoretic translation for $\mathcal {LC}^\varOmega$ of Sect. 3.2, a set-theoretic translation for $\mathcal {ALC}^\varOmega$ can be obtained which extends the translation of $\mathcal {ALC}$ in Sect. 3.1 to the power-set concept. Given a concept C of $\mathcal {ALC}^\varOmega$ on the language of K, its set-theoretic translation $(C^E)^S$ is a set-theoretic term $C^*$:

The translation of an $\mathcal {ALC}^\varOmega$ knowledge base K can be defined accordingly, and a correspondence result follows from Propositions 2.

4 Conclusions and Related Work

The similarities between Description Logics and Set Theory have led to the definition of an extension of $\mathcal {ALC}$, called $\mathcal {ALC}^\varOmega$, with a power-set construct and membership relationships among arbitrary concepts [5]. It was shown that an $\mathcal {ALC}^\varOmega$ knowledge base can be polynomially translated into an $\mathcal {ALCOI}$ knowledge base, providing an ExpTime upper bound for satisfiability in $\mathcal {ALC}^\varOmega$. In this paper, we have developed a set-theoretic translation for the description logic $\mathcal {ALC}^\varOmega$ into the set theory $\varOmega$ exploiting a technique, originally proposed in [3], for translating normal modal and polymodal logics into $\varOmega$. The translation has been defined step by step, first translating $\mathcal {ALC}$ with empty ABox, then translating the fragment of $\mathcal {ALC}^\varOmega$ without roles and individual names and, finally, providing an encoding of $\mathcal {ALC}^\varOmega$ into this fragment. The translation of role assertions and role membership is omitted for space limitations and can be found in [6].

The set-theoretic translation allows, on the one hand, to shed some light on the nature of the power-set concept (which indeed corresponds to the set theoretic power-set) and, on the other hand, to show that the fragment of $\mathcal {ALC}^\varOmega$ without roles and individual names is as expressive as whole $\mathcal {ALC}^\varOmega$. The correspondence among fragments of set-theory and description logics opens to the possibility of transferring proof methods and decidability results across the two formalisms.

Up to our knowledge, the power-set construct has not been considered for DLs before. However, the issue of metamodelling, and the extension of DLs with membership among concept, have been widely studied in DLs [4, 7,8,9,10, 12], starting with the work by Motik [11], and we refer to [5] for comparisons.