Reasoning with Nominals

Nominals, i.e., atomic concepts referring to single individuals of the domain, are studied both in the area of DLs [BPS94,DLNS96] and modal logics [GG93,BS96,ABM99]. In this section we show how, in the presence of nominals, consistency for $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ can be polynomially reduced to consistency of TBoxes consisting of general inclusion axioms, which, in general, is an easier problem. This correspondence is used to obtain two novel results: (i) we show that, for unary coding, consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}$ -TBoxes consisting of cardinality restrictions can be decided in $\textsc{Exp\-Time}$ ; (ii) we show that, in the presence of both inverse roles and number restrictions, reasoning with nominals is strictly harder than without nominals: the complexity of determining consistency of TBoxes with general axioms rises from $\textsc{Exp\-Time}$ to $\textsc{NExp\-Time}$ , and the complexity of concept satisfiability rises from $\textsc{PSpace}$ to $\textsc{NExp\-Time}$ .

Definition 4.1 Let N_I be a set of individual names (also called nominals) disjoint from N_C and N_R. Concepts in $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ are defined as $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ -concepts with the additional rule that, for every $o \in N_I$ , o is an $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ -concept. A general concept inclusion axiom for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ is an expression of the from $C \sqsubseteq D$ , where C and D are $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ -concepts. A $\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}$ for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ is a finite set of general inclusion axioms for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ , where the subscript ``I'' stands for ``Inclusion''. The semantics of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ concepts is defined similar as for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ , with the additional requirement that every interpretation maps a nominal $o \in N_I$ to a singleton set $o^\mathcal{I}\subseteq \Delta^\mathcal{I}$ ; o can be seen as a name for the element in $o^\mathcal{I}$ . Please note that we do not have a unique name assumption, i.e., we do not assume that $o_1 \neq o_2$ implies $o_1^\mathcal{I}\neq o_2^\mathcal{I}$ .

An interpretation $\mathcal{I}$ satisfies an axiom $C \sqsubseteq D$ iff $C^\mathcal{I} \subseteq D^\mathcal{I}$ . It satisfies a $\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}$ $\ensuremath{T_{\text{gci}}}\xspace$ iff it satisfies all axioms in $\ensuremath{T_{\text{gci}}}\xspace$ ; in this case $\mathcal{I}$ is called a model of $\ensuremath{T_{\text{gci}}}\xspace$ , and we will denote this fact by $\mathcal{I}\models \ensuremath{T_{\text{gci}}}\xspace$ . A $\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}$ that has a model is called consistent.

Cardinality restrictions, $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ , and their interpretation for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}$ are defined analogously to $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ .

With $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{O}}\xspace$ we denote the fragment of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}\!\mathcal{O}}\xspace$ that does not contain any inverse roles R^-1.

Proof. Consistency of $\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}$ (and hence of $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ ) is $\textsc{Exp\-Time}$ -hard already for (a syntactical variant of) $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}}$ [HM92]. Assuming unary coding of numbers, we can reduce the problems to satisfiability of $\ensuremath{C^2}$ , which yields the $\textsc{NExp\-Time}$ upper bound.