%%% $Id: main.tex,v 1.19 2000/05/03 07:14:38 tobies Exp $

\documentclass[twoside,11pt]{article}

\usepackage{jair,theapa}
\usepackage{amsmath,amsfonts,amssymb,theorem}
\usepackage{rotating}
%\usepackage{dl}
\usepackage{xspace}



%\input{makros}
%%% $Id: makros.tex,v 1.11 2000/02/16 14:59:11 tobies Exp $

\def\A{\forall}
\def\E{\exists}
\def\N{\mathbb{N}}
\def\Z{\mathbb{Z}}
\def\I{\mathcal{I}}
\def\J{\mathcal{J}}

\def\cA{\mathcal{A}}
\def\cB{\mathcal{B}}
\def\cC{\mathcal{C}}

\newcommand{\mybigsqcap}{{\raisebox{1.3ex}{\begin{turn}{180}$\displaystyle\bigsqcup$\end{turn}}}} 
\newcommand{\bigsqcap}{{\raisebox{1.3ex}{\begin{turn}{180}$\bigsqcup$\end{turn}}}} 

\newcommand{\nrleq}[3]{\ensuremath{(\leqslant #1 \; #2 \; #3)}}
\newcommand{\nrgeq}[3]{\ensuremath{(\geqslant #1 \; #2 \; #3)}}

\newcommand{\alc}{\ensuremath{\mathcal{A\!L\!C}}\xspace}
\newcommand{\alcqi}{\ensuremath{\mathcal{A\!L\!C\!Q\!I}}\xspace}
\newcommand{\alco}{\ensuremath{\mathcal{A\!L\!C\!O}}\xspace}
\newcommand{\alcqio}{\ensuremath{\mathcal{A\!L\!C\!Q\!I\!O}}\xspace}
\newcommand{\alcqo}{\ensuremath{\mathcal{A\!L\!C\!Q\!O}}\xspace}
\newcommand{\alcq}{\ensuremath{\mathcal{A\!L\!C\!Q}}\xspace}

\newcommand{\deltai}{\ensuremath{\Delta^\I}}

\newcommand{\ctwo}{\ensuremath{C^2}\xspace}
\newcommand{\nexptime}{\textsc{NExp\-Time}\xspace}
\newcommand{\exptime}{\textsc{Exp\-Time}\xspace}
\newcommand{\pspace}{\textsc{PSpace}\xspace}

\def\pos{\textit{pos}\xspace}
\def\xpos{\textit{xpos}}
\def\ypos{\textit{ypos}}
\def\succ{\textit{succ}}
\def\Tn{T_n}
\def\TnDw{T(n,\mathcal{D},w)}
\def\refl{{\textit{R}}}

\def\fraisse{Fra\"\i ss\'e\xspace}

\def\proof{\noindent\textbf{Proof. }}

\newcommand{\TcBox}{\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}\xspace}
\newcommand{\TcBoxes}{\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Boxes}}\xspace}
\newcommand{\TgBox}{\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Box}}\xspace}
\newcommand{\TgBoxes}{\ensuremath{\text{T\hspace{-1pt}}_I\hspace{-1pt}\text{Boxes}}\xspace}




%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 




{\theorembodyfont{\itshape} \newtheorem{definition}{Definition}[section]}
{\theorembodyfont{\rmfamily} \theoremstyle{break} \newtheorem{theorem}[definition]{Theorem}}
{\theorembodyfont{\rmfamily} \theoremstyle{break} \newtheorem{corollary}[definition]{Corollary}}
{\theorembodyfont{\rmfamily} \newtheorem{fact}[definition]{Fact}}
{\theorembodyfont{\rmfamily} \newtheorem{lemma}[definition]{Lemma}}

%\newenvironment{proof}{\noindent \textit{Proof.}}{\vspace{-3ex}}  

\newcommand{\qed}{{\unskip\nobreak\hfil\penalty50
   \hskip2em\hbox{}\nobreak\hfil
   \qedd
   \parfillskip=0pt \finalhyphendemerits=0
    \medskip\goodbreak\noindent}}

\newcommand{\qedd}{\vrule height4pt width 4pt depth0pt} 

\renewcommand{\cite}{\shortcite}

\begin{document}

\ShortHeadings{The Complexity of Cardinality Restrictions and
  Nominals}{Stephan Tobies}

\title{The Complexity of Reasoning with Cardinality Restrictions and
  Nominals in Expressive Description Logics}

\author{\name Stephan Tobies \email tobies@informatik.rwth-aachen.de\\
  \addr LuFG Theoretical Computer Science, RWTH Aachen\\
    Ahornstr. 55, 52074 Aachen, Germany }  

\jairheading{12}{2000}{}{12/1999}{5/2000}
\firstpageno{199}

\maketitle

\begin{abstract}
  We study the complexity of the combination of the Description Logics \alcq
  and \alcqi with a terminological formalism based on cardinality restrictions
  on concepts. These combinations can naturally be embedded into \ctwo, the
  two variable fragment of predicate logic with counting quantifiers, which
  yields decidability in \nexptime. We show that this approach leads to an
  optimal solution for \alcqi, as \alcqi with cardinality restrictions has the
  same complexity as \ctwo (\nexptime-complete). In contrast, we show that for
  \alcq, the problem can be solved in \exptime. This result is obtained by a
  reduction of reasoning with cardinality restrictions to reasoning with the
  (in general weaker) terminological formalism of general axioms for \alcq
  extended with nominals . Using the same reduction, we show that,
  for the extension of \alcqi with nominals, reasoning with general axioms is a
  \nexptime-complete problem. Finally, we sharpen this result and show that
  pure concept satisfiability for \alcqi with nominals is
  \nexptime-complete. Without nominals, this problem is known to be
  \pspace-complete.
\end{abstract}

%\input{intro} 
%%% $Id: intro.tex,v 1.15 2000/05/02 11:06:29 tobies Exp $

\section{Introduction}

Description Logics (DLs) can be used in knowledge based systems to represent
and reason about taxonomical knowledge of the application domain in a semantically
well-defined manner \cite{Woods92}. 
%These systems usually consist at least of
%the following three components: (i) a DL that is used to describe the
%concepts/classes of the problem domain; (ii) a terminological component that
%fixes the vocabulary of the domain; and (iii) a reasoning component that
%provides services like the calculation of implicit subsumption relations
%between concepts specified in the terminology or ensures consistency of the
%stored knowledge.
They allow the definition of complex concepts (i.e., classes, unary
predicates) and roles (binary predicates) to be built from atomic ones by the
application of a given set of constructors. For example, the following concept
describes those parents having at least two daughters:
\[
\texttt{Human} \sqcap (\texttt{Male} \sqcup \texttt{Female}) \sqcap \nrgeq 2 {\texttt{hasChild}}
{\texttt{Female}} \sqcap \forall \texttt{hasChild}.\texttt{Human}
\]
This concept is an example for the DL \alcq. \alcq extends the ``standard'' DL
\alc \cite{Schmidt-Schauss91} by qualifying number restrictions, i.e.,
concepts restricting the number of individuals that are related via a given
role (here \texttt{hasChild}), instead of allowing only for existential or
universal restrictions like \alc. \alcq is a
syntactic variant of the (multi-)modal logic $\mathsf{K}$ with \emph{graded
modalities}~\cite{Fine72}. In this paper we will study problems for the DLs
\alcq and \alcqi. The latter extends \alcq with the possibility to refer to
the inverse of role relations.  Additionally, in this paper we will encounter
\emph{nominals}, i.e., concepts referring to single elements of the domain.
The extensions of \alcq and \alcqi with nominals are denoted by \alcqo and
\alcqio. An example concept of \alcqio that describes the common children of the
individuals \texttt{ALICE} and \texttt{BOB} living with \texttt{ALICE} or
\texttt{BOB} is
\[
\exists {\texttt{hasChild}^{-1}}.{\texttt{ALICE}} \sqcap \exists
{\texttt{hasChild}^{-1}}.\texttt{BOB} 
\sqcap \exists {\texttt{livesWith}}.(\texttt{ALICE} \sqcup \texttt{BOB}) .
\]
Here, the parent relationship is expressed as the inverse of the \texttt{hasChild}
relationship.


A terminological component (TBox) allows for the organisation of defined
concepts and roles and forms the knowledge base of a DL system. TBoxes studied
in DLs range from weak ones allowing only for the acyclic introduction of
abbreviations for complex concepts, over TBoxes capable of expressing various
forms of general axioms, to cardinality restrictions that can express
restrictions on the number of elements the extension of a concept may have. In
the following, we give examples of these three types of assertions.

The following TBox introduces parent as an abbreviation for a human having at
least one child and whose children are all human, toddler for very young
human, and busy parent for a parent
having at least two children that are toddlers.
\begin{align*}
  \texttt{Parent} & = \texttt{Human} \sqcap (\geqslant  1 \;
  {\texttt{hasChild}}) \sqcap \forall \texttt{hasChild}.\texttt{Human}\\
  \texttt{Toddler} &= \texttt{Human} \sqcap \texttt{VeryYoung}\\
  \texttt{BusyParent} &= \texttt{Parent} \sqcap \nrgeq 2 {\texttt{hasChild}}
  {\texttt{Toddler}}
\end{align*}
The next expressions are \emph{general axioms} stating that males and females
are disjoint ($\bot$ denotes the empty concept) and that  males or
females coincide with those humans having exactly two human parents.
\begin{align*}
  \texttt{Female} \sqcap \texttt{Male} & = \bot\\
  \texttt{Female} \sqcup \texttt{Male} & = \texttt{Human} \sqcap (= 2 \ 
  \texttt{hasChild}^{-1} \ {\texttt{Human}})
\end{align*}
Finally, the following expression is a \emph{cardinality restriction}
expressing that there are at most two earliest ancestors:
\[
(\leq 2 \; (\texttt{Human} \sqcap \nrleq 0 {\texttt{hasChild}^{-1}}
{\texttt{Human}}))
\]
Cardinality restriction were first introduced by \shortciteA{Baader96a} as a
terminological formalism for the DL \alcq; as we will see, they can express
general axioms and hence are the most expressive of the terminological
formalisms considered in this paper. 

A key component of a DL system is a reasoning component that provides services
like subsumption or consistency tests for the knowledge stored in the TBox. A
subsumption test, for example, could infer from the previous definitions that
both \texttt{Male} and \texttt{Female} are subsumed by \texttt{Human} and that
\texttt{BusyParent} is subsumed by \texttt{Parent} as each busy parent must
have at least one child.  There exist sound and complete algorithms for
reasoning in a large number of DLs and different TBox formalisms that are
optimal with respect to the known worst-case complexity of these problems
\shortcite<see>[for an overview]{DoniniLenzerini+:1996}.

\begin{figure}
  \begin{center}
    \framebox[\textwidth]{
      \begin{tabular}{l|cc|cc}
                                %     \hline
        & \alcq & \alcqo & \alcqi & \alcqio\\
      \hline
      Concept Satisfiability & \pspace-c. & open & \pspace-c. & \textbf{NExpTime}-c.\\
      GCIs & \exptime-c. & \exptime-c. & \exptime-c. & \textbf{NExpTime}-c.\\
      Cardinality Restr. & \textbf{ExpTime}-c. & \textbf{ExpTime}-c. &
      \textbf{NExpTime}-c. & \textbf{NExpTime}-c.%\\
                                %\hline
    \end{tabular}
    }
  \end{center}
  \caption{Complexity results established in this paper (shown in bold face)}
    \label{fig:summary-complexity}
\end{figure}


In this paper we establish a number of new complexity results for DLs with
cardinality restrictions or nominals. Figure~\ref{fig:summary-complexity}
summarises the new complexity bounds established in this paper. All problems
are complete for their respective complexity class. This paper is organised as 
follows.

After giving some basic definitions in Section~\ref{sec:definitions}, we show
that consistency of TBoxes with cardinality restrictions for \alcqi is a
\nexptime-complete problem (Section~\ref{sec:completeness}). Membership in
\nexptime is shown by a translation
to the satisfiability problem of \ctwo~\cite{LICS::PacholskiST1997}%
                                %
\footnote{The \nexptime-result is valid only if we assume unary coding of
  numbers in the counting quantifiers. This is the standard assumption made by
  most results concerning the complexity of DLs.}%  
                                %
, the two variable fragment
of first order predicate logic augmented with counting quantifiers. The
matching lower bound is established by a reduction from a \nexptime-complete
bounded domino problem.

In Section~\ref{sec:nominals}, we show that reasoning with cardinality
restrictions can be reduced to reasoning with the (weaker) formalism of
general axioms in the presence of nominals. This yields interesting complexity
results both for reasoning with cardinality restrictions and with nominals.
Using a result from \cite{DeGiacomo95a}, the reduction shows that consistency
of TBoxes with cardinality restrictions for \alcq is in \exptime.  This
improves the result from \cite{Baader96a}, where it was shown that the problem
can be solved in \nexptime. Moreover, we show that for a DL with number
restrictions, inverse roles, and nominals reasoning problems become
\nexptime-hard, which solves an open problem from \cite{DeGiacomo95a}.  This
combination is of particular interest for the application of DLs in the area
of reasoning with database
schemata~\cite{Calvanese98c,calv-degi-lenz:PODS:98}.




%The \exptime upper bound for \alcq TBoxes with cardinality restrictions is
%obtained by showing that , i.e., atomic expressions referring to single
%elements of the universe of discourse.  

%\shortciteA{Baader96a} present a tableaux algorithm for consistency of
%\alcq-TBoxes with cardinality restrictions that runs in \nexptime.

%  In this
%paper we show, that this solution is not optimal w.r.t.\ worst case complexity 
%as the problem is \eptime-complete. Moreover, we show that In this
%paper we extend the knowledge about the complexity of cardinality restrictions
%in two directions: we show that the consistency of TBoxes with cardinality
%restrictions for \alcqi is a \nexptime-complete problem, whereas for \alcq it
%is shown to be \exptime-complete.








%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 

%\input{definitions} 
%%% $Id: definitions.tex,v 1.12 2000/05/02 11:06:28 tobies Exp $

\section{The Logic \alcqi}
\label{sec:definitions}

\begin{definition}\label{def:basic-definition}
  Let $N_C$ be a set of atomic \emph{concept names} and $N_R$ be a set of
  atomic \emph{role names}.  \emph{Concepts} in \alcqi are built inductively
  from these using the following rules: all $A \in N_C$ are concepts, and, if
  $C$, $C_1$, and $C_2$ are concepts, then also 
  \[
  \neg C, \ C_1 \sqcap C_2, \   \text{and} \ \nrgeq n S C ,
  \]
  are concepts, where $n \in \N$ and $S=R$ or $S= R^{-1}$ for some $R \in
  N_R$.
  
  A \emph{cardinality restriction} of \alcqi is an expression of the form $(\geqslant
  n \ C)$ or $(\leqslant n \ C)$ where $C$ is a concept and $n \in \N$; an \alcqi-\emph{\TcBox}%
  \footnote{The subscripted ``C'' indicates that the TBox consists of
    cardinality restrictions}
                                %
  is a finite set of cardinality restrictions. 
  
  The semantics of concepts is defined relative to an \emph{interpretation}
  $\mathcal{I} = (\Delta^\I,\cdot^\I)$, which consists of a domain \deltai\ 
  and a valuation $(\cdot^\mathcal{I})$ that maps each concept name $A$ to a
  subset $A^{\I}$ of \deltai\ and each role name $R$ to a subset $R^{\I}$ of
  $\deltai \times \deltai$.  This valuation is inductively extended to
  arbitrary concepts using the following rules, where $\sharp M$ denotes the
  cardinality of a set $M$:
  \begin{align*}
    (\neg C)^{\I} & := \deltai \setminus C^{\I},\\
    (C_1 \sqcap C_2)^{\I} & :=  C_1^{\I} \cap C_2^{\I},\\ 
    (\geqslant n \ R \ C)^{\I} & := \{ a \in \deltai \mid
    \sharp\{ b \in \deltai \mid (a,b) \in R^{\I} \wedge b \in C^{\I} \} \geq n
    \}, \\ 
    (\geqslant n \ R^{-1} \ C)^{\I} & := \{ a \in \deltai \mid \sharp\{ b \in
    \deltai \mid (b,a) \in R^{\I} \wedge b \in C^{\I} \} \geq n \}.
  \end{align*}
  
  An interpretation $\I$ \emph{satisfies} a cardinality restriction $(\geqslant n \ 
  C)$ iff $\sharp (C^{\I}) \geq n$, and it satisfies $(\leqslant n \ C)$ iff $\sharp
  (C^{\I}) \leq n$. It satisfies a \TcBox $T$ iff it satisfies all cardinality
  restrictions in $T$; in this case, $\I$ is called a \emph{model} of $T$ and we
  will denote this fact by $\I \models T$. A \TcBox that has a model is called
  \emph{consistent}.
  
  With \alcq we denote the fragment of \alcqi that does not contain any inverse
  roles $R^{-1}$.
\end{definition}

Using the constructors from Definition \ref{def:basic-definition}, we use
$(\forall \ C)$ as an abbreviation for the cardinality restriction $(\leqslant
0 \; \neg C)$ and introduce the following abbreviations for concepts:
\[
\begin{array}{r@{\;}c@{\;}l@{\qquad}r@{\;}c@{\;}l}
  C_1 \sqcup C_2 & = & \neg(\neg C_1 \sqcap \neg  C_2) & \nrleq n S C & = &
  \neg \nrgeq {(n+1)} S C \\
   C_1 \rightarrow C_2 & 
  = & \neg C_1 \sqcup C_2 & (=n \; S \; C) & = & \nrleq n S 
  C \sqcap \nrgeq n S C \\
  \exists S.C & = & \nrgeq 1 S C & \top & = & A \sqcup \neg A \quad \text{for some
    } A \in N_C\\
   \forall S.C & = & \nrleq 0 S {\neg C}
\end{array}
\]
%We define $$ as an abbreviation for $$, $C_1 \rightarrow C_2$ as an abbreviation for $\neg C_1 \sqcup C_2$,
%$\top$ for an arbitrary concept that is satisfied in all interpretations (e.g.
%$A \sqcup \neg A$), and $\nrleq n S C$ as an abbreviation for $\neg \nrgeq
%{(n+1)} S C$.  We also use $(=n \; S \; C)$ as an abbreviation for $\nrleq n S
%C \sqcap \nrgeq n S C$.  Finally, we use the abbreviations $\exists S.C$ for
%$\nrgeq 1 S C$ and $\forall S.C$ for $\nrleq 0 S {\neg C}$. For cardinality
%restrictions, we use $(\forall \ C)$ is an abbreviation for the cardinality
%restriction $(\leqslant 0 \ \neg C$).


TBoxes consisting of cardinality restrictions have first been studied in
\cite{Baader96a} for the DL \alcq.  Obviously, two concepts $C,D$ have the
same extension in an interpretation $\I$ iff $\I$ satisfies the cardinality
restriction $(\leqslant 0 \ (C \sqcap \neg D) \sqcup (\neg C \sqcap D))$.
Hence, cardinality restrictions can express terminological axioms of the form
$C = D$, which are satisfied by an interpretation $\I$ iff $C^\I = D^\I$.
General axioms are the most expressive TBox formalisms usually studied in the
DL context \cite{DeGiacomo96a}. One standard inference service for DL systems
is \emph{satisfiability} of a concept $C$ with respect to a \TcBox $T$, i.e.,
is there an interpretation $\I$ such that $\I \models T$ and $C^\I \neq
\emptyset$.  For a TBox formalism based on cardinality restrictions this is
easily reduced to TBox consistency, because obviously $C$ is satisfiable with
respect to $T$ iff $T \cup \{(\geqslant \ 1 \ C) \}$ is a consistent \TcBox.
For this the reason, we will restrict our attention to \TcBox consistency;
other standard inferences such as concept subsumption can be reduced to
consistency as well.

%There exists a tableaux based decision procedure for \alcq TBox
%consistency~\cite{Baader96a}. While for many other DLs tableaux algorithms can
%be adopted to work with inverse roles \cite{HoSat98c,HorrocksSattlerTobies98},
%this is an non-obvious task for \alcqi. 

\begin{figure}[t]
  \begin{center}
    \framebox[\textwidth]{
      $\begin{array}{l@{\;}c@{\;}l}
        \Psi_x(A) & := & Ax \hfill \text{for $A \in N_C$}\\
        \Psi_x(\neg C) & := & \neg \Psi_x(C)\\
        \Psi_x(C_1 \sqcap C_2) & := & \Psi_x(C_1) \wedge \Psi_x(C_2)\\
        \Psi_x \nrgeq n R C & := & \E^{\geq n} y.(Rxy \wedge \Psi_y(C))\\
        \Psi_x \nrgeq n {R^{-1}} C & := & \E^{\geq n} y.(Ryx \wedge
        \Psi_y(C))\\[1ex]
        \Psi_y(C) & := & \Psi_x(C)[x \backslash y, y \backslash x]\\[1ex]
        \Psi(\bowtie n \ C) & := & \E^{\bowtie n} x.\Psi_x(C) \hfill
        \text{for $\bowtie \;\in \{ \geqslant,\leqslant\}$}\\[1ex]
        \Psi(T) & := & \bigwedge \{ \Psi(\bowtie \ n \ C) \mid (\bowtie \
        n \ C) \in T \}
      \end{array}$
      }
  \end{center}
  \caption{The translation from \alcqi into \ctwo}
  \label{fig:translation}
\end{figure}


Until now there does not exist a direct decision procedure for \alcqi
\TcBox consistency.  Nevertheless this problem can be decided with the help of a
well-known translation of \alcqi-\TcBoxes to \ctwo \cite{Borgida96a}, given in
Figure~\ref{fig:translation}. The logic \ctwo is the fragment of predicate logic
in which formulae may contain at most two variables, but which is enriched with counting quantifiers of
the form $\exists^{\geq \ell}$.  The translation $\Psi$ yields a satisfiable
sentence of \ctwo if and only if the translated \TcBox is consistent.  Since the
translation from \alcqi to \ctwo can be performed in linear time, the
\nexptime upper bound \cite{LICS::GradelOR1997,LICS::PacholskiST1997} for
satisfiability of \ctwo directly carries over to \alcqi-\TcBox consistency:



\begin{lemma}\label{lem:alcqi-in-nexptime}
  Consistency of an \alcqi-\TcBox $T$ can be decided in \nexptime.
\end{lemma}


Please note that the \nexptime-completeness result
from~\cite{LICS::PacholskiST1997} is only valid if we assume unary coding of
numbers in the input; this implies that a number $n$ may not be stored in
logarithmic space in some $k$-ary representation but consumes $n$ units of
storage. This is the standard assumption made by most results concerning the
complexity of DLs. We will come back to this issue in Section~\ref{sec:reduction}.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 



%\input{completeness} 
%%% $Id: completeness.tex,v 1.17 2000/04/07 10:06:20 tobies Exp $

\section{Consistency of \alcqi-\TcBoxes is NExpTime-complete}
\label{sec:completeness}

To show that \nexptime is also the lower bound for the complexity of \TcBox
consistency, we use a bounded version of the domino problem.  Domino problems
\cite{Wang63,Ber66} have successfully been employed to establish undecidability
and complexity results for various description and modal logics
\cite{Spaan93,BaaderSattler-JLC-99}.

\subsection{Domino Systems}

\begin{definition}\label{def:domino-system}
  For $n \in \N$, let $\Z_n$ denote the set $\{0,\dots,n-1\}$ and $\oplus_n$
  denote the addition modulo $n$.  A \emph{domino system} is a triple
  $\mathcal{D} = (D,H,V)$, where $D$ is a finite set (of tiles) and $H,V
  \subseteq D \times D$ are relations expressing horizontal and vertical
  compatibility constraints between the tiles.  For $s,t \in \N$, let $U(s,t)$ be
  the torus $\mathbb{Z}_s \times \mathbb{Z}_t$, and let $w = w_0 \dots w_{n-1}$ be a
  word over $D$ of length $n$  (with $n \leq s$). We say that $\mathcal{D}$ \emph{tiles}
  $U(s,t)$ \emph{with initial condition} $w$ iff there exists a mapping $\tau:
  U(s,t) \rightarrow D$ such that, for all $(x,y) \in U(s,t)$,
  \begin{itemize}
  \item if $\tau(x,y) = d$ and $\tau(x
    \oplus_s 1,y) = d'$, then $(d,d') \in H$ (horizontal constraint);
  \item if $\tau(x,y) = d$ and $\tau(x, y \oplus_t 1) = d'$, then $(d,d')
    \in V$ (vertical constraint);
  \item $\tau(i,0) = w_i$ for $0\leq i < n$ (initial condition).
  \end{itemize}
\end{definition}

Bounded domino systems are capable of expressing the computational behaviour of
restricted, so-called \emph{simple}, Turing Machines (TM). This restriction is
non-essential in the following sense: Every language accepted in time $T(n)$ and
space $S(n)$ by some one-tape TM is accepted within the same time and space
bounds by a simple TM, as long as $S(n),T(n) \geq 2n$~\cite{BBG:clad}.

\begin{theorem}[\cite{BBG:clad}, Theorem 6.1.2]\label{theo:simple-turing-machine-domino}
  Let $M$ be a simple TM with input alphabet $\Sigma$.  Then there exists a
  domino system $\mathcal{D} = (D,H,V)$ and a linear time reduction which takes
  any input $x \in \Sigma^*$ to a word $w \in D^*$ with $|x| = |w|$ such that
  \begin{itemize}
  \item If $M$ accepts $x$ in time $t_0$ with space $s_0$, then $\mathcal{D}$
    tiles $U(s,t)$ with initial condition $w$ for all $s\geq s_0+2, t\geq t_0
    +2$;
  \item if $M$ does not accept $x$, then $\mathcal{D}$ does not tile $U(s,t)$
    with initial condition $w$ for any $s,t \geq 2$.
  \end{itemize}
\end{theorem}

%We use a corollary of this theorem  to prove the \nexptime-hardness result:


\begin{corollary}\label{cor:tiling-is-nexptime-hard}
  There is a domino system $\mathcal{D}$ such that the following is a
  \nexptime-hard problem:

  \begin{quote}
    Given an initial condition $w = w_0 \dots w_{n-1}$ of length $n$. Does
    $\mathcal{D}$ tile the torus $U(2^{n+1},2^{n+1})$ with initial
    condition $w$? 
  \end{quote}
\end{corollary}

\proof Let $M$ be a (w.l.o.g. simple) non-deterministic TM with time- (and
hence space-) bound $2^n$ deciding an arbitrary \nexptime-complete language
$\mathcal{L}(M)$ over the alphabet $\Sigma$. Let $\mathcal{D}$ be the
according domino system and $\textit{trans}$ the reduction from
Theorem~\ref{theo:simple-turing-machine-domino}.
  
  The function $\textit{trans}$ is a linear reduction from $\mathcal{L}(M)$ to
  the problem above: For $v \in \Sigma^*$ with $|v| = n$, it holds that $v \in
  \mathcal{L}(M)$ iff $M$ accepts $v$ in time and space $2^{|v|}$ iff
  $\mathcal{D}$ tiles $U(2^{n+1},2^{n+1})$ with initial condition
  $\textit{trans}(v)$. \qed



\subsection{Defining a Torus of Exponential Size}

Similar to proving undecidability by reduction of unbounded domino problems,
where defining infinite grids is the key problem, defining a torus of
exponential size is the key to obtaining a \nexptime-completeness proof by
reduction of bounded domino problems.

%When we consider the size of a \TcBox we have to fix a way in which numbers will
%be represented. This is of importance, because if we choose binary coding we
%would be able to use numbers of exponential size in the \TcBox, because $2^n$ only
%needs $n$ bits to be represented by a binary coding.

%We will choose unary coding for two reasons: We are able to define a torus of
%exponential size without numbers that big, so it does not do us any harm in
%this section. The second reason is, that if we assume unary coding, we will also
%be able to prove a similar upper bound for the complexity of satisfiability of
%\alcqi TBoxes. By this we are able to give an \emph{exact} characterization of
%the complexity of this problem. From now on in any space considerations we will
%assume numbers to be unary coded.

To be able to apply Corollary~\ref{cor:tiling-is-nexptime-hard} to \TcBox
consistency for \alcqi, we must characterise the torus $\mathbb{Z}_{2^n}
\times \mathbb{Z}_{2^n}$ with a \TcBox of polynomial size. To characterise
this torus, we use $2n$ concepts $X_0,\dots,X_{n-1}$ and $Y_0,\dots,Y_{n-1}$,
where $X_i$ (resp., $Y_i$) codes the $i$th bit of the binary representation of
the X-coordinate (resp., Y-coordinate) of an element $a$.

For an interpretation $\I$ and an element $a \in \Delta^\I$, we define $\pos(a)$
by
\begin{gather*}
  \pos(a) := (\xpos(a), \ypos(a)) := \biggl( \sum_{i = 0}^{n-1} x_i \cdot 2^i, \quad \sum_{i =
    0}^{n-1} y_i \cdot 2^i \biggr) \; , \; \text{where}\\
  \begin{array}{c@{\qquad}c}
    x_i = 
    \begin{cases}
      0, & \text{if $a \not\in X_i^\I$} \\
      1, & \text{otherwise}
    \end{cases} &
    y_i = 
    \begin{cases}
      0, & \text{if $a \not\in Y_i^\I$} \\
      1, & \text{otherwise} \ .
    \end{cases}
  \end{array} 
\end{gather*}

We use a well-known characterisation of binary addition
(e.g. \cite{BBG:clad}) to relate the positions of the elements in the
torus:
\begin{lemma}\label{lem:binary-addition}
  Let $x,x'$ be natural numbers with binary representations
  \[
  x = \sum_{i=0}^{n-1} x_i \cdot 2^i \quad \text{and} \quad x' =
  \sum_{i=0}^{n-1} x'_i \cdot 2^i .
  \]  
  Then
  \begin{multline*}
    \begin{split}
      x' \equiv x+1 \pmod{2^n} \quad \text{iff} \quad & \bigwedge_{k=0}^{n-1}
      (\bigwedge_{j=0}^{k-1} x_j = 1) \rightarrow (x_k = 1 \leftrightarrow x'_k = 0) \\
      \wedge & \bigwedge_{k=0}^{n-1} (\bigvee_{j=0}^{k-1} x_j = 0) \rightarrow
      (x_k = x'_k) \; ,
    \end{split}
  \end{multline*}
  where the empty conjunction and disjunction are interpreted as true
  and false, respectively.
\end{lemma}

\newcommand{\north}{{\textit{north}}\xspace}
\newcommand{\east}{{\textit{east}}\xspace}


\begin{figure}
  \begin{center}
    \framebox[\textwidth]{
      $
      \begin{array}{r@{\;}c@{\;}ll}
        T_n & = \bigl \{  & (\forall \ \exists {\east} . \top), & (\forall \
        \exists {\north} . \top), \\ 
        && (\forall \ (= 1 \; \east^{-1} \; \top)), &   (\forall \ (= 1 \;
        \north^{-1} \; \top)),\\
        && (\geqslant 1 \; C_{(0,0)}), &  (\geqslant 1 \; C_{(2^n-1,2^n-1)}),\\
        && (\leqslant 1 \; C_{(2^n-1,2^n-1)}), & (\forall \ D_\east \sqcap
        D_\north) \ \bigr \}\\[1ex]
        C_{(0,0)}  & = & \underset{k=0}{\overset{n-1}{\mybigsqcap}} \neg X_k \sqcap
        \underset{k=0}{\overset{n-1}{\mybigsqcap}} \neg Y_k\\[1ex]
        C_{(2^n-1,2^n-1)} & = & \underset{k=0}{\overset{n-1}{\mybigsqcap}} X_k \sqcap
        \underset{k=0}{\overset{n-1}{\mybigsqcap}} Y_k\\[1ex]
        D_\east & = & \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{\mybigsqcap}} (
          \underset{j=0}{\overset{k-1}{\mybigsqcap}} X_j) \rightarrow ((X_k \rightarrow
          \forall \east . \neg X_k) \sqcap (\neg X_k \rightarrow \forall
          \east.X_k)) \; \sqcap}\\
        && \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{\mybigsqcap}} (
          \underset{j=0}{\overset{k-1}{\displaystyle \bigsqcup}} \neg X_j) \rightarrow ((X_k
          \rightarrow \forall \east.X_k) \sqcap (\neg X_k \rightarrow \forall \east.
          \neg X_k)) \; \sqcap}\\
        && \multicolumn{2}{@{}l}{\underset{k=0}{\overset{n-1}{\mybigsqcap}}((Y_k \rightarrow \forall 
          \east . Y_k) \sqcap (\neg Y_k \rightarrow \forall \east.\neg Y_k))}\\
        D_\north & = & \dots
      \end{array}
      $
      }
  \end{center}
  \caption{A \TcBox defining a torus of exponential size}
  \label{fig:tbox-torus}
\end{figure}

The \TcBox $\Tn$ is defined in Figure~\ref{fig:tbox-torus}.  The concept
$C_{(0,0)}$ is satisfied by all elements $a$ of the domain for which $\pos(a)
= (0,0)$ holds. $C_{(2^n-1,2^n-1)}$ is a similar concept, whose instances $a$
satisfy $\pos(a) = (2^n-1, 2^n-1)$.

The concept $D_\north$ is similar to $D_\east$ where the role $\north$ has
been substituted for $\east$ and variables $X_i$ and $Y_i$ have been swapped.
The concept $D_\east$ (resp. $D_\north$) enforces that, along the role $\east$
(resp. $\north$), the value of $\xpos$ (resp. $\ypos$) increases by one while
the value of $\ypos$ (resp. $\xpos$) is unchanged. They are analogous to the
formula in Lemma~\ref{lem:binary-addition}.



The following lemma is a  consequence of the definition of $\pos$ and
Lemma~\ref{lem:binary-addition}.

\begin{lemma}\label{lem:addition-along-successors}
  Let $\I = (\Delta^\I, \cdot^\I)$ be an interpretation, $D_\east, D_\north$
  defined as in Figure~\ref{fig:tbox-torus}, and $a,b \in \Delta^\I$.
  
  \begin{gather*}
    \begin{array}{lll}
      \text{$(a,b) \in \east^\I$ and $a \in D_\east^\I$ implies:} \quad &
      \xpos(b) & \equiv \xpos(a)+1 \pmod{2^n} \\
      & \ypos(b) & = \ypos(a)
    \end{array}\\
    \begin{array}{lll}
      \text{$(a,b) \in \north^\I$ and $a \in D_\north^\I$ implies:} \quad &
      \xpos(b) & =  \xpos(a) \\
      & \ypos(b) & \equiv \ypos(a) +1 \pmod{2^n}
    \end{array}
  \end{gather*}
\end{lemma}

The \TcBox $\Tn$ defines a torus of exponential size in the following
sense:

\begin{lemma}\label{lem:tbox-defines-torus}
  Let $\Tn$ be the \TcBox as defined in Figure~\ref{fig:tbox-torus}. Let $\I =
  (\Delta^\I,\cdot^\I)$ be a model of $\Tn$. Then
  \[
  (\Delta^\I,\east^\I,\north^\I) \cong (U(2^n,2^n),S_1,S_2) \; ,
  \]
  where $U(2^n,2^n)$ is the torus $\Z_{2^n} \times \Z_{2^n}$ and $S_1,S_2$ are
  the horizontal and vertical successor relations on this torus.
\end{lemma}

\proof
  We show that the function \pos is an isomorphism from $\deltai$ to
  $U(2^n,2^n)$. Injectivity of $\pos$ is shown by induction on the
  ``Manhattan distance'' $d(a)$ of the $\pos$-value of an element $a$ to the
  $\pos$-value of the upper right corner.

  For an element $a \in \Delta^\I$ we define $d(a)$ by
  \[
  d(a) = (2^n-1 - \xpos(a)) + (2^n-1 - \ypos(a)) .
  \]
  Note that $\pos(a) = \pos(b)$ implies $d(a) = d(b)$. Since $\I \models
  (\leqslant 1 \; C_{(2^n-1,2^n-1)})$, there is at most one element $a \in
  \Delta^\I$ such that $d(a)=0$. Hence, there is exactly one element $a$ such
  that $\pos(a) = (2^n-1,2^n-1)$.  Now assume there are elements $a,b \in
  \Delta^\I$ such that $\pos(a)=\pos(b)$ and $d(a) = d(b) > 0$. Then either
  $\xpos(a) < 2^n-1$ or $\ypos(a) < 2^n-1$.  W.l.o.g., we assume $\xpos(a) <
  2^n-1$. From $\I \models T_n$, it follows that $a,b \in (\exists
  \east.\top)^\I$.  Let $a_1,b_1$ be elements such that $(a,a_1) \in \east^\I$
  and $(b,b_1) \in \east^\I$.  Since $d(a_1) = d(b_1) < d(a)$ and $\pos(a_1) = 
  \pos(b_1)$, the induction
  hypothesis yields $a_1 = b_1$. From
  Lemma~\ref{lem:addition-along-successors} it follows that
  \begin{align*}
    \xpos(a_1) & \equiv \xpos(b_1) \equiv \xpos(a) + 1 \pmod{2^n} \\
    \ypos(a_1) & = \ypos(b_1) = \ypos(a)
  \end{align*}
  This also implies $a=b$ because $a_1 \in (=1 \ \east^{-1}.\top)^\I$ and
  $\{(a,a_1), (b,a_1) \} \subseteq \east^\I$. Hence $\pos$ is injective.
  
  To prove that $\pos$ is also \emph{surjective} we use a similar technique.
  This time, we use an induction on the distance from the lower left corner.
  For each element $(x,y) \in U(2^n,2^n)$, we define:
  \[
  d'(x,y) = x+y .
  \]
  
  We show by induction that, for each $(x,y) \in U(2^n,2^n)$, there is an
  element $a \in \Delta^\I$ such that $\pos(a) = (x,y)$. If $d'(x,y) = 0$, then
  $x=y=0$. Since $\I \models (\geqslant 1 \; C_{(0,0)})$, there is an element $a \in
  \Delta^\I$ such that $\pos(a) = (0,0)$. Now consider $(x,y) \in U(2^n,2^n)$
  with $d'(x,y) >0$.  Without loss of generality we assume $x > 0$ (if $x = 0$
  then $y > 0$ must hold). Hence $(x-1,y) \in U(2^n,2^n)$ and $d'(x-1,y) <
  d'(x,y)$.  From the induction hypothesis, it follows that there is an element
  $a \in \Delta^\I$ such that $\pos(a) = (x-1,y)$. Then there must be an
  element $a_1$ such that $(a,a_1) \in \east^\I$ and 
  Lemma~\ref{lem:addition-along-successors} implies that $\pos(a_1) =
  (x,y)$.  Hence $\pos$ is also surjective.
  
  Finally, $\pos$ is indeed a homomorphism as an immediate consequence of
  Lemma~\ref{lem:addition-along-successors}.  \qed
  
  It is interesting to note that we need inverse roles only to guarantee that
  \pos is injective. The same can be achieved by adding the cardinality
  restriction $(\leqslant (2^n \cdot 2^n) \ \top)$ to $\Tn$, from which the
  injectivity of \pos follows from its surjectivity and simple cardinality
  considerations. Of course the size of this cardinality restriction would
  only be polynomial in $n$ if we assume binary coding of numbers. Also note
  that we have made explicit use of the special expressive power of
  cardinality restrictions by stating that, in any model of $\Tn$, the
  extension of $C_{(2^n-1,2^n-1)}$ must have \emph{at most} one element. This
  cannot be expressed with a \alcqi-TBox consisting of terminological axioms.

\subsection{Reducing Domino Problems to \TcBox Consistency}
\label{sec:reduction}

Once Lemma~\ref{lem:tbox-defines-torus} has been proved, it is easy to reduce
the bounded domino problem to \TcBox consistency. We use the standard reduction
that has been applied in the DL context, e.g., in~\cite{BaaderSattler-JLC-99}.

\begin{lemma}\label{lem:dominoe-reduces-to-alcqi-sat}
  Let $\mathcal{D} = (D,V,H)$ be a domino system. Let $w = w_0 \dots w_{n-1} \in
  D^*$. There is a \TcBox $\TnDw$ such that:
  \begin{itemize}
  \item $\TnDw$ is consistent iff $\mathcal{D}$ tiles $U(2^n,2^n)$ with initial
    condition $w$.
  \item $\TnDw$ can be computed in time polynomial in $n$.
  \end{itemize}
\end{lemma}

\proof We define $\TnDw := \Tn \cup T_\mathcal{D} \cup T_w $, where $\Tn$ is
defined in Figure~\ref{fig:tbox-torus}, $T_\mathcal{D}$ captures the vertical
and horizontal compatibility constraints of the domino system $\mathcal{D}$,
and $T_w$ enforces the initial condition. We use an atomic concept $C_d$ for
each tile $d \in D$.  $T_\mathcal{D}$ consists of the following cardinality
restrictions:
  \begin{gather*}
    (\forall \ \underset{d \in D}{\bigsqcup} C_d), \quad
    (\forall \ \underset{d \in D}{\mybigsqcap} \ \ \underset{d' \in
      D\setminus\{d\}}{\mybigsqcap} \neg (C_d \sqcap C_{d'})),\\
    (\forall \ \underset{d \in D}{\mybigsqcap} (C_d \rightarrow (\forall
    \east. \underset{(d,d') \in H}{\bigsqcup} C_{d'}))), \quad
    (\forall \ \underset{d \in D}{\mybigsqcap} (C_d \rightarrow (\forall \north.
    \underset{(d,d') \in V}{\bigsqcup} C_{d'}))).
  \end{gather*}
  $\mathcal{T}_w$ consists of the cardinality restrictions
  \[
  (\forall \ (C_{(0,0)}  \rightarrow C_{w_0})), \dots, 
  (\forall \ (C_{(n-1,0)} \rightarrow C_{w_{n-1}}) ,
  \]  
  where, for each $x,y$, $C_{(x,y)}$ is a concept that is satisfied by an
  element $a$ iff $\pos(a) = (x,y)$, defined similarly to $C_{(0,0)}$ and $C_{(2^n-1,2^n-1)}$.
  
  From the definition of $\TnDw$ and Lemma~\ref{lem:tbox-defines-torus}, it
  follows that each model of $\TnDw$ immediately induces a tiling of
  $U(2^n,2^n)$ and vice versa.  Also, for a fixed domino system $\mathcal{D}$,
  $\TnDw$ is obviously polynomially computable. \qed



%We have to prove that $\TnDw$ is satisfiable iff $\mathcal{D}$ tiles
%$U(2^n,2^n)$ with initial condition $w$.

%For the \emph{if}-direction let $\mathcal{D}$ tile $U(2^n,2^n)$ with initial
%condition $w$ and let $\tau$ be the according mapping. We define $\I$ as
%follows:
%\begin{align*}
%  \Delta^\I & = U(2^n,2^n)\\
%  \succ_i^\I & = S_i\\
%  X_i^\I & = \{ (x,y) \mid \text{the $i$th bit in $(x)_2$ is $1$} \}\\
%  Y_i^\I & = \{ (x,y) \mid \text{the $i$th bit in $(y)_2$ is $1$} \}\\
%  C_d^\I & = \{ (x,y) \mid \tau(x,y) = d \}
%\end{align*}
%where $(x)_2$ denotes the binary representation of $x$.

%It is easy to see that $\I \models \TnDw$ and hence $\TnDw$ is satisfiable.

%For the $only-if$-direction assume $\I \models \TnDw$. This implies that $\pos :
%\Delta^\I \rightarrow U(2^n,2^n)$ is an isomorphism which ``maps'' $\succ_i$ to
%$i$th successor relation of $U(2^n,2^n)$. We define the mapping $\tau$ as
%follows:
%\[
%\tau(x,y) = d \ \text{iff} \ \pos^{-1}(x,y) \in C_d^\I
%\]
%It is easy to see that $\tau$ is a well-defined function from $U(2^n,2^n)$ to
%$D$ which satisfies the initial condition as well as the local conditions.

%Finally we have to consider the size of $\TnDw$. The number of atomic concepts
%and roles in $\mathcal{T}_\mathcal{D}$ only does depend on the size of
%$\mathcal{D}$ which does not depend on the size $n$ of the input $w$ and hence
%plays no role in our considerations.. $|\TnDw| = |\mathcal{T}_n| +
%|\mathcal{T}_\mathcal{D}| + |\mathcal{T}_w|$. $|\mathcal{T}_n| =
%\mathcal{O}(n^2)$ by Lemma~\ref{lem:tn-size-is-polynomial}. The size of
%$\mathcal{T}_\mathcal{D}$ does not depend on $n$, hence
%$|\mathcal{T}_\mathcal{D}| = \mathcal{O}(1)$.  Finally $|\mathcal{T}_w| \leq n
%\times | \pos = (0,0) \rightarrow C_{w_0}| = \mathcal{O}(n^2)$. Obviously
%$\TnDw$ can also be computed in polynomial time.  \qed
  
  The main result of this section is now an immediate consequence of
  Lem\-ma~\ref{lem:alcqi-in-nexptime},
  Lem\-ma~\ref{lem:dominoe-reduces-to-alcqi-sat}, and
  Corollary~\ref{cor:tiling-is-nexptime-hard}:

\begin{theorem}\label{theo:alcqi-sat-is-nexptime-hard}
  Consistency of \alcqi-\TcBoxes is \nexptime-complete, even if unary coding
  of numbers is used in the input.
\end{theorem}

Recalling the note below the proof of Lemma~\ref{lem:tbox-defines-torus},
we see that the same argument also applies to $\alcq$ if we allow
binary coding of numbers.

\begin{corollary}\label{theo:alcq-sat-is-nexptime-hard}
  Consistency of $\alcq$-\TcBoxes is \nexptime-hard, if binary coding is used to
  represent numbers in cardinality restrictions.
\end{corollary}

It should be noted that it is open if the problem can be decided in \nexptime,
if binary coding of numbers is used, since the reduction of \ctwo only yields
decidability in 2-\nexptime.

In the following section, we will see that, for unary coding of numbers,
deciding consistency of \alcq-\TcBoxes can be done in \exptime
(Corollary~\ref{cor:alcq-exptime-complete}). This shows that the coding of
numbers indeed has an influence on the complexity of the reasoning
problem. It is worth noting that the complexity of pure concept satisfiability
for \alcq does not depend on the coding; the problem is \pspace-complete both
for binary and unary coding of numbers~\cite{Tobies-JLC-2000}.

For unary coding, we needed both inverse roles and cardinality restrictions for
the reduction. This is consistent with the fact that satisfiability for \alcqi
concepts with respect to TBoxes consisting of terminological axioms is still
in \exptime, which can be shown by a reduction to the \exptime-complete logics
$\mathcal{CIN}$~\cite{DeGiacomo95a} or \textsf{CPDL}~\cite{Pratt1979}. This shows
that cardinality restrictions on concepts are an additional source of
complexity. One reason for this might be that \alcqi with cardinality
restrictions no longer has the tree-model property.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 


%\input{nominals}
%%% $Id: nominals.tex,v 1.17 2000/05/02 11:06:30 tobies Exp $
\newcommand{\Tgci}{\ensuremath{T_{\text{gci}}}\xspace}
\newcommand{\create}{\textit{create}}

\section{Reasoning with Nominals}
\label{sec:nominals}

Nominals, i.e., atomic concepts referring to single individuals of the domain,
are studied both in the area of DLs
\cite{BOR:PAT:JAIR94,DoniniLenzerini+:1996} and modal logics
\cite{GargovGoranko1993,BlackSel-JLLI-95,ArecesBlackburnMarx-CSL-99}. In this
section we show how, in the presence of nominals, consistency for \TcBoxes 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 \alcq-TBoxes consisting of cardinality restrictions can be
decided in \exptime; (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 \exptime to \nexptime, and the complexity of concept
satisfiability rises from \pspace to \nexptime.

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

  An interpretation $\I$ \emph{satisfies} an axiom $C \sqsubseteq D$ iff $C^\I 
  \subseteq D^\I$. It satisfies a \TgBox $\Tgci$ iff it satisfies all axioms 
  in $\Tgci$; in this case $\I$ is called a \emph{model} of $\Tgci$, and we will
  denote this fact by $\I \models \Tgci$. A \TgBox that has a model is
  called \emph{consistent}.

  Cardinality restrictions, \TcBoxes, and their interpretation for
  \alcqio are defined analogously to \alcqi.

  With $\alcqo$ we denote the fragment of $\alcqio$ that does not contain any
  inverse roles $R^{-1}$.
\end{definition}

\begin{lemma}\label{lem:all-exptime-hard}
  Consistency of \TcBoxes or \TgBoxes both for \alcqo and \alcqio is
  \exptime-hard and can be decided in \nexptime, if unary coding of numbers is 
  used.
\end{lemma}

\proof Consistency of \TgBoxes (and hence of \TcBoxes) is \exptime-hard
already for (a syntactical variant of) \alc\cite{HalpernMoses92}. Assuming
unary coding of numbers, we can reduce the problems to satisfiability of
\ctwo, which yields the \nexptime upper bound. \qed



\subsection{Expressing Cardinality Restrictions Using Nominals}

In the following we show how, under the assumption of unary coding of numbers,
consistency of \alcqi-\TcBoxes can be polynomially reduced to consistency of
\alcqio-\TgBoxes. It should be noted that, conversely, it is also possible to
polynomially reduce consistency of \alcqio-\TgBoxes to consistency of
\alcqi-\TcBoxes: for an arbitrary concept $C$, the cardinality restrictions
$\{(\leqslant 1 \; C), (\geqslant 1 \; C) \}$ force the interpretation of $C$
to be a singleton. Since we do not gain any further insight from this
reduction, we do not formally prove this result.

\begin{definition}
  Let $T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$ be an
  \alcqi-\TcBox.  W.l.o.g., we assume that $T$ contains
  no cardinality restriction of the form $(\geqslant 0 \; C)$ as these are
  trivially satisfied by any interpretation. The translation of $T$, denoted
  by $\Phi(T)$, is the \alcqio-\TgBox defined as follows:
  \[
  \Phi(T) = \bigcup \{ \Phi(\bowtie_i n_i \; C_i) \mid 1 \leq i \leq k \} , 
  \]
  where $\Phi(\bowtie_i n_i \; C_i)$ is defined depending on whether
  $\bowtie_i = \leqslant$ or $\bowtie_i = \geqslant$. 
  \[
  \Phi(\bowtie_i n_i \; C_i) = 
  \begin{cases}
    \{ C_i \sqsubseteq o_i^1 \sqcup \dots \sqcup o_i^{n_i} \} & \text{if }
    \bowtie_i = \leqslant \\
    \{ o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j
    \sqsubseteq \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} & \text{if }
    \bowtie_i = \geqslant 
  \end{cases} ,
  \]
  where $o_i^1, \dots, o_i^{n_i}$ are fresh and distinct nominals and we use
  the convention that the empty disjunction is interpreted as $\neg \top$ to deal
  with the case $n_i = 0$.
\end{definition}

Assuming unary coding of numbers, the translation of a \TcBox $T$ is obviously
computable in polynomial time.

\begin{lemma}\label{lem:alcqi-to-alcqio}
  Let $T$ be an \alcqi-\TcBox. $T$ is consistent iff $\Phi(T)$ is consistent.
\end{lemma}

\proof
  Let $T = \{ (\bowtie_1 n_1 \; C_1), \dots (\bowtie_k n_k \; C_k) \}$ be a
  consistent \TcBox. Hence, there is a model $\I$ of $T$, and $\I \models
  (\bowtie_i n_i \; C_i)$ for each $1 \leq i \leq k$. We show how to
  construct a model $\I'$ of $\Phi(T)$ from $\I$. $\I'$ will be identical to
  $\I$ in every respect except for the interpretation of the nominals $o_i^j$ 
  (which do not appear in $T$).
  
  If $\bowtie_i = \leqslant$, then $\I \models T$ implies $\sharp C_i^\I \leq
  n_i$. If $n_i = 0$, then we have not introduced new nominals, and $\Phi(T)$
  contains $C_i \sqsubseteq \neg \top$. Otherwise, we define $(o_i^j)^{\I'}$ such
  that $C_i^\I \subseteq \{ (o_i^j)^{\I'} \mid 1 \leq j \leq n_i \}$. This
  implies $C_i^{\I'} \subseteq (o_i^1)^{\I'} \cup \dots \cup
  (o_i^{n_i})^{\I'}$ and hence, in either case, $\I' \models \Phi(\leqslant n_i
  \; C_i)$.
  
  If $\bowtie_i = \geqslant$, then $n_i > 0$ must hold, and $\I \models T$
  implies $\sharp C_i^\I \geq n_i$.  Let $x_1, \dots x_{n_i}$ be $n_i$
  distinct elements from $\Delta^\I$ with $\{ x_1, \dots, x_{n_i} \} \subseteq
  C_i^\I$.  We set $(o_i^j)^{\I'} = \{x_j \}$. Since we have chosen distinct
  individuals to interpret different nominals, we have $\I' \models o_i^j
  \sqsubseteq \neg o_i^\ell$ for every $1 \leq i < \ell \leq n_i$. Moreover, $x_j
  \in C_i^\I$ implies $\I' \models o_i^j \sqsubseteq C_i$ and hence $\I'
  \models \Phi(\geqslant n_i \; C_i)$.
  
  We have chosen distinct nominals for every cardinality restrictions, hence
  the previous construction is well-defined and, since $\I'$ satisfies
  $\Phi(\bowtie_i n_i \; C_i)$ for every $i$, $\I' \models \Phi(T)$.
  
  For the converse direction, let $\I$ be a models of $\Phi(T)$. The fact that
  $\I \models T$ (and hence the consistency of $T$) can be shown as follows:
  let $(\bowtie_i n_i \; C_i)$ be an arbitrary cardinality restriction in $T$.
  If $\bowtie_i = \leqslant$ and $n_i = 0$, then we have $\Phi(\leqslant 0 \;
  C_i) = \{ C_i \sqsubseteq \; \neg \top \}$ and, since $\I \models \Phi(T)$,
  we have $C_i^\I = \emptyset$ and hence $\I \models (\leqslant 0 \; C_i)$. If
  $\bowtie_i = \leqslant$ and $n_i > 0$, we have $\{ C_i \sqsubseteq o_i^1
  \sqcup \dots \sqcup o_i^{n_i} \} \subseteq \Phi(T)$. From $\I \models
  \Phi(T)$ follows $\sharp C_i^\I \leq \sharp (o_i^1 \sqcup \dots \sqcup
  o_i^{n_i})^\I \leq n_i$.  If $\bowtie_i = \geqslant$, then we have $ \{
  o_i^j \sqsubseteq C_i \mid 1 \leq j \leq n_i \} \cup \{ o_i^j \sqsubseteq
  \neg o_i^\ell \mid 1 \leq j < \ell \leq n_i \} \subseteq \Phi(T)$. From the
  first set of axioms we get $\{ (o_i^j)^\I \mid 1 \leq j \leq n_i \}
  \subseteq C_i^\I$.  From the second set of axioms we get that, for every $1
  \leq j < \ell \leq n_i$, $(o_i^j)^\I \neq (o_i^\ell)^\I$.  This implies that
  $n_i = \sharp \bigcup \{ (o_i^j)^\I \mid 1 \leq j \leq n_i \} \leq \sharp
  C_i^\I$. \qed


\begin{theorem}\label{theo:alcqi-to-alcqio}
  Assuming unary coding of numbers, consistency of \alcqi-\TcBoxes can be
  polynomially reduced to consistency of \alcqio-\TgBoxes. Similarly,
  consistency of \alcq-\TcBoxes can be polynomially reduced to consistency of
  \alcqo-\TgBoxes.
\end{theorem}

\proof
  The first proposition follows from the fact that $\Phi(T)$ is polynomially
  computable from $T$ if we assume unary coding of numbers and from
  Lemma~\ref{lem:alcqi-to-alcqio}. The second proposition follows from the
  fact that the translation does not introduce additional inverse roles. If
  $T$ does not contain inverse roles, then neither does $\Phi(T)$, and hence
  the result of translating an \alcq-\TcBox is an \alcqo-\TgBox. \qed



\subsection{Complexity Results}

We will now use Theorem~\ref{theo:alcqi-to-alcqio} to obtain new complexity
results both for DLs with cardinality restrictions and with nominals.  

\subsubsection{\alcq and \alcqo}

\shortciteA{DeGiacomo95a} obtains complexity results for various DLs by
sophisticated polynomial reduction to a propositional dynamic logic.  The
author establishes many complexity results, one of which is of special
interest for our purposes.

\begin{theorem}[\cite{DeGiacomo95a}, Section 7.3]
  Satisfiability and logical im\-pli\-ca\-tion for $\mathcal{C\!N\!O}$ knowledge
  bases (TBox and ABox) are \exptime-complete.
\end{theorem}

The DL $\mathcal{C\!N\!O}$ studied by the author is a strict extension of
\alcqo; TBoxes in his thesis correspond to what we call \TgBoxes in this
paper.  Unary coding of numbers is assumed throughout his thesis. Although a
unique name assumption is made, it is not inherent to the utilised reduction
since is explicitly enforced. It is thus possible to eliminate the
propositions that require a unique interpretation of individuals from the
reduction. Hence, together with Lemma~\ref{lem:all-exptime-hard}, we get the
following corollary.

\begin{corollary}
  Consistency of \alcqo-\TgBoxes is \exptime-complete if unary coding of
  number is assumed.
\end{corollary}

Together with Theorem~\ref{theo:alcqi-to-alcqio}, this solves the open problem
concerning the lower bound for the complexity of \alcq with cardinality
restrictions; moreover, it shows that the \nexptime-algorithm presented in
\cite{Baader96a} is not optimal with respect to worst case complexity.

\begin{corollary}\label{cor:alcq-exptime-complete}
  Consistency of \alcq-\TcBoxes is \exptime-complete, if unary coding of numbers 
  in cardinality and number restrictions is used.
\end{corollary}


\subsubsection{\alcqio}

Conversely, using Theorem~\ref{theo:alcqi-to-alcqio} enables us to transfer
the \nexptime-completeness result from Theorem~\ref{theo:alcqi-sat-is-nexptime-hard} to \alcqio.

\begin{corollary}\label{cor:alcqio-nexptime-complete}
  Consistency of \alcqio-\TgBoxes or \TcBoxes is \nexptime-complete.
\end{corollary}

\proof
  For \TgBoxes, this is an immediate corollary of
  Theorem~\ref{theo:alcqi-to-alcqio} and
  Theorem~\ref{theo:alcqi-sat-is-nexptime-hard}. Reasoning with \TcBoxes is as hard as
  for \TgBoxes in the presences of nominals. \qed

  
  This results explains a gap in \cite{DeGiacomo95a}. There the author
  establishes the complexity of satisfiability of knowledge bases consisting
  of \TgBoxes and ABoxes both for $\mathcal{C\!N\!O}$, which allows for
  qualifying number restrictions, and for $\mathcal{C\!I\!O}$, which allows
  for inverse roles, by reduction to an \exptime-complete PDL. No results are
  given for the combination $\mathcal{C\!I\!N\!O}$, which is a strict
  extension of \alcqio.  Corollary~\ref{cor:alcq-exptime-complete} shows that,
  assuming $\exptime \neq \nexptime$, there cannot be a polynomial reduction
  from the satisfiability problem of $\mathcal{C\!I\!N\!O}$ knowledge bases to
  an \exptime-complete PDL.  Again, a possible explanation for this leap in
  complexity is the loss of the tree model property. While for
  $\mathcal{C\!I\!O}$ and $\mathcal{C\!N\!O}$, consistency is decided by
  searching for a tree-like pseudo-models even in the presence of nominals,
  this seems no longer to be possible in the case of knowledge bases for
  $\mathcal{C\!I\!N\!O}$.

\paragraph{Unique Name Assumption}

It should be noted that our definition of nominals is non-standard for
Description Logics in the sense that we do not impose the unique name
assumption that is widely made, i.e., for any two individual names $o_1,o_2
\in N_I$, $o_1^\I \neq o_2^\I$ is required. Even without a unique name
assumption, it is possible to enforce distinct interpretation of nominals by
adding axioms of the form $o_1 \sqsubseteq \neg o_2$.  Moreover, imposing a
unique name assumption in the presence of inverse roles and number restriction
leads to peculiar effects. Consider the following \TgBox:
\begin{equation*}
  T = \{ o \sqsubseteq \nrleq k R \top, \ \top \sqsubseteq \exists R^- . o \}
\end{equation*}
Under the unique name assumption, $T$ is consistent iff $N_I$ contains at most
$k$ individual names, because each individual name must be interpreted by a
unique element of the domain, every element of the domain must be reachable
from $o^\I$ via the role $R$, and $o^\I$ may have at most $k$ $R$-successors.
We believe that this dependency of the consistency of a \TgBox on constraints
that are not explicit in the \TgBox is counter-intuitive and hence have not
imposed the unique name assumption.


Nevertheless, it is possible to obtain a tight complexity bound for
consistency of \alcqio-\TgBoxes with the unique name assumption without using
Theorem~\ref{theo:alcqi-to-alcqio}, but  by an immediate adaption of the 
proof of Theorem~\ref{theo:alcqi-sat-is-nexptime-hard}. 

\begin{corollary}
  Consistency of \alcqio-\TgBoxes \emph{with the unique name assumption} is
  \nexptime-complete if unary coding of numbers assumed.
\end{corollary}



\proof
  A simple inspection of the reduction used to prove
  Theorem~\ref{theo:alcqi-sat-is-nexptime-hard}, and especially of the proof of
  Lemma~\ref{lem:tbox-defines-torus} shows that only a single nominal, which
   marks the upper right corner of the torus, is necessary to perform the
  reduction. If $o$ is an individual name and $\create$ is a role name, then the
  following \TgBox defines a torus of exponential size:
  \[
  \begin{array}{r@{\;}c@{\;}ll}
    T_n & = \bigl \{  & \top \sqsubseteq \exists {\east} . \top, & \top \sqsubseteq
    \exists {\north} . \top, \\ 
    && \top \sqsubseteq  (= 1 \; \east^{-1} \; \top), &   \top \sqsubseteq  (= 1 \;
    \north^{-1} \; \top),\\
    && \top \sqsubseteq  \exists {\create} . {C_{(0,0)}}, &  o \;\sqsubseteq
    C_{(2^n-1,2^n-1)},\\ 
    && C_{(2^n-1,2^n-1)} \sqsubseteq o, & \top \sqsubseteq  D_\east \sqcap  D_\north \ \bigr \}
  \end{array}
  \]
  Since this reduction uses only a single individual name, the unique name
  assumption is irrelevant. \qed



\paragraph{Internalisation of Axioms}

In the presence of inverse roles and nominals, it is possible to \emph{internalise}
general inclusion axioms into concepts using the \emph{spy-point} technique
used, e.g., in \cite{BlackSel-JLLI-95,ArecesBlackburnMarx-CSL-99}. The main
idea of this technique is to enforce that all elements in the model of a
concept are reachable from a distinct point (the spy-point) marked by an
individual name in a single step.

\newcommand{\spy}{\textit{spy}}

\begin{definition}
  Let $T$ be an \alcqio-\TgBox. W.l.o.g., we assume that $T$ is of the form $\{
  \top \sqsubseteq C_1, \dots, \top \sqsubseteq C_k \}$. Let $\spy$ denote a
  fresh role name and $i$ a fresh individual name. We define the function
  $\cdot^{\spy}$ inductively on the structure of concepts by setting $A^{\spy} =
  A $ for all $A \in N_C$, $o^{\spy} = o$ for all $o \in N_I$, $(\neg
  C)^{\spy} = \neg C^{\spy}$, $(C_1 \sqcap C_2)^{\spy} = C_1^{\spy} \sqcap
  C_2^{\spy}$, and ${\nrgeq n R C}^{\spy} = \nrgeq n R {(\exists {\spy^-}.i) \sqcap
    C^{\spy}}$. 
  
  The \emph{internalisation} $C_T$ of $T$ is defined as follows:
  \begin{equation*}
    C_T = i \sqcap \underset{\top \sqsubseteq C \in T}{\mybigsqcap} C^{\spy}
    \sqcap \underset{\top \sqsubseteq C \in T}{\mybigsqcap} \forall \spy . C^{\spy}
  \end{equation*}
\end{definition}

\begin{lemma}\label{lem:spypoint}
  Let $T$ be an \alcqio-\TgBox. $T$ is consistent iff $C_T$ is satisfiable.
\end{lemma}

\proof
  For the \emph{if}-direction let $\I$ be a model of $C_T$ with $a \in
  (C_T)^\I$.  This implies $i^\I = \{ a\}$. Let $\I'$ be defined by
  \[
  \Delta^{\I'} = \{ a\} \cup \{ x \in \Delta^\I \mid (a,x) \in \spy^\I
  \}
  \]
  and $\cdot^{\I'} = \cdot^\I |_{\Delta^{\I'}}$. 
  
  \vspace{1ex}

  \noindent \textsc{Claim 1:} For every $x \in \Delta^{\I'}$ and every
  \alcqio-concept $C$, we have $x \in (C^{\spy})^\I$ iff $x \in C^{\I'}$.
 
  \vspace{1ex}
  
  We proof this claim by induction on the structure of $C$.  The only
  interesting case is $C = \nrgeq n R D$. In this case $C^{\spy} = \nrgeq n R
  {(\exists {\spy^-}.i) \sqcap D^{\spy}}$. We have 
  \begin{align*}
    & x \in \nrgeq n R
    {(\exists {\spy^-}.i) \sqcap D^{\spy}}^\I \\
    \text{iff } \; & \sharp \{ y \in \Delta^\I \mid (x,y) \in R^\I \text{ and } y
    \in (\exists \spy^-.i)^\I \cap (D^{\spy})^\I \} \geqslant n\\
    (*) \text{ iff } \; & \sharp \{ y \in \Delta^{\I'} \mid (x,y) \in R^{\I'} \text{
      and } y \in D^{\I'} \} \geqslant n\\
    \text{iff } \; & x \in \nrgeq n R D^{\I'} ,
  \end{align*}
  where the equivalence  $(*)$ holds because of set equality and the
  definition of $\I'$.

  By construction, for every $\top \sqsubseteq C \in T$ and
  every $x \in \Delta^{\I'}$, $x \in (C^{\spy})^\I$. Due to Claim 1, this
  implies $x \in C^{\I'}$ and hence $\I' \models \top \sqsubseteq C$.
  
  For the \emph{only-if}-direction, let $\I$ be an interpretation with $\I
  \models T$. We pick an arbitrary element $a \in \Delta^\I$ and define an
  extension $\I'$ of $\I$ by setting $i^{\I'} = \{ a \}$ and $\spy^{\I'} = \{
  (a,x) \mid x \in \Delta^\I$. Since $i$ and $\spy$ do not occur in $T$, we
  still have that $\I' \models T$.

  \vspace{1ex}
 
  \noindent \textsc{Claim 2:} For every $x \in \Delta^{\I'}$
  and every \alcqio-concept $C$ that does not contain $i$ or $\spy$, $x \in
  C^{\I'}$ iff $x \in (C^{\spy})^{\I'}$. 

  \vspace{1ex}
  
  Again, this claim is proved by induction on the structure of concepts and the
  only interesting case is $C = \nrgeq n R D$. 
  \begin{align*}
    & x \in \nrgeq n R D^{\I'}\\
    \text{iff } \; & \sharp \{ y \in \Delta^{\I'} \mid (x,y) \in R^{\I'}
    \text{ and } y \in D^{\I'} \} \geqslant n\\
    (*) \text{ iff } \; & \sharp \{ y \in \Delta^{\I'} \mid (x,y) \in R^{\I'},
    (a,y) \in \spy^{\I'}, \text{ and } y \in (D^{\spy})^{\I'} \} \geqslant n\\
    \text{iff } \; & x \in \nrgeq n R {(\exists {\spy^-}.i) \sqcap
      D^{\spy}}^{\I'} .
  \end{align*}
  Again, the equivalence  $(*)$ holds due to set equality and the definition
  of $\I'$.
  
  
  Since, for every $\top \sqsubseteq C \in T$, we have $\I' \models \top
  \sqsubseteq C$, Claim 2 yields that $({\bigsqcap}_{\top \sqsubseteq C \in T}
  C^{\spy} )^{\I'} = \Delta^{\I'}$ and hence $a \in (C_T)^{\I'}$ \qed



As a consequence, we obtain the sharper result that already pure concept
satisfiability for \alcqio is a \nexptime-complete problem.

\begin{corollary}
  Concept satisfiability for \alcqio is \nexptime-complete.
\end{corollary}

\proof
  From Lemma~\ref{lem:spypoint}, we get that the function mapping a
  \alcqio-\TgBox $T$ to $C_T$ is a reduction from consistency of
  \alcqio-\TgBoxes to \alcqio-concept satisfiability. From
  Corollary~\ref{cor:alcqio-nexptime-complete} we know that the former problem
  is \nexptime-complete. Obviously, $C_T$ can be computed from $T$ in
  polynomial time. Hence, the lower complexity bound transfers. \qed



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 

%\input{conclusion}
%%% $Id: conclusion.tex,v 1.15 2000/05/02 11:06:28 tobies Exp $

\section{Conclusion}
\label{sec:conclusion}

Combining the results from \cite{DeGiacomo95a} and
\cite{Tobies-JLC-2000} with the results from this paper, we
obtain the classification of the complexity of concept satisfiability and
TBox-consistency for various DLs and for TBoxes consisting either of
cardinality restrictions or of general concept inclusion axioms shown in
Figure~\ref{fig:complexity}, where  we assume unary coding of numbers. 

\begin{figure}
  \begin{center}
    \framebox[\textwidth]{
      \begin{tabular}{l|cc|cc}
                                %     \hline
        & \alcq & \alcqo & \alcqi & \alcqio\\
      \hline
      Concept Satisfiability & \pspace-c. & open & \pspace-c. & \nexptime-c.\\
      GCIs & \exptime-c. & \exptime-c. & \exptime-c. & \nexptime-c.\\
      Cardinality Restr. & \exptime-c. & \exptime-c. &
      \nexptime-c. & \nexptime-c.
    \end{tabular}
    }
  \end{center}
  \caption{Complexity of the reasoning problems}
  \label{fig:complexity}
\end{figure}

The result for \alcqio shows that the current efforts of extending very
expressive DLs as the logic $\mathcal{S\!H\!I\!Q}$ \cite{Horrocks99j} and
$\mathcal{D\!L\!R}$\cite{calvanese-et-al-1998} or
propositional dynamic logics as $\mathsf{CPDL}_g$ \cite{DeGiacomo96a} with
nominals are difficult tasks, if one wants to obtain a practical decision
procedure, since already concept satisfiability for these logics is a
\nexptime-hard problem.

We have shown that, while having the same complexity
as \ctwo, \alcqi does not reach its expressive power~\cite{Tobies-CSL-99}.  Cardinality
restrictions, although interesting for knowledge representation, are
inherently hard to handle algorithmically.  The same applies to nominals in
the presence of inverse roles and number restrictions. As an explanation for
this we offer the lack of a tree model property, which was identified by
\citeA{Vardi97} as an explanation for good algorithmic behaviour of many modal
logics.

At a first glance, our results make \alcqi with cardinality restrictions on
concepts or \alcqio with general axioms obsolete for knowledge representation
because \ctwo delivers more expressive power at the same computational price.
Yet, is is likely that a dedicated algorithm for \alcqi may have better
average complexity than the \ctwo algorithm; such an algorithm has yet to be
developed.  This is highly desirable as it would also be applicable to
reasoning problems for expressive DLs with nominals, which have applications
in the area of reasoning with database
schemata~\cite{Calvanese98c,calv-degi-lenz:PODS:98}.

An interesting question lies in the coding of numbers: If we allow binary
coding of numbers, the translation approach together with the result from
\cite{LICS::PacholskiST1997} leads to a 2-\nexptime algorithm. As for \ctwo,
it is an open question whether this additional exponential blow-up is
necessary. A positive answer would settle the same question for \ctwo while a
proof of the negative answer might give hints how the result for \ctwo might
be improved. For \alcq with cardinality restrictions, we have partially solved
this problem: with unary coding, the problem is \exptime-complete whereas, for
binary coding, it is \nexptime-hard.

\clearpage

\acks I would like to thank Franz Baader, Ulrike Sattler, and the anonymous referees
for valuable comments and suggestions. This work was supported by the DFG,
Project No. GR 1324/3--1.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 

%\bibliographystyle{theapa} 
%\bibliography{aux,dl,ian,all}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Aiello, Doyle, \BBA\ Shapiro}{Aiello
  et~al.}{1996}]{kr'96}
Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.~C.\BEDS., Proceedings of KR'96
  \BBOP1996\BBCP.
\newblock {\Bem Principles of Knowledge Representation and Reasoning:
  Proceedings of the Fifth International Conference (KR'96)}. Morgan Kaufmann
  Publishers, San Francisco, California.

\bibitem[\protect\BCAY{Areces, Blackburn, \BBA\ Marx}{Areces
  et~al.}{1999}]{ArecesBlackburnMarx-CSL-99}
Areces, C., Blackburn, P., \BBA\ Marx, M. \BBOP1999\BBCP.
\newblock \BBOQ A road-map on complexity for hybrid logics\BBCQ\
\newblock In {\Bem Proceedings of the Annual Conference of the European
  Association for Computer Science Logic {(CSL-99)}}, LNCS 1683, \BPGS\
  307--321. Springer-Verlag.

\bibitem[\protect\BCAY{Baader, Buchheit, \BBA\ Hollunder}{Baader
  et~al.}{1996}]{Baader96a}
Baader, F., Buchheit, M., \BBA\ Hollunder, B. \BBOP1996\BBCP.
\newblock \BBOQ Cardinality restrictions on concepts\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 88\/}(1--2), 195--213.

\bibitem[\protect\BCAY{Baader \BBA\ Sattler}{Baader \BBA\
  Sattler}{1999}]{BaaderSattler-JLC-99}
Baader, F.\BBACOMMA\  \BBA\ Sattler, U. \BBOP1999\BBCP.
\newblock \BBOQ Expressive number restrictions in description logics\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 9\/}(3), 319--350.

\bibitem[\protect\BCAY{Berger}{Berger}{1966}]{Ber66}
Berger, R. \BBOP1966\BBCP.
\newblock \BBOQ The undecidability of the dominoe problem\BBCQ\
\newblock {\Bem Memoirs of the American Mathematical Society}, {\Bem 66}.

\bibitem[\protect\BCAY{Blackburn \BBA\ Seligman}{Blackburn \BBA\
  Seligman}{1996}]{BlackSel-JLLI-95}
Blackburn, P.\BBACOMMA\  \BBA\ Seligman, J. \BBOP1996\BBCP.
\newblock \BBOQ Hybrid languages\BBCQ\
\newblock {\Bem Journal of Logic, Language and Information}, {\Bem 3\/}(4),
  251--272.

\bibitem[\protect\BCAY{B{\"o}rger, Gr{\"a}del, \BBA\ Gurevich}{B{\"o}rger
  et~al.}{1997}]{BBG:clad}
B{\"o}rger, E., Gr{\"a}del, E., \BBA\ Gurevich, Y. \BBOP1997\BBCP.
\newblock {\Bem The Classical Decision Problem}.
\newblock Perspectives in Mathematical Logic. Springer-Verlag, Berlin.

\bibitem[\protect\BCAY{Borgida}{Borgida}{1996}]{Borgida96a}
Borgida, A. \BBOP1996\BBCP.
\newblock \BBOQ On the relative expressiveness of description logics and first
  order logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 82}, 353--367.

\bibitem[\protect\BCAY{Borgida \BBA\ Patel-Schneider}{Borgida \BBA\
  Patel-Schneider}{1994}]{BOR:PAT:JAIR94}
Borgida, A.\BBACOMMA\  \BBA\ Patel-Schneider, P.~F. \BBOP1994\BBCP.
\newblock \BBOQ A semantic and complete algorithm for subsumption in the
  classic description logic\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1},
  277--308.

\bibitem[\protect\BCAY{Calvanese, {De~Giacomo}, Lenzerini, Nardi, \BBA\
  Rosati}{Calvanese et~al.}{1998a}]{Calvanese98c}
Calvanese, D., {De~Giacomo}, G., Lenzerini, M., Nardi, D., \BBA\ Rosati, R.
  \BBOP1998a\BBCP.
\newblock \BBOQ Source integration in data warehousing\BBCQ\
\newblock In {\Bem Proceedings of the Ninth International Workshop on Database
  and Expert Systems Applications (DEXA-98)}, \BPGS\ 192--197. {IEEE} Computer
  Society Press.

\bibitem[\protect\BCAY{Calvanese, De~Giacomo, \BBA\ Lenzerini}{Calvanese
  et~al.}{1998b}]{calv-degi-lenz:PODS:98}
Calvanese, D., De~Giacomo, G., \BBA\ Lenzerini, M. \BBOP1998b\BBCP.
\newblock \BBOQ On the decidability of query containment under
  constraints\BBCQ\
\newblock In {\Bem Proceedings of the Seventeenth ACM SIGACT SIGMOD SIGART
  Symposium on Principles of Database Systems (PODS-98)}.

\bibitem[\protect\BCAY{Calvanese, De~Giacomo, Lenzerini, Nardi, \BBA\
  Rosati}{Calvanese et~al.}{1998c}]{calvanese-et-al-1998}
Calvanese, D., De~Giacomo, G., Lenzerini, M., Nardi, D., \BBA\ Rosati, R.
  \BBOP1998c\BBCP.
\newblock \BBOQ Description logic framework for information integration\BBCQ\
\newblock In {\Bem Proc.\ of the 6th Int.\ Conf.\ on the Principles of
  Knowledge Representation and Reasoning (KR'98)}, \BPGS\ 2--13.

\bibitem[\protect\BCAY{{De~Giacomo}}{{De~Giacomo}}{1995}]{DeGiacomo95a}
{De~Giacomo}, G. \BBOP1995\BBCP.
\newblock {\Bem Decidability of Class-Based Knowledge Representation
  Formalisms}.
\newblock Ph.D.\ thesis, Dipartimento di Informatica e Sistemistica, Univ.\ di Roma ``La
  Sapienza''.

\bibitem[\protect\BCAY{{De~Giacomo} \BBA\ Lenzerini}{{De~Giacomo} \BBA\
  Lenzerini}{1996}]{DeGiacomo96a}
{De~Giacomo}, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1996\BBCP.
\newblock \BBOQ {TBox} and {ABox} reasoning in expressive description
  logics\BBCQ.
\newblock In Aiello et~al. \cite{kr'96}, \BPGS\ 316--327.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini
  et~al.}{1996}]{DoniniLenzerini+:1996}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Schaerf, A. \BBOP1996\BBCP.
\newblock \BBOQ Reasoning in description logics\BBCQ\
\newblock In Brewka, G.\BED, {\Bem Foundation of Knowledge Representation},
  \BPGS\ 191--236. CSLI-Publications.

\bibitem[\protect\BCAY{Fine}{Fine}{1972}]{Fine72}
Fine, K. \BBOP1972\BBCP.
\newblock \BBOQ In so many possible worlds\BBCQ\
\newblock {\Bem Notre Dame Journal of Formal Logic}, {\Bem 13}, 516--520.

\bibitem[\protect\BCAY{Gargov \BBA\ Goranko}{Gargov \BBA\
  Goranko}{1993}]{GargovGoranko1993}
Gargov, G.\BBACOMMA\  \BBA\ Goranko, V. \BBOP1993\BBCP.
\newblock \BBOQ Modal logic with names\BBCQ\
\newblock {\Bem J.\ of Philosophical Logic}, {\Bem 22}, 607--636.

\bibitem[\protect\BCAY{Gr{\"a}del, Otto, \BBA\ Rosen}{Gr{\"a}del
  et~al.}{1997}]{LICS::GradelOR1997}
Gr{\"a}del, E., Otto, M., \BBA\ Rosen, E. \BBOP1997\BBCP.
\newblock \BBOQ Two-variable logic with counting is decidable\BBCQ\
\newblock In {\Bem Proceedings, Twelth Annual {IEEE} Symposium on Logic in
  Computer Science}, \BPGS\ 306--317\ Warsaw, Poland. IEEE Computer Society
  Press.

\bibitem[\protect\BCAY{Halpern \BBA\ Moses}{Halpern \BBA\
  Moses}{1992}]{HalpernMoses92}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Moses, Y. \BBOP1992\BBCP.
\newblock \BBOQ A guide to completeness and complexity for model logics of
  knowledge and belief\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 54\/}(3), 319--379.

\bibitem[\protect\BCAY{Horrocks, Sattler, \BBA\ Tobies}{Horrocks
  et~al.}{1999}]{Horrocks99j}
Horrocks, I., Sattler, U., \BBA\ Tobies, S. \BBOP1999\BBCP.
\newblock \BBOQ Practical reasoning for expressive description logics\BBCQ\
\newblock In {\Bem Proceedings of the 6th International Conference on Logic for
  Programming and Automated Reasoning (LPAR'99)}, \BPGS\ 161--180.

\bibitem[\protect\BCAY{Pacholski, Szwast, \BBA\ Tendera}{Pacholski
  et~al.}{1997}]{LICS::PacholskiST1997}
Pacholski, L., Szwast, W., \BBA\ Tendera, L. \BBOP1997\BBCP.
\newblock \BBOQ Complexity of two-variable logic with counting\BBCQ\
\newblock In {\Bem Proceedings, Twelth Annual {IEEE} Symposium on Logic in
  Computer Science}, \BPGS\ 318--327\ Warsaw, Poland. IEEE Computer Society
  Press.

\bibitem[\protect\BCAY{Pratt}{Pratt}{1979}]{Pratt1979}
Pratt, V.~R. \BBOP1979\BBCP.
\newblock \BBOQ Models of program logics\BBCQ\
\newblock In {\Bem Proceedings of the Twentieth {IEEE} Symposium on Foundations
  of Computer Science}, \BPGS\ 115--122. {IEEE}.

\bibitem[\protect\BCAY{Schmidt-Schau{\ss} \BBA\ Smolka}{Schmidt-Schau{\ss}
  \BBA\ Smolka}{1991}]{Schmidt-Schauss91}
Schmidt-Schau{\ss}, M.\BBACOMMA\  \BBA\ Smolka, G. \BBOP1991\BBCP.
\newblock \BBOQ Attributive concept descriptions with complements\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 48}, 1--26.

\bibitem[\protect\BCAY{Spaan}{Spaan}{1993}]{Spaan93}
Spaan, E. \BBOP1993\BBCP.
\newblock {\Bem Complexity of Modal Logics}.
\newblock Ph.D.\ thesis, University of Amsterdam.

\bibitem[\protect\BCAY{Tobies}{Tobies}{1999}]{Tobies-CSL-99}
Tobies, S. \BBOP1999\BBCP.
\newblock \BBOQ A {NExpTime}-complete description logic strictly contained in
  {$C^2$}\BBCQ\
\newblock In Flum, J.\BBACOMMA\  \BBA\ Rodr{\'i}guez-Artalejo, M.\BEDS, {\Bem
  Proceedings of the Annual Conference of the European Association for Computer
  Science Logic {(CSL-99)}}, LNCS 1683, \BPGS\ 292--306. Springer-Verlag.

\bibitem[\protect\BCAY{Tobies}{Tobies}{2000}]{Tobies-JLC-2000}
Tobies, S. \BBOP2000\BBCP.
\newblock \BBOQ {PSPACE} reasoning for graded modal logics\BBCQ\
\newblock {\Bem Journal of Logic and Computation}.
\newblock To appear.

\bibitem[\protect\BCAY{Vardi}{Vardi}{1997}]{Vardi97}
Vardi, M.~Y. \BBOP1997\BBCP.
\newblock \BBOQ Why is modal logic so robustly decidable?\BBCQ\
\newblock In {\Bem Descriptive Complexity and Finite Models: Proceedings of a
  DIMACS Workshop, January 14-17, 1996}, \lowercase{\BNUM}~31 in DIMACS Series
  in Discrete Mathematics and Theoretical Computer Science, \BPGS\ 149--184.
  American Math. Society.

\bibitem[\protect\BCAY{Wang}{Wang}{1963}]{Wang63}
Wang, H. \BBOP1963\BBCP.
\newblock \BBOQ Dominoes and the {AEA} case of the {D}ecision {P}roblem\BBCQ\
\newblock {\Bem Bell {S}yst. {T}ech. {J}.}, {\Bem 40}, 1--41.

\bibitem[\protect\BCAY{Woods \BBA\ Schmolze}{Woods \BBA\
  Schmolze}{1992}]{Woods92}
Woods, W.~A.\BBACOMMA\  \BBA\ Schmolze, J.~G. \BBOP1992\BBCP.
\newblock \BBOQ The \textsc{Kl-One} family\BBCQ\
\newblock {\Bem Computers and Mathematics with Applications -- Special Issue on
  Artificial Intelligence}, {\Bem 23\/}(2--5), 133--177.

\end{thebibliography}


\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 







