\documentclass[twoside,11pt,letterpaper]{article}
\usepackage{jair}
\usepackage{theapa}


\usepackage{amsmath,amssymb,amsthm}
\usepackage{epsfig}
\usepackage{color}
\usepackage{bbm}
\usepackage{boxedminipage}
\usepackage{pifont}
\usepackage{xspace}
\usepackage{graphics}
\usepackage{url}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

%
% Uli stuff
%

\newcommand{\ca}{\textsf{(Ca)}\xspace}
\newcommand{\cb}{\textsf{(Cb)}\xspace}
\newcommand{\cc}{\textsf{(Cc)}\xspace}
\newcommand{\cd}{\textsf{(Cd)}\xspace}
\newcommand{\ce}{\textsf{(Ce)}\xspace}

\newcommand{\simc}{\sim_{\mathsf c}}
\newcommand{\approxcm}[1]{\approx^{#1}_{\mathsf c}}
\newcommand{\approxc}{\approx_{\mathsf c}}
\newcommand{\approxa}{\approx_{\mathsf a}}
\newcommand{\approxam}[1]{\approx^{#1}_{\mathsf a}}

\newcommand{\Inv}{\mn{Inv}}
\newcommand{\Tr}{\mn{Trans}}
\newcommand{\sss}{{\mathrel{\kern.25em{\sqsubseteq}\kern-.5em \mbox{{\scriptsize *}}\kern.25em}}}
\newcommand{\smallsss}{{\mathrel{\kern.25em{\sqsubseteq}\kern-.4em \mbox{{\scriptsize *}}\kern.25em}}}
\newcommand{\qnrleq}[3]{\ensuremath{(\leqslant #1 \; #2 \; #3)}}
\newcommand{\qnrgeq}[3]{\ensuremath{(\geqslant #1 \; #2 \; #3)}}
\newcommand{\hset}[1]{\mbox{\textbf{(S#1)}}}
\newcommand{\hnode}[1]{\mbox{\textbf{(N#1)}}}
\newcommand{\hmatch}[1]{\mbox{\textbf{(M#1)}}}
\newcommand{\htree}[1]{\mbox{\textbf{(T#1)}}}
\newcommand{\htg}[1]{\mbox{\textbf{(G#1)}}}

\newcommand{\Inds}{\ensuremath{\mathsf{N_N}}}

\newcommand{\ndoteq}{\mathop{\not\doteq}}
\newcommand{\nneg}{\mathop{\dot\neg}}
\newcommand{\keyfor}{\text{ keyfor }}

\newcommand{\Et}{\ensuremath{E}\xspace}
\newcommand{\Etc}{\ensuremath{\mathop e}\xspace}

\newcommand{\Efa}{\ensuremath{\mathop{E_r}}\xspace}
\newcommand{\Efv}{\ensuremath{\mathop{E_v}}\xspace}
\newcommand{\Efc}{\ensuremath{\mathop e}\xspace}

\newcommand{\T}{\ensuremath{\mathbf T}\xspace}
\newcommand{\R}{\ensuremath{\mathcal R}\xspace}
\renewcommand{\S}{\ensuremath{\mathbf S}\xspace}
\newcommand{\tuple}[2]{(#1,#2)}

\newcommand{\some}[2]{\exists #1.#2}
\newcommand{\all}[2]{\forall #1.#2}
\newcommand{\atleastq}[3]{\ensuremath{(\geqslant #1 \; #2 \; #3)}}
\newcommand{\atmostq}[3]{\ensuremath{(\leqslant #1 \; #2 \; #3)}}

\newcommand{\tabl}[1]{\mbox{\textbf{(T#1)}}}
\newcommand{\clash}[1]{\mbox{\textbf{(C#1)}}}

\newcommand{\I}{\ensuremath{\mathcal{I}}\xspace}
\newcommand{\ifunc}{\ensuremath{^{\mathcal{I}}}}

\newcommand{\gt}[2]{{#1}\!{\rightarrow}\!#2}
\newcommand{\Etilde}{\ensuremath{\tilde{E}}}
\newcommand{\Ltilde}{\ensuremath{\tilde{\Lmc}}}
\newcommand{\dotsim}{\ensuremath{\mathrel{\dot\sim}}}
\newcommand{\node}{\ensuremath{\mathop{\mathsf{node}}}}


%
% Index stuff
%
\newcommand{\emphindex}[1]{\emph{#1}\index{#1}}
\newcommand{\indextext}[1]{\index{#1}#1}

%
% DL Names
%
\newcommand{\ALC}{\ensuremath{{\cal ALC}}\xspace}
\newcommand{\ALCD}{\ensuremath{{\cal ALC(D)}}\xspace}
\newcommand{\ALCO}{\ensuremath{{\cal ALCO}}\xspace}
\newcommand{\ALCK}{\ensuremath{{\cal ALCK}}\xspace}
\newcommand{\ALCI}{\ensuremath{{\cal ALCI}}\xspace}
\newcommand{\ALCOD}{\ensuremath{{\cal ALCO(D)}}\xspace}
\newcommand{\ALCKD}{\ensuremath{{\cal ALCK(D)}}\xspace}
\newcommand{\ALCOKD}{\ensuremath{{\cal ALCOK(D)}}\xspace}
\newcommand{\ALCID}{\ensuremath{{\cal ALC}^-(\Dmc)}\xspace}
\newcommand{\ALCDmin}{\ensuremath{{\cal ALC}f(\Dmc)}\xspace}
\newcommand{\ALCFD}{\ensuremath{{\cal ALCF(D)}}\xspace}
\newcommand{\ALCPD}{\ensuremath{{\cal ALCP(D)}}\xspace}
\newcommand{\ALCRPD}{\ensuremath{{\cal ALC}^{rp}({\cal D})}\xspace}
\newcommand{\ALCRPID}{\ensuremath{{\cal ALC}^{rp,-}({\cal D})}\xspace}
\newcommand{\BIGL}{\ensuremath{{\cal ALCP}^{rp,-,\sqcap}({\cal D})}\xspace}
\newcommand{\ALCF}{\ensuremath{{\cal ALCF}}\xspace}
\newcommand{\ALCFI}{\ensuremath{{\cal ALCF}^-}\xspace}
\newcommand{\ALCNR}{\ensuremath{{\cal ALCNR}}\xspace}
\newcommand{\ALCQ}{\ensuremath{{\cal ALCQ}}\xspace}
\newcommand{\HS}{\ensuremath{{\sf HS}}\xspace}
\newcommand{\shiq}{\ensuremath{{\cal SHIQ}}\xspace}
\newcommand{\shoq}{\ensuremath{{\cal SHOQ}}\xspace}
\newcommand{\TDL}{\ensuremath{{\cal TDL}}\xspace}
\newcommand{\OIL}{\ensuremath{{\sf OIL}}\xspace}
\newcommand{\DAMLOIL}{\ensuremath{{\sf DAML{+}OIL}}\xspace}
\newcommand{\shiqt}{\ensuremath{\mathbbm{Q}\text{-}{\cal SHIQ}}\xspace}
\newcommand{\shiqtva}{\ensuremath{\shiqt^\ast}\xspace}
\newcommand{\shiqtvb}{\ensuremath{\shiqt^{\ast\ast}}\xspace}
\newcommand{\SHIQ}{\ensuremath{{\cal SHIQ}}\xspace}
\newcommand{\SHIQO}{\ensuremath{{\cal SHIQO}}\xspace}
\newcommand{\SHOQ}{\ensuremath{{\cal SHOQ}}\xspace}
\newcommand{\SHOQD}{\ensuremath{{\cal SHOQ(D)}}\xspace}
\newcommand{\SHOQKD}{\ensuremath{{\cal SHOQK(D)}}\xspace}
\newcommand{\roles}{\ensuremath{\mn{ROL}}\xspace}
\newcommand{\concepts}{\ensuremath{\mn{CON}}\xspace}

%
% System Names
%
\newcommand{\KRIS}{\ensuremath{{\cal KRIS}}\xspace}
\newcommand{\FaCT}{\ensuremath{{\sf FaCT}}\xspace}
\newcommand{\RACER}{\ensuremath{{\sf RACER}}\xspace}
\newcommand{\Meson}{\textnormal{{\textsc{meson}}}\xspace}
\newcommand{\Classic}{\textnormal{{\textsc{classic}}}\xspace}

%
% Numbers
%
\newcommand{\naturals}{\ensuremath{\mathbb{N}}\xspace}
\newcommand{\naturalswz}{\ensuremath{\mathbb{N}_0}\xspace}
\newcommand{\integers}{\ensuremath{\mathbb{Z}}\xspace}
\newcommand{\rationals}{\ensuremath{\mathbb{Q}}\xspace}
\newcommand{\reals}{\ensuremath{\mathbb{R}}\xspace}

%
% Sets, functions, operators, etc.
%
\newcommand{\mn}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\bigo}{\ensuremath{\mathcal{O}}}
\newcommand{\con}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\impl}{\rightarrow}
\newcommand{\ineq}{\not\sim}

\newcommand{\NC}{\ensuremath{{\sf N_C}}\xspace}
\newcommand{\NO}{\ensuremath{{\sf N_O}}\xspace}
\newcommand{\NaF}{\ensuremath{{\sf N_{aF}}}\xspace}
\newcommand{\NcF}{\ensuremath{{\sf N_{cF}}}\xspace}
\newcommand{\NcFDK}{\ensuremath{{\sf N}_{\sf cF}^{D,\Kmc}}\xspace}
\newcommand{\NRDRK}{\ensuremath{{\sf N}_{\sf R}^{D,\Rmc,\Kmc}}\xspace}
\newcommand{\NcFD}{\ensuremath{{\sf N}_{\sf cF}^{D}}\xspace}
\newcommand{\NRDR}{\ensuremath{{\sf N}_{\sf R}^{D,\Rmc}}\xspace}
\newcommand{\NR}{\ensuremath{{\sf N_R}}\xspace}
\newcommand{\NtR}{\ensuremath{{\sf N_{tR}}}\xspace}
\newcommand{\NrR}{\ensuremath{{\sf N_{rR}}}\xspace}

\newcommand{\OA}{\ensuremath{{\sf O}_{\sf a}}\xspace}
\newcommand{\OC}{\ensuremath{{\sf O}_{\sf c}}\xspace}

\newcommand{\V}{\ensuremath{{\sf V}}\xspace}

\newcommand{\sub}{\ensuremath{{\sf sub}}\xspace}

\newcommand{\my}{\ensuremath{\mathop{\rule[-.05em]{0.33pt}{7.5pt}\rule[.25em]{3ex}{.33pt}}}}
\newcommand{\mys}{\ensuremath{\mathop{\rule[-.05em]{0.33pt}{7.5pt}\overset{*}{\rule[.25em]{3ex}{.33pt}}}}}

\newcommand{\nnf}{\ensuremath{\mathsf{nnf}}\xspace}
\newcommand{\cl}{\mathop{\mathsf{cl}}}

%
% Other abbreviations
%
\newcommand{\bauts}{looping automata\xspace}
\newcommand{\baut}{looping automaton\xspace}
\newcommand{\hint}[1]{\mbox{\textbf{(H#1)}}}
\newcommand{\pcpl}[1]{\mbox{\textbf{(P#1)}}}
\newcommand{\cand}[1]{\mbox{\textbf{(C#1)}}}
\newcommand{\zip}[1]{\mbox{\textbf{(Z#1)}}}

%
% For the layout of algorithms
%
\newlength{\indxlength}
\setlength{\indxlength}{4mm}
\newcommand{\ind}[1]{\hspace*{#1\indxlength}}

%
% Complexity classes
%
\newcommand{\cclass}{\textnormal{\sc C}\xspace}
\newcommand{\PTime}{\textnormal{\sc PTime}\xspace}
\newcommand{\NP}{\textnormal{\sc NP}\xspace}
\newcommand{\PSpace}{\textnormal{\sc PSpace}\xspace}
\newcommand{\NPSpace}{\textnormal{\sc NPSpace}\xspace}
\newcommand{\ExpTime}{\textnormal{\sc ExpTime}\xspace}
\newcommand{\NExpTime}{\textnormal{\sc NExpTime}\xspace}
\newcommand{\TwoNExpTime}{\textnormal{\sc 2-NExpTime}\xspace}
\newcommand{\exptime}{\textnormal{\sc exptime}\xspace}
\newcommand{\nexptime}{\textnormal{\sc nexptime}\xspace}
\newcommand{\ExpSpace}{\textnormal{\sc ExpSpace}\xspace}
\newcommand{\TwoExpSpace}{\textnormal{\sc 2-ExpSpace}\xspace}
\newcommand{\expspace}{\textnormal{\sc expspace}\xspace}
\newcommand{\NExpSpace}{\textnormal{\sc NExpSpace}\xspace}
\newcommand{\TwoNExpSpace}{\textnormal{\sc 2-NExpSpace}\xspace}

%
% Completion rules
%
\newcommand{\Rand}{\ensuremath{\Rsf\sqcap}\xspace}
\newcommand{\Ror}{\ensuremath{\Rsf\sqcup}\xspace}
\newcommand{\Rex}{\ensuremath{\Rsf\exists}\xspace}
\newcommand{\Rnom}{\ensuremath{\mathsf{Rnom}}\xspace}
\newcommand{\Rexco}{\ensuremath{\Rsf\exists\mathsf{c}}\xspace}
\newcommand{\Rall}{\ensuremath{\Rsf\forall}\xspace}
\newcommand{\Rallplus}{\ensuremath{\Rsf\forall_+}\xspace}

\newcommand{\Rsima}{\ensuremath{\Rsf{\approxa}}\xspace}
\newcommand{\Rsimc}{\ensuremath{\Rsf{\sim}_c}\xspace}
\newcommand{\Rgeq}{\ensuremath{\Rsf{\geqslant}}\xspace}
\newcommand{\Rleq}{\ensuremath{\Rsf{\leqslant}}\xspace}

\newcommand{\Rfex}{\ensuremath{\Rsf\exists\fsf}\xspace}
\newcommand{\Rfall}{\ensuremath{\Rsf\forall\fsf}\xspace}
\newcommand{\Rrex}{\ensuremath{\Rsf\exists\rsf}\xspace}
\newcommand{\Rrall}{\ensuremath{\Rsf\forall\rsf}\xspace}
\newcommand{\Rch}{\ensuremath{\Rsf\mn{ch}}\xspace}
\newcommand{\Rc}{\ensuremath{\Rsf\csf}\xspace}
\newcommand{\Rca}{\ensuremath{\Rsf\csf1}\xspace}
\newcommand{\Rcb}{\ensuremath{\Rsf\csf2}\xspace}
\newcommand{\Rcc}{\ensuremath{\Rsf\csf3}\xspace}
\newcommand{\Rexc}{\ensuremath{\Rsf\exists\csf}\xspace}
\newcommand{\Rallc}{\ensuremath{\Rsf\forall\csf}\xspace}
\newcommand{\Rrc}{\ensuremath{\Rsf\psf\rsf}\xspace}
\newcommand{\Ragr}{\ensuremath{\Rsf{\downarrow}}\xspace}
\newcommand{\Rdagr}{\ensuremath{\Rsf{\uparrow}}\xspace}
\newcommand{\Rfe}{\ensuremath{\Rsf\mn{fe}}\xspace}
\newcommand{\Rtb}{\ensuremath{\Rsf{\doteq}}\xspace}
\newcommand{\Rp}{\ensuremath{\Rsf\mn{p}}\xspace}
\newcommand{\Rsim}{\ensuremath{\Rsf\!{\sim}}\xspace}
\newcommand{\RN}{\ensuremath{\Rsf{N}}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% ABBREVIATIONS FOR LETTERS
%

%
% Calligraphic letters
%
\newcommand{\Amc}{\ensuremath{\mathcal{A}}\xspace}
\newcommand{\Bmc}{\ensuremath{\mathcal{B}}\xspace}
\newcommand{\Cmc}{\ensuremath{\mathcal{C}}\xspace}
\newcommand{\Dmc}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\Emc}{\ensuremath{\mathcal{E}}\xspace}
\newcommand{\Fmc}{\ensuremath{\mathcal{F}}\xspace}
\newcommand{\Gmc}{\ensuremath{\mathcal{G}}\xspace}
\newcommand{\Hmc}{\ensuremath{\mathcal{H}}\xspace}
\newcommand{\Imc}{\ensuremath{\mathcal{I}}\xspace}
\newcommand{\Jmc}{\ensuremath{\mathcal{J}}\xspace}
\newcommand{\Kmc}{\ensuremath{\mathcal{K}}\xspace}
\newcommand{\Lmc}{\ensuremath{\mathcal{L}}\xspace}
\newcommand{\Mmc}{\ensuremath{\mathcal{M}}\xspace}
\newcommand{\Nmc}{\ensuremath{\mathcal{N}}\xspace}
\newcommand{\Omc}{\ensuremath{\mathcal{O}}\xspace}
\newcommand{\Pmc}{\ensuremath{\mathcal{P}}\xspace}
\newcommand{\Qmc}{\ensuremath{\mathcal{Q}}\xspace}
\newcommand{\Rmc}{\ensuremath{\mathcal{R}}\xspace}
\newcommand{\Smc}{\ensuremath{\mathcal{S}}\xspace}
\newcommand{\Tmc}{\ensuremath{\mathcal{T}}\xspace}
\newcommand{\Umc}{\ensuremath{\mathcal{U}}\xspace}
\newcommand{\Vmc}{\ensuremath{\mathcal{V}}\xspace}
\newcommand{\Wmc}{\ensuremath{\mathcal{W}}\xspace}
\newcommand{\Xmc}{\ensuremath{\mathcal{X}}\xspace}
\newcommand{\Ymc}{\ensuremath{\mathcal{Y}}\xspace}
\newcommand{\Zmc}{\ensuremath{\mathcal{Z}}\xspace}

%
% Fraktur letters
%
\newcommand{\Amf}{\ensuremath{\mathfrak{A}}\xspace}
\newcommand{\Bmf}{\ensuremath{\mathfrak{B}}\xspace}
\newcommand{\Cmf}{\ensuremath{\mathfrak{C}}\xspace}
\newcommand{\Dmf}{\ensuremath{\mathfrak{D}}\xspace}
\newcommand{\Emf}{\ensuremath{\mathfrak{E}}\xspace}
\newcommand{\Fmf}{\ensuremath{\mathfrak{F}}\xspace}
\newcommand{\Gmf}{\ensuremath{\mathfrak{G}}\xspace}
\newcommand{\Hmf}{\ensuremath{\mathfrak{H}}\xspace}
\newcommand{\Imf}{\ensuremath{\mathfrak{I}}\xspace}
\newcommand{\Jmf}{\ensuremath{\mathfrak{J}}\xspace}
\newcommand{\Kmf}{\ensuremath{\mathfrak{K}}\xspace}
\newcommand{\Lmf}{\ensuremath{\mathfrak{L}}\xspace}
\newcommand{\Mmf}{\ensuremath{\mathfrak{M}}\xspace}
\newcommand{\Nmf}{\ensuremath{\mathfrak{N}}\xspace}
\newcommand{\Omf}{\ensuremath{\mathfrak{O}}\xspace}
\newcommand{\Pmf}{\ensuremath{\mathfrak{P}}\xspace}
\newcommand{\Qmf}{\ensuremath{\mathfrak{Q}}\xspace}
\newcommand{\Rmf}{\ensuremath{\mathfrak{R}}\xspace}
\newcommand{\Smf}{\ensuremath{\mathfrak{S}}\xspace}
\newcommand{\Tmf}{\ensuremath{\mathfrak{T}}\xspace}
\newcommand{\Umf}{\ensuremath{\mathfrak{U}}\xspace}
\newcommand{\Vmf}{\ensuremath{\mathfrak{V}}\xspace}
\newcommand{\Wmf}{\ensuremath{\mathfrak{W}}\xspace}
\newcommand{\Xmf}{\ensuremath{\mathfrak{X}}\xspace}
\newcommand{\Ymf}{\ensuremath{\mathfrak{Y}}\xspace}
\newcommand{\Zmf}{\ensuremath{\mathfrak{Z}}\xspace}

%
% Boldface letters
%
\newcommand{\Abf}{\ensuremath{\mathbf{A}}\xspace}
\newcommand{\Bbf}{\ensuremath{\mathbf{B}}\xspace}
\newcommand{\Cbf}{\ensuremath{\mathbf{C}}\xspace}
\newcommand{\Dbf}{\ensuremath{\mathbf{D}}\xspace}
\newcommand{\Ebf}{\ensuremath{\mathbf{E}}\xspace}
\newcommand{\Fbf}{\ensuremath{\mathbf{F}}\xspace}
\newcommand{\Gbf}{\ensuremath{\mathbf{G}}\xspace}
\newcommand{\Hbf}{\ensuremath{\mathbf{H}}\xspace}
\newcommand{\Ibf}{\ensuremath{\mathbf{I}}\xspace}
\newcommand{\Jbf}{\ensuremath{\mathbf{J}}\xspace}
\newcommand{\Kbf}{\ensuremath{\mathbf{K}}\xspace}
\newcommand{\Lbf}{\ensuremath{\mathbf{L}}\xspace}
\newcommand{\Mbf}{\ensuremath{\mathbf{M}}\xspace}
\newcommand{\Nbf}{\ensuremath{\mathbf{N}}\xspace}
\newcommand{\Obf}{\ensuremath{\mathbf{O}}\xspace}
\newcommand{\Pbf}{\ensuremath{\mathbf{P}}\xspace}
\newcommand{\Qbf}{\ensuremath{\mathbf{Q}}\xspace}
\newcommand{\Rbf}{\ensuremath{\mathbf{R}}\xspace}
\newcommand{\Sbf}{\ensuremath{\mathbf{S}}\xspace}
\newcommand{\Tbf}{\ensuremath{\mathbf{T}}\xspace}
\newcommand{\Ubf}{\ensuremath{\mathbf{U}}\xspace}
\newcommand{\Vbf}{\ensuremath{\mathbf{V}}\xspace}
\newcommand{\Wbf}{\ensuremath{\mathbf{W}}\xspace}
\newcommand{\Xbf}{\ensuremath{\mathbf{X}}\xspace}
\newcommand{\Ybf}{\ensuremath{\mathbf{Y}}\xspace}
\newcommand{\Zbf}{\ensuremath{\mathbf{Z}}\xspace}

%
% Sans Serife Letter
%
\newcommand{\Asf}{\ensuremath{\mathsf{A}}\xspace}
\newcommand{\Bsf}{\ensuremath{\mathsf{B}}\xspace}
\newcommand{\Csf}{\ensuremath{\mathsf{C}}\xspace}
\newcommand{\Dsf}{\ensuremath{\mathsf{D}}\xspace}
\newcommand{\Esf}{\ensuremath{\mathsf{E}}\xspace}
\newcommand{\Fsf}{\ensuremath{\mathsf{F}}\xspace}
\newcommand{\Gsf}{\ensuremath{\mathsf{G}}\xspace}
\newcommand{\Hsf}{\ensuremath{\mathsf{H}}\xspace}
\newcommand{\Isf}{\textnormal{I}\xspace}
\newcommand{\Jsf}{\ensuremath{\mathsf{J}}\xspace}
\newcommand{\Ksf}{\ensuremath{\mathsf{K}}\xspace}
\newcommand{\Lsf}{\ensuremath{\mathsf{L}}\xspace}
\newcommand{\Msf}{\ensuremath{\mathsf{M}}\xspace}
\newcommand{\Nsf}{\ensuremath{\mathsf{N}}\xspace}
\newcommand{\Osf}{\ensuremath{\mathsf{O}}\xspace}
\newcommand{\Psf}{\ensuremath{\mathsf{P}}\xspace}
\newcommand{\Qsf}{\ensuremath{\mathsf{Q}}\xspace}
\newcommand{\Rsf}{\ensuremath{\mathsf{R}}\xspace}
\newcommand{\Ssf}{\ensuremath{\mathsf{S}}\xspace}
\newcommand{\Tsf}{\ensuremath{\mathsf{T}}\xspace}
\newcommand{\Usf}{\ensuremath{\mathsf{U}}\xspace}
\newcommand{\Vsf}{\ensuremath{\mathsf{V}}\xspace}
\newcommand{\Wsf}{\ensuremath{\mathsf{W}}\xspace}
\newcommand{\Xsf}{\ensuremath{\mathsf{X}}\xspace}
\newcommand{\Ysf}{\ensuremath{\mathsf{Y}}\xspace}
\newcommand{\Zsf}{\ensuremath{\mathsf{Z}}\xspace}
%
% small
%
\newcommand{\asf}{\ensuremath{\mathsf{a}}\xspace}
%\newcommand{\bsf}{\ensuremath{\mathsf{b}}\xspace}
\newcommand{\csf}{\ensuremath{\mathsf{c}}\xspace}
\newcommand{\dsf}{\ensuremath{\mathsf{d}}\xspace}
\newcommand{\esf}{\ensuremath{\mathsf{e}}\xspace}
\newcommand{\fsf}{\ensuremath{\mathsf{f}}\xspace}
\newcommand{\gsf}{\ensuremath{\mathsf{g}}\xspace}
\newcommand{\hsf}{\ensuremath{\mathsf{h}}\xspace}
\newcommand{\isf}{\ensuremath{\mathsf{i}}\xspace}
\newcommand{\jsf}{\ensuremath{\mathsf{j}}\xspace}
\newcommand{\ksf}{\ensuremath{\mathsf{k}}\xspace}
\newcommand{\lsf}{\ensuremath{\mathsf{l}}\xspace}
\newcommand{\msf}{\ensuremath{\mathsf{m}}\xspace}
\newcommand{\nsf}{\ensuremath{\mathsf{n}}\xspace}
\newcommand{\osf}{\ensuremath{\mathsf{o}}\xspace}
\newcommand{\psf}{\ensuremath{\mathsf{p}}\xspace}
\newcommand{\qsf}{\ensuremath{\mathsf{q}}\xspace}
\newcommand{\rsf}{\ensuremath{\mathsf{r}}\xspace}
\newcommand{\ssf}{\ensuremath{\mathsf{s}}\xspace}
\newcommand{\tsf}{\ensuremath{\mathsf{t}}\xspace}
\newcommand{\usf}{\ensuremath{\mathsf{u}}\xspace}
\newcommand{\vsf}{\ensuremath{\mathsf{v}}\xspace}
\newcommand{\wsf}{\ensuremath{\mathsf{w}}\xspace}
\newcommand{\xsf}{\ensuremath{\mathsf{x}}\xspace}
\newcommand{\ysf}{\ensuremath{\mathsf{y}}\xspace}
\newcommand{\zsf}{\ensuremath{\mathsf{z}}\xspace}

%
% for big sqcaps and sqcups
%
%\newfont{\bigmathxx}{cmsy10 scaled 1440}
\newfont{\bigmathxx}{cmsy10 scaled 2200}
\newfont{\smallmathxx}{cmsy10 scaled 720}
\newcommand{\bigsqcap}{\mathop{\mathop{\mbox{\bigmathxx\symbol{117}}}}\limits}
\renewcommand{\bigsqcup}{\mathop{\mathop{\mbox{\bigmathxx\symbol{116}}}}\limits}

\jairheading{23}{2005}{667-726}{07/04}{06/05}
\ShortHeadings{Keys, Nominals and Concrete Domains}
{Lutz, Areces, Horrocks, \& Sattler}

\firstpageno{667}

\begin{document}

\title{Keys, Nominals, and Concrete Domains}

\author{\name Carsten Lutz   
        \email lutz@tcs.inf.tu-dresden.de\\
        \addr Theoretical Computer Science, TU Dresden\\
        D-01062 Dresden, Germany
        \AND
        \name Carlos Areces  
        \email areces@loria.fr\\
        \addr INRIA Lorraine, Nancy\\
        54602 Villers les Nancy Cedex, France
        \AND
        \name Ian Horrocks   
        \email horrocks@cs.man.ac.uk\\
        \addr Department of Computer Science\\
        University of Manchester\\
        Oxford Road, Manchester M13 9PL, UK
        \AND
        \name Ulrike Sattler 
        \email sattler@cs.man.ac.uk\\
        \addr Department of Computer Science\\
        University of Manchester\\
        Oxford Road, Manchester M13 9PL, UK}

\maketitle

\begin{abstract}
\noindent
Many description logics (DLs) combine knowledge representation on an
abstract, logical level with an interface to ``concrete'' domains like
numbers and strings with built-in predicates such as $<$, $+$, and
\mn{prefix\text{-}of}. These hybrid DLs have turned out to be useful
in several application areas, such as reasoning about conceptual
database models.  We propose to further extend such DLs with \emph{key
  constraints} that allow the expression of statements like ``US
citizens are uniquely identified by their social security number''.
Based on this idea, we introduce a number of natural description
logics and perform a detailed analysis of their decidability and
computational complexity.  It turns out that naive extensions with key
constraints easily lead to undecidability, whereas more careful
extensions yield \NExpTime-complete DLs for a variety of useful
concrete domains.
\end{abstract}



\section{Motivation}
\label{sect:intro}

Description logics (DLs) are a family of formalisms that allow the
representation of and reasoning about conceptual knowledge in a
structured and semantically well-understood
manner~\cite{Baader-et-al-01}.  The central entities for
representing such knowledge are \emph{concepts}, which are constructed
from atomic \emph{concept names} (unary predicates) and \emph{role
  names} (binary relations) by means of the concept and role
constructors offered by a particular DL. For example, in the basic
propositionally closed description logic \ALC
\cite{Schmidt-Schauss-Smolka-91}, we can describe a company that has
part-time employees but only full-time managers using the concept
$$
\mn{Company} \sqcap \exists \mn{employee} . \mn{Parttime} \sqcap
\forall \mn{employee} . ( \neg\mn{Manager} \sqcup \neg \mn{Parttime} ).
$$

\noindent
In this example, all words beginning with uppercase letters denote
concept names while \mn{employee} denotes a role name.

Rather than being viewed only as conceptual entities in a knowledge
base, concepts can, more generally, be understood as the central
notion in various kinds of class-centered formalisms. In the last
decade, this observation has given rise to various new and challenging
applications of description logics such as reasoning about database
conceptual models expressed in entity-relationship diagrams or
object-oriented schemas \cite{Calvanese-et-al-98b,Calvanese-et-al-98c}
                                %
and reasoning about ontologies for use in the semantic web
\cite{Baader-et-al-02b,Horrocks-02e,Horrocks-et-al-02b}.  These new
applications have, in turn, stimulated research in description logics
since the expressive power of existing DLs was insufficient for the
new tasks.  One important extension is by providing expressive means
that allow the integration of numbers and other datatypes: suppose,
for example, that we want to extend our earlier descriptions of
companies and employees to include the founding year of a company and
the hiring year of an employee.
                                %
Then, we may want to describe companies that were founded before 1970
and state that the hiring year of employees is not prior to the
founding year of the employing company.  To do this, we obviously need
a way to talk about natural numbers (such as 1970) and comparisons
between natural numbers.

Nowadays, the standard approach to integrate datatypes into
description logics is to extend DLs with \emph{concrete domains}, as
first proposed by Baader and Hanschke \citeyear{Baader-Hanschke-91} and recently surveyed
by Lutz \citeyear{Lutz-02e}.  More precisely, a concrete domain \Dmc consists
of a set (such as the natural numbers) and predicates which are
associated with a \emph{fixed} extension over this set\footnote{This
  fixed extension is why these predicates are often called
  ``built-in''.}  (such as the unary $=_0$, the binary $<$, and the
ternary $+$). The integration of concrete domains into, say, the
description logic \ALC is achieved by adding
%
\begin{enumerate}
  
%\item so-called \emph{abstract features}, which are role names
%  interpreted in functional relations;
      
%\item so-called \emph{concrete features}, which are interpreted in
%  (partial) functions associating values from the concrete domain
%  (e.g., natural numbers) to logical objects;

\item \emph{abstract features}, i.e.\ functional roles;
      
\item \emph{concrete features}, i.e.\
  (partial) functions associating values from the concrete domain
  (e.g., natural numbers) with logical objects;

\item a concrete domain-based concept constructor.

\end{enumerate}

\noindent
The DL obtained by extending \ALC in this way is called \ALCD, where
\Dmc denotes a concrete domain that can be viewed as a parameter to
the logic. For example, using a suitable concrete domain \Dmc we can
describe the constraints formulated above: the concept
$$
\mn{Employee} \sqcap \exists \mn{employer} . \exists
\mn{foundingyear} . {<}_{1970} \sqcap \exists \mn{hiringyear},
(\mn{employer} \; \mn{foundingyear}) . {\geq}
$$
%
describes the set of employees who are employed by a company founded
before 1970 and who have a hiring year not prior to the company's
founding year. In this example, the term ``$\exists \mn{foundingyear}
.  {<}_{1970}$'' is an instance of the concrete domain concept
constructor (not to be confused with the existential value restriction
as in $\exists \mn{employee} .  \mn{Parttime}$), and so is the third
conjunct. While ${<}_{1970}$ is a unary predicate and thus the former
instance only takes one concrete feature \mn{foundingyear} as argument,
the second instance uses the binary predicate ``$\geq$''
requiring two arguments: the concrete feature \mn{hiringyear} and
the sequence of features $(\mn{employer} \; \mn{foundingyear})$
consisting of the abstract feature \mn{employer} and the concrete
feature \mn{foundingyear}.

Concrete domains are rather important in many applications of DLs,
including the two mentioned above:

\begin{itemize}
%-- 
\item The standard way of using description logics for reasoning about
  conceptual database models is to translate a given model into a DL
  representation and then use a DL reasoner such as \FaCT
  \cite{Horrocks-98} or \RACER \cite{Haarslev-Moeller-01b} to compute
  the consequences of the information provided explicitly in the
  model. This includes detecting inconsistencies and inferring
  additional, implicit containments between
  entities/classes~\cite{Calvanese-et-al-98b}.
                                %
Since most databases store ``concrete'' data like numbers and strings,
constraints concerning such data are usually part of the conceptual
model and should thus also be captured by the description logic used
for reasoning.  Indeed, the above example concepts can be viewed as
the DL encoding of constraints from a database about companies and
their employees. As discussed by~\citeA{Lutz-02}, description logics
with concrete domains are well-suited for conceptual modeling
applications involving concrete datatypes.

\item So-called \emph{concrete datatypes} play a prominent role in the
  construction of ontologies~\cite{Horrocks-et-al-02b}. Say, for
  example, that we want to construct an ontology which can be used for
  describing car dealers' web pages and web services. In such an
  ontology, concrete datatypes such as prices, manufacturing years,
  and names of car models will doubtlessly be very important. To
  formulate this ontology using a DL, we need a way to represent these
  concrete datatypes.  Consequently, almost all DLs that have been
  proposed as an ontology language are equipped with some form of
  concrete
  domain~\cite{Horrocks-et-al-01,Horrocks-et-al-02b,Dean-et-al-02}.
  Furthermore, since these ontology languages provide inverse abstract
  roles and functional restrictions, the users and ontology designers
  were quite surprised to find that they do not provide inverse
  concrete functional features---which is due to the fact that such
  features correspond to ``concrete key constraints'', for which no
  reasoning algorithms were known and whose effect on the
  decidability/complexity was not yet investigated.
\end{itemize}

\noindent
% In this paper, we propose to further extend the expressive power of
% description logics with concrete domains in a way that is useful both
% for knowledge representation and the two applications sketched above.
% Let us describe the basic idea --- which is to use concrete features for
% defining ``key constraints''--- using three examples:
In this paper, we propose to further enhance the expressive power of
description logics with concrete domains by extending them with 
``concrete key constraints''.  This extension is useful
both for knowledge representation and for the two applications sketched
above. The following three examples describe the basic idea. 
%
\begin{enumerate}
  
\item Suppose that, in a knowledge representation application, we
  represent nationalities by concept names such as \mn{US} and
  \mn{German} and, for US citizens, we store the social security
  number using a concrete feature \mn{ssn}. Then it would be natural
  to state that US citizens are uniquely identified by their social
  security number, i.e.\ any two distinct instances of 
  $$
  \mn{Human} \sqcap \exists\mn{nationality}.\mn{US}
  $$ 
                                
  \noindent
  must have different values for the \mn{ssn} feature. In our
  extension of DLs with concrete domains, this can be expressed by
  using the \emph{key assertion}\footnote{Readers familiar with the
    relationship between DLs and first order logic will notice that this key
    assertion is equivalent to  
$\forall x_1x_2.( 
     (\bigwedge_{i\in\{1,2\}} 
        (\mn{Human}(x_i) \wedge \exists z.
           (\mn{nationality}(x_i,z) \wedge \mn{US}(z)
           ) 
        ) \wedge \neg(x_1 = x_2)
     ) \Rightarrow \neg
     (\mn{ssn}(x_1)= \mn{ssn}(x_2)))$. }
  $$
  (\mn{ssn} \text{ keyfor }
  \mn{Human} \sqcap \exists\mn{nationality}.\mn{US}).
  $$
 

  
\item Returning to our database about companies and employees, it
  could be useful to equip every employee with (i)~a concrete feature
  \mn{branch} storing the branch-ID in which she is working and (ii)~a
  concrete feature \mn{id} storing her personnel-ID.  It would then be
  natural to enforce that the branch-ID together with the personnel-ID
  uniquely identifies employees, even though personnel-IDs are not
  unique. We can do this by using the \emph{composite} key assertion
  $$ 
  (\mn{branch},\mn{id} \text{ keyfor } \mn{Employee}).
  $$
  
\item In the car dealers' ontology, we may assume that cars as well as
  manufacturers are equipped with identification numbers and that
  every car is uniquely identified by the combination of its own
  identification number and its manufacturers one. To express this, we
  could employ a composite key assertion referring to \emph{sequences}
  of features, in this case $(\mn{manufacturer} \; \mn{id})$: 
  $$
  (\mn{id},(\mn{manufacturer} \; \mn{id}) \text{ keyfor }
  \mn{Car}).
  $$

\end{enumerate}

\noindent
More formally, we propose to extend DLs to provide for concrete
domains with \emph{key boxes}, which are sets of key assertions of
the form
$$
  (u_1,\dots,u_n \text{ keyfor } C),
$$

\noindent
where each $u_i$ is a sequence $f_1 \cdots f_n g$ of abstract features
$f_j$ followed by a single concrete feature $g$, and $C$ is a concept.
As the above examples illustrate, the idea of key constraints is very
natural. Since, moreover, keys play an important role in databases
and, as mentioned above, reasoning about database conceptual models is
an important, challenging application of description logics, several
approaches to extend description logics with keys have already been
investigated~\cite{Borgida-Weddell-97,Calcanese-et-al-00c,Khidzer-et-al-01}.
What distinguishes our approach from existing ones, however, is the
idea of using concrete domains for constructing key constraints, rather
than defining keys on an abstract, logical level.

\medskip

The goal of this paper is \emph{to provide a comprehensive analysis of
  the effects on decidability and computational complexity of adding
  key boxes to description logics with concrete domains}. To this end,
we extend the two description logics \ALCD and \SHOQD with key boxes,
in this way obtaining \ALCKD and \SHOQKD, respectively. While the
basic DL with concrete domains \ALCD has already been discussed above,
\SHOQD was proposed as an ontology language
in~\cite{Horrocks-Sattler-01}. It provides a wealth of expressive
possibilities such as general concept inclusion axioms (GCIs),
transitive roles, role hierarchies, nominals, and qualifying number
restrictions.  Moreover, it offers a restricted variant of the
concrete domain constructor that disallows the use of \emph{sequences}
of features in order to avoid undecidability of reasoning.
%
% CARLOS
%The main outcome of our investigations is that key constraints easily
%induce undecidability and thus have a dramatic impact on the
%decidability and complexity of reasoning, but that decidability
%can be regained by imposing suitable syntactic restrictions
%on  key assertions.
The main outcome of our investigations is that key constraints can
have a dramatic impact on the decidability and complexity of
reasoning: for example, whereas satisfiability of \ALCD-concepts is
known to be \PSpace-complete~\cite{Lutz-02d}, we will show that
satisfiability of \ALCKD-concepts w.r.t.\ key boxes is, in general,
undecidable.  Decidability can be regained if we restrict the concepts
used in key boxes to Boolean combinations of concept names (Boolean
key boxes).  Interestingly, satisfiability of \ALCKD-concepts w.r.t.\ 
Boolean key boxes is still \NExpTime-complete even for very simple
concrete domains. In the case of \SHOQD and \SHOQKD, the leap in
complexity is somewhat less dramatic since \SHOQD-concept
satisfiability is already \ExpTime-complete: again, the addition of
key boxes results in \NExpTime-complete reasoning problems.

It is interesting to note that there exists a close connection between
key assertions and so-called \emph{nominals}, i.e.\ concept names
that can have \emph{at most one} instance, such as \mn{Pope}. Nominals
are a standard means of expressivity in description logics and
sometimes appear in disguise as the ``one-of''
operator~\cite{Borgida-Patel-Schneider-94,Horrocks-et-al-02b}. It is
not hard to see that key boxes can ``simulate'' nominals: if, for
example, we use a concrete domain based on the natural numbers and
providing unary predicates $=_n$ for equality with $n \in
\mathbbm{N}$, then the key assertion $(g \text{ keyfor } \top)$,
where $\top$ stands for logical truth, obviously makes the concept
$\exists g . {=}_n$ behave like a nominal, for each $n \in
\mathbbm{N}$. For this reason, we also consider \ALCOD, the extension
of \ALCD with nominals, and \ALCOKD, the extension of \ALCKD with
nominals.\footnote{Note that the logic \SHOQD already provides for
  nominals.} 
%
% CARLOS
%Our main result concerning nominals is that, although in general being
%of lower expressive power than key boxes, they already make reasoning
%\NExpTime-hard if combined with concrete domains. Thus, there is a
%considerable jump in complexity from the known \PSpace-completeness of
%\ALCD to \ALCOD \cite{Lutz-02d}.  We should like to stress that this
%and the other \NExpTime-hardness results obtained in this paper are in
%accordance with the observation made in~\cite{Lutz-02f}, namely that
%the \PSpace-upper bound for reasoning with \ALCD is not robust w.r.t.\ 
%extensions of the logic: there exist several ``seemingly harmless''
%extensions of \ALCD (for example with acyclic TBoxes and with inverse
%roles) which make the complexity of reasoning leap from
%\PSpace-completeness to \NExpTime-completeness for many natural
%concrete domains.
%
Our main result concerning nominals is that, although in general being
of lower expressive power than key boxes, they already make reasoning
\NExpTime-hard if combined with concrete domains: there exist concrete
domains \Dmc such that \ALCOD-concept satisfiability is
\NExpTime-complete.  We should like to stress that this and the other
\NExpTime-hardness results obtained in this paper are in accordance
with the observation made in~\cite{Lutz-02f} that the \PSpace-upper
bound for reasoning with \ALCD is not robust w.r.t.\ extensions of the
logic: there exist several ``seemingly harmless'' extensions of \ALCD
(for example with acyclic TBoxes and with inverse roles) which make
the complexity of reasoning leap from \PSpace-completeness to
\NExpTime-completeness for many natural concrete domains.


\medskip

The remainder of this paper is organized as follows: in
Section~\ref{sect:dl}, we formally introduce concrete domains, key
boxes, and the DL \ALCOKD together with its fragments \ALCKD and
\ALCOD. Moreover, we define Boolean key boxes, which only allow
Boolean combinations of concept names to appear in key definitions.
Additionally, we introduce some other important properties of key
boxes: \emph{path-free} key boxes prohibit the use of sequences of
features in key assertions; in \emph{unary} key boxes, each key
assertion involves exactly one sequence of features; and
\emph{composite} key boxes are simply non-unary ones.

Section~\ref{lowerbounds} is devoted to establishing lower bounds for
extensions of \ALCD with key boxes or nominals. In
Section~\ref{sect:alckdundec}, we use a reduction of the Post
Correspondence Problem to prove that \ALCKD-concept satisfiability
w.r.t.\ (non-Boolean) key boxes is undecidable for a large class of 
concrete domains.
%if the concrete domain
%\Dmc includes the natural numbers, a unary predicate for equality with
%zero, binary equality and inequality, and a binary incrementation
%predicate. 
We then shift our attention to Boolean key boxes
since, in Section~\ref{reasoningprocedures}, we show that this
restriction restores decidability. In Section~\ref{subsect:redprelim},
we introduce a \NExpTime-complete variant of the domino problem and
three concrete domains that are useful for the reduction of this
problem to concept satisfiability in DLs with Boolean key boxes or
nominals. In Section~\ref{sect:alckdhard}, we use these concrete
domains to prove that \ALCKD-concept satisfiability w.r.t.\ Boolean,
path-free and unary key boxes is \NExpTime-hard for some  natural 
concrete domains.
%if $\Dmc$ includes two unary
%predicates denoting disjoint singleton sets. We then strengthen this
%result to unary key boxes, but, to compensate for the weaker key box
%formalism, we use more expressive concrete domains.  For example, it
%suffices that the concrete domain \Dmc includes the natural numbers, a
%unary predicate $=_n$ for each $n \in \mathbbm{N}$, and ternary
%addition.  
In Section~\ref{sect:alcodhard}, we prove that there exist concrete
domains \Dmc such that \ALCOD-concept satisfiability without reference
to key boxes is already \NExpTime-hard; we show that this is true even
for some concrete domains that are computationally very simple
(\PTime) when considered in isolation.


The purpose of Section~\ref{reasoningprocedures} is to develop
reasoning procedures for description logics with key boxes and to
prove upper complexity bounds matching the \NExpTime lower bounds
established in the previous section. We start in
Section~\ref{sect:alcokdtableau} with a tableau algorithm that decides
\ALCOKD-concept satisfiability w.r.t.\ Boolean key boxes, provided that
the concrete domain \Dmc is \emph{key-admissible}.  Intuitively, a
concrete domain \Dmc is key-admissible if there exists an algorithm
that takes a finite conjunction $c$ of predicates from \Dmc over some
set of variables, decides whether this conjunction is satisfiable and,
if so, chooses a solution of $c$ and
                                %
returns the information on which variables take the same values in it.
We call such an algorithm a \emph{\Dmc-tester}.  We have
chosen a tableau algorithm since this type of reasoning procedure has
the potential to be implemented in efficient reasoners and has been
shown to behave well in
practice~\cite{Horrocks-et-al-00c,Haarslev-Moeller-01b}.
                                %
Our algorithm implies the following upper complexity bound: if \Dmc is
a key-admissible concrete domain for which a non-deterministic
polynomial time \Dmc-tester exists, then \ALCOD-concept
satisfiability w.r.t.\ Boolean key boxes is in \NExpTime.


In Section~\ref{shoqkd}, we devise a tableau algorithm for
\SHOQKD-concept satisfiability w.r.t.\ path-free key boxes which might
involve \emph{non-Boolean} concepts.  
                                %
For the decidability of \ALCOKD, we restricted key boxes to Boolean
ones.  For \SHOQKD, such a restriction is not possible since \SHOQD
provides TBoxes, and we can thus no longer distinguish
between Boolean and non-Boolean concepts. 
                                %
On the other hand, it follows from an undecidability proof by Baader
and Hanschke \citeyear{Baader-Hanschke-92} that \SHOQD is undecidable if
we allow for \emph{sequences} of features in concrete domain
constructors.
                                %
Thus we restrict key assertions analogously to path-free ones, and
show that this yields indeed a decidable logic. Its expressive power
is orthogonal to the one of \ALCOKD, and our previous undecidability
results imply that the combination of \ALCOKD and \SHOQKD is
undecidable.
                                %
As a by-product of the correctness proof of the algorithm, we obtain a
bounded model property for \SHOQKD, which implies that \SHOQKD-concept
satisfiability w.r.t.\ path-free key boxes is in \NExpTime if \Dmc is
a key-admissible concrete domain for which a non-deterministic
polynomial time \Dmc-tester exists.




In Section~\ref{conclusions}, we summarize the  results obtained and give an outlook to
possible future research.

\section{Description Logics with Concrete Domains}
\label{sect:dl}

In the following, we introduce the description logic \ALCOKD. Let us
start by defining concrete domains:

\begin{definition}[Concrete Domain]
  \label{def:concdom}
  A \emph{concrete domain} \Dmc is a pair
  $(\Delta_\Dmc,\Phi_\Dmc)$, where $\Delta_\Dmc$ is a set and $\Phi_\Dmc$ a
  set of \indextext{predicate} names. Each predicate name $P \in \Phi_\Dmc$ is associated
  with an arity $n$ and an $n$-ary predicate $P^\Dmc \subseteq \Delta_\Dmc^n$.
%  Let \V be a set of variables. A \indextext{predicate conjunction} of the form
%  %
%  $$
%  c=\bigwedge_{i < k} (x^{(i)}_0,\dots,x^{(i)}_{n_i}) : P_i,
%  $$
%  %
%  where $P_i$ is an $n_i$-ary predicate for $i < k$ and the $x^{(i)}_j$ are
%  variables from \V, is called \emph{satisfiable} iff there exists a function
%  $\delta$ mapping the variables in $c$ to elements of $\Delta_\Dmc$ such that
%  $(\delta(x^{(i)}_0),\dots,\delta(x^{(i)}_{n_i})) \in P_i^\Dmc$ for each $i <
%  k$. Such a function is called a \emph{solution}\index{solution (for a
%    predicate conjunction)} for~$c$.  A concrete domain
%  \Dmc is called \emph{admissible} iff
%  %
%  \begin{enumerate}
%  \item its set of predicate names is closed under negation and
%  contains a name $\top_\Dmc$ for $\Delta_\Dmc$ and 
%  \item the
%  satisfiability problem for finite conjunctions of predicates is
%  decidable. 
%  \end{enumerate}
%  %
%  By $\overline{P}$, we denote the name for the negation of the predicate
%  $P$, i.e., if the arity of $P$ is $n$, then $\overline{P}^\Dmc=\Delta^n_\Dmc
%  \setminus P^\Dmc$.
\end{definition}

\noindent
Based on concrete domains, we can now define \ALCOKD-concepts and key
boxes.
%
\begin{definition}[\ALCOKD Syntax] \label{def:alcdsyn}
  Let $\NC$, $\NO$, $\NR$, $\NcF$ be pairwise disjoint and countably
  infinite sets of \emph{concept names}, \emph{nominals}, \emph{role
  names}, and \emph{concrete features}.  Furthermore, we assume that
  \NR contains a countably infinite subset \NaF of \emph{abstract
  features}. A \emph{path} $u$ is a composition $f_1 \cdots f_n g$ of
  $n$ abstract features $f_1,\dots,f_n$ ($n \geq 0$) and a concrete
  feature $g$.  Let \Dmc be a concrete domain. The set of
  \ALCOKD-concepts is the smallest set such that
  %
  \begin{itemize}
  
  \item every concept name and every nominal is a concept, and 
    
  \item if $C$ and $D$ are concepts, $R$ is a role name, $g$ is a
    concrete feature, $u_1,\dots,u_n$ are paths, and $P \in \Phi_\Dmc$
    is a predicate of arity $n$, then the following expressions are
    also concepts:
  $$
  \neg C,~C \sqcap D,~C \sqcup D,~\exists R . C,~\forall R .
  C,~\exists u_1,\dots,u_n.P,\text{ and } g{\uparrow}.
  $$
  \end{itemize}
  
\noindent
  A \emph{key assertion} is an expression 
  $$
    (u_1,\dots,u_k \text{ keyfor } C),
  $$
  
\noindent 
  where $u_1,\dots,u_k$ ($k \geq 1$) are paths and $C$ is a concept.
  A finite set of key assertions is called a \emph{key box}.
\end{definition}

\noindent
As usual, we use $\top$ as an abbreviation for an arbitrary propositional
tautology, $\bot$ as an abbreviation for $\neg \top$, $C\rightarrow D$ as
an abbreviation for $\neg C\sqcup D$, and $C\leftrightarrow D$ as
an abbreviation for $(C\rightarrow D) \sqcap (D\rightarrow C)$.
Throughout this paper, we will also consider several fragments of the
description logic \ALCOKD. The DL \ALCOD is obtained from \ALCOKD by
admitting only empty key boxes. In particular, the set of
\ALCOD-concepts is just the set of \ALCOKD-concepts. Furthermore, by
disallowing the use of nominals, we obtain the fragment \ALCD of
\ALCOD and \ALCKD of \ALCOKD.

The description logic \ALCOKD is equipped with a Tarski-style set-theoretic
semantics. Along with the semantics, we introduce the two standard inference
problems: concept satisfiability and concept subsumption.

\begin{definition}[\ALCOKD Semantics]  \label{def:semantics}
  An \emph{interpretation} \Imc is a pair $(\Delta_\Imc, \cdot^\Imc)$,
  where $\Delta_\Imc$ is a non-empty set, called the \emph{domain},
  and $\cdot^\Imc$ is the \emph{interpretation function}.  The
  interpretation function maps
   %
  \begin{itemize}
  \item each concept name $C$ to a subset $C^\Imc$ of $\Delta_\Imc$,
  \item each nominal $N$ to a singleton subset $N^\Imc$ of $\Delta_\Imc$,
  \item each role name $R$ to a subset $R^\Imc$ of $\Delta_\Imc \times
    \Delta_\Imc$,
  \item each abstract feature $f$ to a partial function $f^\Imc$ from
    $\Delta_\Imc$ to $\Delta_\Imc$, and 
  \item each concrete feature $g$ to a partial function $g^\Imc$ from
    $\Delta_\Imc$ to $\Delta_\Dmc$.
  \end{itemize}
  
\noindent
  If $u=f_{1} \cdots f_n g$ is a path, then $u^\Imc(d)$ is defined as
  $g^\Imc(f_{n}^\Imc \cdots (f_1^\Imc(d))\cdots)$. The interpretation function
  is extended to arbitrary concepts as follows:
  %
  \begin{gather*}
    \begin{split}
      (\neg C)^\Imc &:= \Delta_\Imc \setminus C^\Imc \\
      (C \sqcap D)^\Imc &:= C^\Imc \cap D^\Imc \\
      (C \sqcup D)^\Imc &:= C^\Imc \cup D^\Imc \\
      (\exists R . C)^\Imc &:= \{ d \in \Delta_\Imc \mid \text{There
      is }e\in \Delta_\Imc\text{ with }(d,e)\in R^\Imc \text{ and }e\in C^\Imc\}\\
      (\forall R . C)^\Imc &:= \{ d \in \Delta_\Imc \mid \text{For all
      }e\in \Delta_\Imc\text{, if }(d,e)\in R^\Imc \text{, then }e\in C^\Imc\} \\
      (\exists u_1,\dots,u_n.P)^\Imc &:= \{ d \in \Delta_\Imc \mid \exists
      x_1,\dots,x_n \in \Delta_\Dmc: u_i^\Imc(d)=x_i \mbox{ and } (x_1,\dots,x_n) \in P^\Dmc \}
      \\
      (g {\uparrow})^\Imc &:= \{ d \in \Delta_\Imc \mid g^\Imc(d) \text{
        undefined} \}.
    \end{split}
  \end{gather*}
  
\noindent
  Let \Imc be an interpretation. Then \Imc is a \emph{model} of a
  concept $C$ iff $C^\Imc \neq \emptyset$. Moreover, \Imc \emph{satisfies} a
  key assertion $(u_1,\dots,u_n \mbox{ keyfor } C)$ if, for any
  $a,b \in C^\Imc$,
  %
  \begin{center}
%      if,  for all $1 \leq i \leq n$,   $u_i^\Imc(a)=u_i^\Imc(b)$, then 
%    $a=b$.
$u_1^\Imc(a)=u_1^\Imc(b)$, \ldots, $u_n^\Imc(a)=u_n^\Imc(b)$ implies that
    $a=b$.
  \end{center}
  %
\noindent
  \Imc is a \emph{model} of a key box $\Kmc$ iff \Imc satisfies all key assertions
  in $\Kmc$. 
  %
  A concept $C$ is \emph{satisfiable w.r.t.\ a key box $\Kmc$} iff $C$
  and $\Kmc$ have a common model. $C$ is \emph{subsumed by} a concept $D$
  \emph{w.r.t.\ a key box $\Kmc$} (written $C \sqsubseteq_\Kmc D$) iff $C^\Imc
  \subseteq D^\Imc$ for all models \Imc of $\Kmc$.
\end{definition}

\noindent
It is well-known that, in description logics providing for all Boolean
operators, subsumption can be reduced to (un)satisfiability and vice
versa: $C \sqsubseteq_\Kmc D$ iff $C \sqcap \neg D$ is unsatisfiable
w.r.t.\ $\Kmc$ and $C$ is satisfiable w.r.t.\ $\Kmc$ iff $C
\not\sqsubseteq_\Kmc \bot$. This allows us to concentrate on concept
satisfiability when devising complexity bounds for reasoning with
description logics: lower and upper complexity bounds for
  concept satisfiability imply corresponding bounds for concept
  subsumption---only for the complementary complexity class.

If decision procedures for description logics with concrete domains
are to be devised without committing to a \emph{particular} concrete
domain, then a well-defined interface between the decision procedure
and a concrete domain reasoner is needed. Usually, this interface is
based on the assumption that the concrete domain is
\emph{admissible}~\cite{Baader-Hanschke-91,Lutz-Diss,Lutz-02e}:
%
\begin{definition}[\Dmc-conjunction, Admissibility]\label{def:adm}
  Let \Dmc be a concrete domain and \V a set of variables. A
  \emph{\Dmc-conjunction} is a (finite) predicate conjunction of the
  form
  $$
  c=\bigwedge_{i < k} (x^{(i)}_0,\dots,x^{(i)}_{n_i}) : P_i,
  $$
  
\noindent
  where $P_i$ is an $n_i$-ary predicate for $i < k$ and the
  $x^{(i)}_j$ are variables from \V. A \Dmc-conjunction $c$ is
  \emph{satisfiable} iff there exists a function $\delta$ mapping the
  variables in $c$ to elements of $\Delta_\Dmc$ such that
  $(\delta(x^{(i)}_0),\dots,\delta(x^{(i)}_{n_i})) \in P_i^\Dmc$ for
  each $i < k$. Such a function is called a
  \emph{solution}\index{solution (for a predicate conjunction)}
  for~$c$.  We say that the concrete domain \Dmc is \emph{admissible}
  iff
  %
  \begin{enumerate}

  \item $\Phi_\Dmc$ contains a unary predicate $\top_\Dmc$ such that $\top_\Dmc^\Dmc = \Delta_\Dmc$;
    
  \item $\Phi_\Dmc$ is closed under negation, i.e., for each $n$-ary
    predicate $P \in \Phi_\Dmc$, there is a  predicate
    $\overline{P} \in \Phi_\Dmc$ of arity $n$ such that
    $\overline{P}^\Dmc=\Delta^n_\Dmc \setminus P^\Dmc$;

  \item  satisfiability of \Dmc-conjunctions is decidable.

  \end{enumerate}
  
\noindent
  We refer to the satisfiability of \Dmc-conjunctions as
  \emph{\Dmc-satisfiability}.
\end{definition}

\noindent
As we shall see, it sometimes makes a considerable difference w.r.t.\ 
complexity and decidability to restrict key boxes in various ways, for
example to disallow paths of length greater than one.  Therefore, we
introduce some useful notions.
%
\begin{definition}[Boolean, Path-free, Simple]
  A key box \Kmc is called 
  %
  \begin{itemize}
  \item \emph{Boolean} if all concepts appearing in (key assertions
    in) \Kmc are Boolean combinations of concept names;

  \item \emph{path-free} if, for all key assertions $(u_1,\dots,u_n \text{ keyfor } C)$ in \Kmc, $u_1,\dots,u_n \in \NcF$;

  
  \item \emph{simple} if it is both path-free and Boolean;
    
  \item \emph{unary} if all key assertions in \Kmc are \emph{unary
      key assertions}, i.e.\ of the form $(u \text{ keyfor } C)$.
  \end{itemize}
  
\noindent
  A concept $C$ is called \emph{path-free} if, in all its subconcepts
  of the form $\exists u_1,\dots,u_n.P$, $u_1,\dots,u_n$ are concrete
  features.
\end{definition}

\noindent
To emphasize that a key box might \emph{not} necessarily be Boolean
or path-free, we sometimes call such a key box \emph{general}. Similarly,
to emphasize that a key box is not necessarily a unary key box, we sometimes
call such a key box \emph{composite}.

\section{Lower Bounds}\label{lowerbounds}

In this section, we prove lower complexity bounds for description
logics with concrete domains and key boxes and/or nominals. In
Section~\ref{sect:alckdundec}, we start by showing that the
satisfiability of \ALCKD-concepts w.r.t.\ (general) key boxes is
undecidable for many interesting concrete domains. The discouraging
picture painted by this result is mitigated by the fact that, in
Section~\ref{sect:alcokdtableau}, we shall prove that the restriction
to Boolean key boxes restores decidability. It is thus interesting to
look for lower complexity bounds that apply under this restriction.
In preparation for this, we introduce in
Section~\ref{subsect:redprelim} a \NExpTime-complete variant of the
domino problem and three concrete domains that are well-suited for
reductions of this problem.

In Section~\ref{sect:alckdhard}, we then prove that satisfiability of
path-free \ALCKD-concepts w.r.t.\ simple key boxes is \NExpTime-hard
for a large class of concrete domains \Dmc and that, for many concrete
domains, this holds even if we restrict key boxes to unary ones.
Finally, we consider the description logic \ALCOD in
Section~\ref{sect:alcodhard} and identify several concrete domains
such that \ALCOD-concept satisfiability (without key boxes!) is
\NExpTime-hard. As we already mentioned, key boxes and nominals are closely
related: key boxes can express nominals, but are in general more powerful.

\subsection{Undecidability of \ALCKD with General Key Boxes}
\label{sect:alckdundec}

We prove that satisfiability of \ALCKD-concepts w.r.t.\ key boxes is
undecidable for a large class of concrete domains if we allow complex
\ALCKD-concepts to occur in key assertions. The proof is by a
reduction of the well-known undecidable Post Correspondence
Problem~\cite{Post-46,Hopcroft-Ullman-79}.
%
\begin{definition}[PCP]
  An \emph{instance} $P$ of the \emph{Post Correspondence Problem}
  (PCP) is given by a finite, non-empty list
  $(\ell_1,r_1),\dots,(\ell_k,r_k)$ of pairs of words over some
  alphabet~$\Sigma$.  A sequence of integers $i_1,\dots,i_m$, with $m
  \geq 1$, is called a \index{PCP-solution}\emph{solution} for $P$ if
  $\ell_{i_1} \cdots \ell_{i_m} = r_{i_1} \cdots r_{i_m}$.  The PCP is
  to decide whether a given instance $P$ has a solution.
\end{definition}

\noindent
For reducing the PCP to the satisfiability of our DLs, we need an
appropriate concrete domain. It is obviously natural to use a concrete
domain based on words and concatenation. We will later see that the
results obtained for this concrete domain carry over to other concrete
domains based on numbers and arithmetics. The following concrete
domain was introduced by Lutz~\citeyear{Lutz-02f}. Its definition presupposes
a fixed alphabet $\Sigma$ that is at least binary.
%
\begin{definition}[Concrete domain \Wsf]
The concrete domain $\Wsf$ is
  defined by setting $\Delta_{\Wsf} := \Sigma^*$ and defining $\Phi_{\Wsf}$ as
  the smallest set containing the following predicates:
  %
  \begin{itemize}
  \item unary predicates $\mn{word}$ and $\mn{nword}$ with
    $\mn{word}^\Wsf=\Delta_\Wsf$ and $\mn{nword}^\Wsf=\emptyset$,
  \item unary predicates $=_\epsilon$ and $\neq_\epsilon$ with
    ${=_\epsilon^\Wsf} = {\{ \epsilon \}} $ and ${\neq_\epsilon^\Wsf}
    = {\Sigma^+}$, 
  \item a binary equality predicate $=$ and a binary inequality predicate
    $\neq$ with the obvious interpretation, and
  \item for each $w \in \Sigma^+$, two binary
    predicates $\mn{conc}_w$ and $\mn{nconc}_w$ with
    $$
    \mn{conc}_w^\Wsf = \{ (u,v) \mid v=uw \}
    \text{ and }
    \mn{nconc}_w^\Wsf = \{ (u,v) \mid v \neq uw \}.
    $$
  \end{itemize}
\end{definition}

\noindent
It is readily checked that \Wsf satisfies properties~1 and~2 of
admissibility (see Definition~\ref{def:adm}).  Moreover,
\Wsf-satisfiability is decidable:

%In~\cite{Lutz-02f}, the complexity of \Wsf-satisfiability is
%investigated.
%
\begin{theorem}[\citeR{Lutz-02f}]
\label{wsat}
  \Wsf-satisfiability is in \PTime.
\end{theorem}

\noindent
Thus, \Wsf is admissible and even of low complexity. This is important
since our aim is to demonstrate that the undecidability of
$\ALCK({\Wsf})$-concept satisfiability is due to the presence of keys,
and not due to the high complexity of ${\Wsf}$-satisfiability.

We can now discuss the reduction of the PCP. A given instance
$(\ell_1,r_1),\dots,(\ell_k,r_k)$ is translated into an \ALCKD-concept
$C_P$ and key box $\Kmc_P$ as defined in
Figure~\ref{fig:alckdundecred} such that $P$ has a solution iff $C_P$
is unsatisfiable w.r.t.~$\Kmc_P$.
%
\psfull
\begin{figure}[t!]
  \begin{boxedminipage}[t]{\textwidth}
  \begin{center}
  \begin{gather*}
    \begin{split}
     \mn{Step} := \; &\bigsqcap_{1 \leq i \leq k} \exists f_i . (\neg A \sqcap \exists g . {=}_\epsilon \sqcap \exists \ell,r . {\neq}) \\[1mm]
      & \sqcap \; \bigsqcap_{1 \leq i \leq k} ( \exists \ell, f_i \ell . \mn{conc}_{\ell_i} \sqcap \exists r, f_i r . \mn{conc}_{r_i})
      %
      \\[2mm]
      %
      C_P := \; &\exists \ell . {=}_\epsilon \sqcap \exists r . {=}_\epsilon \\
      & \sqcap \; \exists R . ( A \sqcap \exists g . {=}_\epsilon \sqcap \neg \mn{Step}) \\
      & \sqcap \mn{Step}
      \\[2mm]
      %
      \Kmc_P := \; &\{ g \text{ keyfor } \neg \mn{Step} \}
      \\[4mm]
    \end{split}      
  \end{gather*}
  \end{center}
  \end{boxedminipage}
  \caption{The $\ALCK(\Wsf)$ reduction concept $C_P$ and key box $\Kmc_P$.}
  \label{fig:alckdundecred}
\end{figure}
\psdraft
%
The idea behind the reduction is that a common model of $C_P$ and
$\Kmc_P$ encodes all \emph{potential solutions} for $P$ (i.e.,
sequences $i_1,\ldots,i_n$ of integers $i_j$ between 1 and $k$) and
makes sure that none of them is in fact a solution.
                                %
In Figure~\ref{fig:alckdundecred}, $f_1,\dots,f_k$ denote abstract
features while $g$, $\ell$, and $r$ denote concrete features. The
definition of the concept $\mn{Step}$ just serves as an abbreviation
and should not be confused with so-called TBoxes (see
Section~\ref{shoqkd} for the definition of TBoxes).
%
\psfull
\begin{figure}[tb]
  \begin{center}
    \framebox[1\textwidth]{\input{gci.pdftex_t}}
  \end{center}
  %
    \caption{An example model of $C_P$ and $\Kmc_P$.}
    \label{fig:modelgci}
\end{figure}
\psdraft
%
Models of $C_P$ and $\Kmc_P$, such as the one displayed in
Figure~\ref{fig:modelgci}, have the form of an infinite $k$-ary tree
whose root is connected to an ``extra node'' $x$ via the role $R$.
Intuitively, each node of the tree represents one partial solution
$i_1,\dots,i_n$, its $\ell$-successor represents the corresponding
left concatenation $\ell_{i_1} \cdots \ell_{i_n}$, and its
$r$-successor the corresponding right concatenation $r_{i_1} \cdots
r_{i_n}$.

To enforce the existence of the infinite tree, we employ the key box
$\Kmc_P$: consider for example the root node's $f_1$-successor in
Figure~\ref{fig:modelgci}---let us call this node $y$. Due to Line~3
of $C_P$ and Line~1 of \mn{Step}, we have $y \in (\exists g .
{=}_\epsilon)^\Imc$. Due to Line~2 of $C_P$, we also have $x \in
(\exists g .  {=}_\epsilon)^\Imc$ and $x \in (\neg \mn{Step})^\Imc$,
where $x$ is the ``extra node'' mentioned above. In view of the key
box $\Kmc_P$, this implies that either (i)~$x = y$ or (ii)~$y \in
\mn{Step}^\Imc$. It is easy to see that (i) is impossible since Line~2
of $C_P$ and Line~1 of \mn{Step} imply that $x \in A^\Imc$ and $y \in
(\neg A)^\Imc$. Hence $y \in \mn{Step}^\Imc$ and, by Line~2 of
\mn{Step}, $y$ has the appropriate $f_i$-successors for $1 \leq i \leq
n$. In the same way, the construction of the tree can be continued ad
infinitum.  The second line in the definition of $\mn{Step}$ enforces
that $\ell^\Imc (z) = \ell_{i_1}\cdots \ell_{i_n}$ and $r^\Imc (z) =
r_{i_1}\cdots r_{i_n}$ for $z$ an $f_{i_1}\cdots f_{i_n}$-successor of
the root node.  Finally, the concept $\exists \ell,r.{\neq}$ in Line~1
of $\mn{Step}$ implies that $\ell^\Imc(z) \neq r^\Imc(z)$ holds at all
nodes $z$ of the tree (except for the root), which implies that no
potential solution is a solution.

Since the size of $C_P$ and $\Kmc_P$ is clearly polynomial in $k$ and
the key box $\Kmc_P$ is a unary key box, we obtain the following
proposition.
%
\begin{proposition}
\label{prop:undec}
The satisfiability of $\ALCK(\Wsf)$-concepts w.r.t.\ (non-Boolean)
path-free unary key boxes is undecidable.
\end{proposition}

\noindent
To emphasize that this undecidability result was obtained using a
very simple concrete domain, let us combine Theorem~\ref{wsat} with
Proposition~\ref{prop:undec}.
%
\begin{theorem}
  There exists a concrete domain \Dmc such that \Dmc-satisfiability is
  in \PTime and satisfiability of $\ALCKD$-concepts w.r.t.\ 
  (non-Boolean) path-free unary key boxes is undecidable.
\end{theorem}

\noindent
At first sight, the concrete domain \Wsf might look artificial and one
may question the relevance of lower bounds that have been obtained
using \Wsf. However, it is straightforward to encode words as natural
numbers and to define concatenation of words as rather simple
operations on the natural numbers~\cite{Baader-Hanschke-92}: a word $w
\neq \epsilon$ over the alphabet $\Sigma$ of cardinality $\#\Sigma$
can be interpreted as a number written at base $\#\Sigma +1 $ in which
the symbol that is the ``0 digit'' does not occur. Hence, we can use
the corresponding natural number (e.g., in base 10) to represent a word
$w$, and the number 0 to represent the empty word. The concatenation
of two words $v$ and $w$ can then be expressed as $vw = v \cdot
(\#\Sigma+1)^{|w|} +w$, where $|w|$ denotes the length of the word
$w$. Moreover, exponentiation can be expressed as multiple
multiplications, multiplication as multiple additions, and addition as
multiple incrementation: this is shown in Section 5.6 of
\cite{Lutz-02f} for the case of \ALCD extended with TBoxes (c.f.\ 
Section~\ref{shoqkd}) and can easily be adapted to \ALCD with
non-Boolean key boxes.  This observation gives rise to the following
theorem:
%
\begin{theorem}
  Let \Dmc be a concrete domain such that $\mathbbm{N} \subseteq
  \Delta_\Dmc$, $\Phi_\Dmc$ contains a unary predicate ${=}_0$ with
  $({=}_0)^\Dmc=\{0\}$, binary equality and inequality predicates, and
  a binary predicate $\mn{incr}$ with $\mn{incr}^\Dmc \cap \{ (n,x)
  \mid n \in \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{
  (k,k+1) \mid k \in \mathbbm{N}\}$. Then satisfiability of
  \ALCKD-concepts w.r.t.\ (non-Boolean) path-free unary key boxes is
  undecidable.
\end{theorem}

\subsection{Domino Problems and Concrete Domains}
\label{subsect:redprelim}

In this section, we introduce a \NExpTime-complete variant of the
well-known, undecidable domino problem~\cite{Berger-66,Knuth-68}, and
then define three concrete domains $\Dsf_1$, $\Dsf_2$, and~$\Dsf_3$.
These concrete domains will be used in Sections~\ref{sect:alckdhard}
and~\ref{sect:alcodhard} to establish lower bounds for reasoning with
\ALCKD and Boolean key boxes, and for reasoning with \ALCOD.

In general, a domino problem is given by a finite set of \emph{tile
  types}.  Intuitively, all tile types are of the same size, each type
having a square shape and colored edges.  An unlimited number of tiles
of each type is available.  In the \NExpTime-hard variant of the
domino problem that we use, the task is to tile a $2^{n+1} \times
2^{n+1}$-torus (i.e., a $2^{n+1} \times 2^{n+1}$-rectangle whose
borders are ``glued'' together) where neighboring edges have the same
color.
%
\begin{definition}[Domino System]\label{domsys}
  A \emph{domino system} $\Dmf$ is a triple $(T,H,V)$, where $T
  \subsetneq \mathbbm{N}$ is a finite set of \emph{tile types} and $H,V
  \subseteq T \times T$ represent the horizontal and vertical matching
  conditions.  Let \Dmf be a domino system and $a = a_0,\dots,a_{n-1}$
  an \emph{initial condition}, i.e.\ an $n$-tuple of tiles.  A mapping
  $\tau: \{0,\dots,2^{n+1}-1\} \times \{0,\dots,2^{n+1}-1\} \to T$ is a
  \emph{solution} for \Dmf and $a$ iff, for all $x,y < 2^{n+1}$, the
  following holds:
  %
  \begin{itemize}
  \item if $\tau(x,y) = t$ and $\tau(x \oplus_{2^{n+1}} 1,y) =
    t'$, then $(t,t') \in H$
  \item if $\tau(x,y) = t$ and $\tau(x,y \oplus_{2^{n+1}} 1) =
    t'$, then $(t,t') \in V$
  \item $\tau(i,0) = a_i$ for $i < n$.
  \end{itemize}
  
\noindent
  where $\oplus_i$ denotes addition modulo $i$.
\end{definition}

\noindent
It follows from results in~\cite{Boerger-et-al-97} that the above
variant of the domino problem is \NExpTime-complete.

We define the concrete domain $\Dsf_1$ to be used in the
reduction of the \NExpTime-complete domino problem to
$\ALCK(\Dsf_1)$-concept satisfiability w.r.t.\ Boolean key boxes.

\begin{definition}[Concrete Domain $\Dsf_1$]
  The concrete domain $\Dsf_1$ is defined by setting $\Delta_{\Dsf_1}
  := \{ 0,1 \}$ and $\Phi_{\Dsf_1}$ to the (smallest) set containing
  the following predicates:
                                %
  \begin{itemize}
  \item unary predicates $\top_{\Dsf_1}$ with
    $(\top_{\Dsf_1})^{\Dsf_1} = \Delta_{\Dsf_1}$ and 
    $\bot_{\Dsf_1}$ with $(\bot_{\Dsf_1})^{\Dsf_1} = \emptyset$;
    
  \item unary predicates ${=}_0$ and ${=}_1$ with
    $({=}_i)^{\Dsf_1} = \{ i \}$, $i \in \{0,1\}$.

  \end{itemize}
\end{definition}

\noindent
The second concrete domain $\Dsf_2$ will be used for a reduction of
the \NExpTime-complete domino problem to $\ALCK(\Dsf_2)$-concept
satisfiability w.r.t.\ Boolean \emph{unary} key boxes.  For this
reduction we need to ``store'' vectors of bits in single concrete
domain elements.
%
\begin{definition}[Concrete Domain $\Dsf_2$]
  For every $n \in \mathbbm{N}$, a function $v:\{0,\dots,n-1\}
  \rightarrow \{0,1\}$ is called a \emph{bit vector} of dimension
  $n$. We use $\mn{BV}_n$ to denote the set of all bit vectors of
  dimension~$n$.  The concrete domain $\Dsf_2$ is defined by setting
  $\Delta_{\Dsf_2} := \bigcup_{i>0} \mn{BV}_i$ and
  $\Phi_{\Dsf_2}$ to the (smallest) set containing the following
  predicates:
                                %
  \begin{itemize}
  \item unary predicates $\top_{\Dsf_2}$ with
    $(\top_{\Dsf_2})^{\Dsf_2} = \Delta_{\Dsf_2}$ and 
    $\bot_{\Dsf_2}$ with $(\bot_{\Dsf_2})^{\Dsf_2} = \emptyset$;

  \item for every $k,i \in \mathbbm{N}$ with $i < k$, unary
    predicates $\mn{bit0}^i_k$ and $\mn{bit1}^i_k$ with
  $$
    (\mn{bit}n^i_k)^{\Dsf_2} = \{ v \in \Delta_{\Dsf_2} \mid v \in \mn{BV}_{k} \text{ and } v(i)=n \},
  $$
%  
%\noindent
  and unary predicates $\overline{\mn{bit0}^i_k}$ and
  $\overline{\mn{bit1}^i_k}$ with
  $(\overline{\mn{bit}n^i_k})^{\Dsf_2} = \Delta_{\Dsf_2} \setminus
  (\mn{bit}n^i_k)^{\Dsf_2}$.

  \end{itemize}
\end{definition}

\noindent
The last concrete domain $\Dsf_3$ is used in the reduction of the
\NExpTime-complete domino problem to $\ALCO(\Dsf_3)$-concept
satisfiability. In this reduction, the concrete domain $\Dsf_3$
contains two kinds of elements: firstly, there are elements
of~$\Delta_{\Dsf_3}$ that can represent the \emph{whole} $2^{n+1}
\times 2^{n+1}$-torus, so-called \emph{domino arrays}.  Secondly,
there are elements of $\Delta_{\Dsf_3}$ that represent positions in
the torus. For technical reasons to be discussed later, these elements
are vectors of natural numbers rather than bit vectors, and in the
following we shall just call them \emph{vectors}. A domino array is
then a function mapping each pair of vectors (of certain length) to a
natural number which represents a tile type.
%
\begin{definition}[Concrete Domain $\Dsf_3$]
  For every $k \in \mathbbm{N}$, a function $v:\{0,\dots,k-1\}
  \rightarrow \mathbbm{N}$ is called a \emph{vector} of dimension $k$.
  We use $\mn{VE}_k$ to denote the set of all vectors of
  dimension~$k$. For every $k \in \mathbbm{N}$, a function \mbox{$k:
  \mn{VE}_{k} \times \mn{VE}_{k} \rightarrow \mathbbm{N}$} is called a
  \emph{domino array} of dimension $k$. We use $\mn{DA}_{k}$ to denote
  the set of all domino arrays of dimension~$k$.  The concrete domain
  $\Dsf_3$ is defined by setting $\Delta_{\Dsf_3} := \bigcup_{i>0}
  \mn{VE}_i \cup \bigcup_{i>0} \mn{DA}_{i}$ and $\Phi_{\Dsf_3}$ to the
  (smallest) set containing the following predicates:
  %
  \begin{itemize}
    
  \item unary predicates $\top_{\Dsf_3}$ with
    $(\top_{\Dsf_3})^{\Dsf_3} = \Delta_{\Dsf_3}$ and $\bot_{\Dsf_3}$
    with $(\bot_{\Dsf_3})^{\Dsf_3} = \emptyset$;
    
  \item for every $k,i \in \mathbbm{N}$ with $i < k$, unary predicates
    $\mn{pos0}^i_k$ and $\mn{pos1}^i_k$ with
  $$
    (\mn{pos}n^i_k)^{\Dsf_3} = \{ v \in \Delta_{\Dsf_3} \mid v \in
    \mn{VE}_{k} \text{ and } v(i)=n \}
  $$
                                
\noindent
  and unary predicates $\overline{\mn{pos0}^i_k}$ and
  $\overline{\mn{pos1}^i_k}$ with $(\overline{\mn{pos}n^i_k})^{\Dsf_3}
  = \Delta_{\Dsf_3} \setminus (\mn{pos}n^i_k)^{\Dsf_3}$;

  \item for every $k,i \in \mathbbm{N}$, a predicate $\mn{tile}^i_k$ of
   arity 3 with 
    $$
    (\mn{tile}^i_k)^{\Dsf_3} = \{
    (v_x,v_y,d) \mid v_x,v_y \in \mn{VE}_{k},\; d \in \mn{DA}_{k},
    \text{ and } d(v_x,v_y)=i \}
    $$
    
\noindent
    and a predicate $\overline{\mn{tile}^i_k}$ of arity 3 with
    $(\overline{\mn{tile}^i_k})^{\Dsf_3} = (\Delta_{\Dsf_3})^{3} \setminus
    (\mn{tile}^i_k)^{\Dsf_3}$.
    
  \end{itemize}
\end{definition}

\noindent
The reason for using vectors of natural numbers rather than bit
vectors in the definition of $\Dsf_3$ is that we want
$\Dsf_3$-satisfiability to be of low complexity, preferably in \PTime:
consider the $\Dsf_3$-conjunction
$$
\begin{array}{l}
  \mn{pos0}^0_2(x) \wedge \mn{pos0}^0_2(y) \wedge \mn{pos0}^0_2(z)
  \; \wedge \\[1mm]
  \mn{tile}^7_2(x,v,d) \wedge  \mn{tile}^8_2(y,v,d) \wedge  \mn{tile}^9_2(z,v,d).
\end{array}
$$

\noindent
If we use bit vectors rather than vectors of natural numbers, then the
upper line enforces that at least two out of the three variables $x$,
$y$, and $z$ must take the same value. Since the value of $v$ is
fixed, the lower line makes the conjunction unsatisfiable: it tries to
assign the three different values 7, 8, 9 to two different positions in
the domino array.  It seems unlikely that this kind of inconsistency
can be detected in polynomial time.  This problem is circumvented
by using vectors of natural numbers in the definition of $\Dsf_3$ (but
enforcing them to be bit vectors in the reduction): in this case, the
above conjunction is clearly satisfiable.

\begin{proposition}\label{d1compl}\label{d2compl}\label{d3compl}
  For each $i\in \{1,2,3\}$, the concrete domain $\Dsf_i$ is
  admissible and satisfiability of $\Dsf_i$-conjunctions is in \PTime.
\end{proposition}
                                %
\noindent
For $\Dsf_1$, this is trivial. For $\Dsf_2$, a proof can be found in
Appendix~\ref{applower}. And for $\Dsf_3$, a proof can
be found in \cite{Areces-et-al-02}.

\subsection{\NExpTime-hardness of \ALCKD with Boolean Key Boxes}
\label{sect:alckdhard}

In this section, we prove two \NExpTime-lower bounds for
\ALCKD-concept satisfiability w.r.t.\ Boolean key boxes by reducing
the \NExpTime-complete domino problem introduced in the previous
section.  The first reduction uses the very simple concrete domain
$\Dsf_1$, but depends on composite key assertions. The second
reduction uses the slightly more complex concrete domain $\Dsf_2$, but
only needs unary key assertions. As we will see, the two reductions
yield different, incomparable results.

\psfull
\begin{figure}[t!]
  \begin{boxedminipage}[t]{\textwidth}
  \begin{center}
  \begin{gather*}
    \begin{split}
      \mn{TreeX} &:= \exists R . X_0 \sqcap
      \exists R . \neg X_0 
      \sqcap \bigsqcap_{i=1..n}\forall R^{i}.(\mn{DistX}_{i-1} \sqcap
      \exists R. X_{i} \sqcap \exists R . \neg X_{i}) 
      \\
      \mn{TreeY} &:= \mn{DistX}_n \sqcap \exists R . Y_0 \sqcap 
      \exists R . \neg Y_0 
      \sqcap \\
      &\phantom{Cc} \bigsqcap_{i=1..n} \forall R^{i}.(\mn{DistY}_{i-1} \sqcap \mn{DistX}_n\sqcap
      \exists R. Y_{i} \sqcap \exists R . \neg Y_{i}) 
      \\
      \mn{DistX}_k &:= \bigsqcap_{i=0..k}((X_i \to \forall R . X_i) \sqcap
      (\neg X_i \to \forall R . \neg X_i)) 
      \\
      \mn{DistY}_k &:= \bigsqcap_{i=0..k}((Y_i \to \forall R . Y_i) \sqcap
      (\neg Y_i \to \forall R . \neg Y_i)) 
      \\
      \mn{TransXPos} &:=  \bigsqcap_{i=0..n} ( X_i
      \rightarrow \exists \mn{xpos}_i . =_{1} ) \sqcap ( \neg X_i \rightarrow
      \exists \mn{xpos}_i . =_0 ) 
      \\
      \mn{TransYPos} &:=  \bigsqcap_{i=0..n} ( Y_i
      \rightarrow \exists \mn{ypos}_i . =_{1} ) \sqcap ( \neg Y_i \rightarrow
      \exists \mn{ypos}_i . =_0 ) 
      \\
      \mn{Succs} &:= \exists R_x . ( \mn{TransXPos} \sqcap \mn{TransYPos} ) \sqcap \exists R_y . ( \mn{TransXPos} \sqcap \mn{TransYPos} ) 
      \\
      \mn{XSuccOk} &:= \bigsqcap_{i=0..n} \big ( 
        ( Y_i \rightarrow \forall R_x . Y_i ) \sqcap
        ( \neg Y_i \rightarrow \forall R_x . \neg Y_i ) \big ) \\
      &\phantom{Cc} \bigsqcap_{k=0..n} \big ( \bigsqcap_{j=0..k} X_j \big )
       \rightarrow \big ( (X_k \rightarrow \forall R_x.\neg X_k ) \sqcap 
        (\neg X_k \rightarrow \forall R_x. X_k ) \big ) \\
      &\phantom{Cc} \bigsqcap_{k=0..n} \big ( \bigsqcup_{j=0..k} \neg X_j \big )
       \rightarrow \big ( (X_k \rightarrow \forall R_x. X_k ) \sqcap 
        (\neg X_k \rightarrow \forall R_x. \neg X_k ) \big )
      \\
      \mn{YSuccOk} &:= \bigsqcap_{i=0..n} \big ( 
        ( X_i \rightarrow \forall R_y . X_i ) \sqcap
        ( \neg X_i \rightarrow \forall R_y . \neg X_i ) \big ) \\
      &\phantom{Cc} \bigsqcap_{k=0..n} \big ( \bigsqcap_{j=0..k} Y_j \big )
       \rightarrow \big ( (Y_k \rightarrow \forall R_y.\neg Y_k ) \sqcap 
        (\neg Y_k \rightarrow \forall R_y. Y_k ) \big ) \\
      &\phantom{Cc} \bigsqcap_{k=0..n} \big ( \bigsqcup_{j=0..k} \neg Y_j \big )
       \rightarrow \big ( (Y_k \rightarrow \forall R_y. Y_k ) \sqcap 
        (\neg Y_k \rightarrow \forall R_y. \neg Y_k ) \big )
      \\
      \mn{Label} &:= \bigsqcup_{i \in T} D_i \; \sqcap \bigsqcap_{i,j \in T, i \neq j} \neg (D_i \sqcap D_j)
      \\
      \mn{CheckMatch} &:= \bigsqcup_{(i,j) \in H} (D_i \sqcap \forall R_x . D_j) \; \sqcap \bigsqcup_{(i,j) \in V} (D_i \sqcap \forall R_y . D_j)
      \\
      \mn{Init} &:= \bigsqcap_{i=0..n-1}  \Big ( \big ( 
        \bigsqcap_{j=0..n, \mn{bit}_j(i) = 0} \neg X_j \; \sqcap
        \bigsqcap_{j=0..n, \mn{bit}_j(i) = 1} X_j \; \sqcap \bigsqcap_{j=0..n} \neg Y_j \big ) \rightarrow D_{a_i} \Big )
      \\
%      \mn{Init} &:= \bigsqcap_{i=0..n-1}  \Big ( \big ( 
%        \bigsqcap_{j=0..n} \exists \mn{xpos}_j . {=}_{\mn{bit}_j(i)} \; \sqcap
%        \bigsqcap_{j=0..n} \exists \mn{ypos}_j . {=}_0 \big ) \rightarrow D_{a_i} \Big )
%      \\
      C_{\Dmf,a} &:= \mn{TreeX} \sqcap \forall R^{n+1} . \mn{TreeY}  \\
      &\phantom{Cc} \sqcap \forall R^{2(n+1)} . ( \mn{TransXPos} \sqcap \mn{TransYPos} \sqcap \mn{Succs} \sqcap \mn{XSuccOk} \sqcap \mn{YSuccOk}) \\
      &\phantom{Cc} \sqcap \forall R^{2(n+1)} . (\mn{Label} \sqcap \mn{CheckMatch} \sqcap \mn{Init})
    \end{split}      
  \end{gather*}
  \end{center}
  \end{boxedminipage}
  \caption{The $\ALCK(\Dsf_1)$ reduction concept $C_{\Dmf,a}$.}
  \label{fig:alckdred}
\end{figure}
\psdraft
%
We first reduce the \NExpTime-complete domino problem to
$\ALCK(\Dsf_1)$-concept satisfiability w.r.t.\ Boolean composite key
boxes. Each domino system $\Dmf=(T,H,V)$ with initial condition
$a=a_0,\dots,a_{n-1}$ is translated into an $\ALCK(\Dsf_1)$-concept
$C_{\Dmf,a}$ as displayed in Figure~\ref{fig:alckdred}. Names such as
\mn{TreeX} and \mn{TreeY} are used as abbreviations only. We use
$\forall R^i.C$ as an abbreviation for the $n$-fold nesting $\forall
R. \cdots \forall R .C$.  The names $\mn{xpos}_i$ and $\mn{ypos}_i$
used in the figure denote concrete features. In the definition of the
\mn{Init} concept, for each $n \in \mathbbm{N}$, $\mn{bit}_i(n)$ is
supposed to denote the $i$'th bit of the binary representation of $n$.
We claim that $C_{\Dmf,a}$ is satisfiable w.r.t.\ the key box
$$
  \{ (\mn{xpos}_0,\dots,\mn{xpos}_n,\mn{ypos}_0,\dots,\mn{ypos}_n
  \text{ keyfor } \top) \}
$$

\noindent
iff there exists a solution for $\Dmf$ and $a$. To substantiate this
claim, let us go through the reduction and explain the various parts
of the concept~$C_{\Dmf,a}$. The first step towards understanding the
structure of models of $C_{\Dmf,a}$ (which is the key to understanding
the reduction itself) is to note that the purpose of the first line of
$C_{\Dmf,a}$ is to enforce a tree structure of depth $2(n+1)$, whose
leaves correspond to positions in the $2^{n+1} \times 2^{n+1}$-torus.
More precisely, the \mn{TreeX} concept guarantees that, in every model
\Imc of $C_{\Dmf,a}$, there exists a binary tree of depth $n+1$.
Moreover, the $\mn{DistX}_k$ concepts (there exists one for each $k
\in \{0,\dots,n\}$) ensure that the leaves of this tree are binarily
numbered (from 0 to $2^{n+1}-1$) by the concept names
$X_0,\dots,X_{n}$. More precisely, for a domain object $d \in
\Delta_\Imc$, set
  $$
  \mn{xpsn}(d)=\Sigma_{i=0}^{n} \alpha_i(d) * 2^i ~~\mbox{ where }~~
\alpha_i(d) = \left\{ 
  \begin{array}{ll}
    1 & \text{if } d \in X_i^\Imc \\
    0 & \text{otherwise.}
  \end{array} \right.
  $$
  
\noindent
The \mn{TreeX} and \mn{DistX} concepts ensure that there exist nodes
$d_0,\dots,d_{2^{n+1}-1}$ at level $n+1$ of the tree such that
$\mn{xpsn}(d_i)=i$. Intuitively, this numbering represents the
horizontal positions in the $2^{n+1} \times 2^{n+1}$-torus. The
vertical positions are coded in a similar way by the $Y_0,\dots,Y_n$
concept names.  More specifically, the concepts \mn{TreeY},
\mn{DistX}, and \mn{DistY} ensure that every $d_i$ ($i \leq
2^{n+1}-1$) is the root of another tree, in which (i)~every node has
the same ``$X_0,\dots,X_{n}$-configuration'' as its root node, and
(ii)~the leaves are numbered binarily using the concept names
$Y_0,\dots,Y_n$ (note that the \mn{TreeY} concept appears in
$C_{\Dmf,a}$ inside a $\forall R^{n+1}$ value restriction). Define
  $$ 
\mn{ypsn}(d)=\Sigma_{i=0}^{n} \beta_i(d) * 2^i ~~\mbox{ where }~~
\beta_i(d) = \left\{ 
  \begin{array}{ll}
    1 & \text{if } d \in Y_i^\Imc \\
    0 & \text{otherwise.}
  \end{array} \right.
  $$

\noindent
In the set of leaf nodes of all the trees enforced by the \mn{TreeY}
concept, there exists, for each $i,j < 2^{n+1}$, an object\footnote{It does
  not matter if there is more than one such object.} $e_{i,j}
\in \Delta_\Imc$ such that $\mn{xpsn}(e_{i,j})=i$ and
$\mn{ypsn}(e_{i,j})=j$, i.e., each $e_{i,j}$ represents the position
$(i,j)$ in the $2^{n+1} \times 2^{n+1}$-torus.
  
  The next step is to translate the individual bits of the numbering
  of the $e_{i,j}$-objects, which are up to now represented by
  concept names, into concrete domain values. This is done by the
  \mn{TransXPos} and \mn{TransYPos} concepts which ensure that,
  for all $\ell \leq n$, we have
  $\mn{xpos}^\Imc_\ell(e_{i,j})=0$ if $e_{i,j} \in \neg X_\ell$,
  $\mn{xpos}^\Imc_\ell(e_{i,j})=1$ if $e_{i,j} \in X_\ell$, and similarly for
  $\mn{ypos}_\ell$ and~$Y_\ell$. Since \Imc is a model for the key box
  $$
  \{ (\mn{xpos}_0,\dots,\mn{xpos}_n,\mn{ypos}_0,\dots,\mn{ypos}_n
  \text{ keyfor } \top) \},
  $$

\noindent
  grid positions are \emph{uniquely} represented by domain elements
  from $(\mn{TransXPos} \sqcap \mn{TransYPos})^\Imc$, i.e., if $d,e
  \in (\mn{TransXPos} \sqcap \mn{TransYPos})^\Imc$ such that
  $\mn{xpsn}(d)=\mn{xpsn}(e)$ and $\mn{ypsn}(d)=\mn{yxpsn}(e)$, then
  $d=e$. This fact is used in the concepts $\mn{Succs}$, $\mn{XSuccOk}$, and
  $\mn{YSuccOk}$ to enforce that, for the two roles $R_x$ and $R_y$
  and each $i,j \leq n$, the following holds:
  %
  \begin{equation}
  \begin{array}{rcl}
    R_x^\Imc \cap ( \{ e_{i,j} \} \times \Delta_\Imc ) & = & \{ (e_{i,j},e_{(i \oplus_{2^{n+1}} 1),j} \} \\[1mm]
    R_y^\Imc \cap ( \{ e_{i,j} \} \times \Delta_\Imc ) & = & \{ (e_{i,j},e_{i,(j \oplus_{2^{n+1}} 1)} \}.
  \end{array}
  \tag{$*$}
  \end{equation}
  
\noindent
  The \mn{Succs} concept ensures that, for each
  $e_{i,j}$, there exists an $R_x$-successor and an $R_y$-successor,
  and that both are in $(\mn{TransXPos} \sqcap \mn{TransYPos})^\Imc$.
  Let $d$ be an $R_x$-successor of $e_{i,j}$.  Then the $\mn{XSuccOk}$
  concept ensures that $\mn{xpsn}(d)=i \oplus_{2^{n+1}} 1$ and
  $\mn{ypsn}(d)=j$. Before we explain how it does this, let us note
  that, since all $e_{i,j}$ are in $(\mn{TransXPos} \sqcap
  \mn{TransYPos})^\Imc$ and the grid positions are uniquely
  represented by elements of $(\mn{TransXPos} \sqcap
  \mn{TransYPos})^\Imc$, this implies $d=e_{(i \oplus_{2^{n+1}} 1),j}$
  which shows that the upper line of $(*)$ does indeed hold.
  
  Let us now consider the $\mn{XSuccOk}$ concept in some more detail.
  It is essentially the DL-formulation of the well-known propositional
  formula
  $$
     \bigwedge_{k=0}^{n}
    (\bigwedge_{j=0}^{k-1} x_j = 1) \rightarrow (x_k = 1 \leftrightarrow x'_k
    = 0) 
    ~\wedge~ \bigwedge_{k=0}^{n} (\bigvee_{j=0}^{k-1} x_j = 0) \rightarrow
    (x_k = x'_k)
  $$

\noindent
which encodes incrementation modulo $2^{n+1}$, i.e., if $t$ is the
number (binarily) encoded by the propositional variables
$x_0,\dots,x_{n}$ and $t'$ is the number encoded by the propositional
variables $x'_0,\dots,x'_{n}$, then we have $t' = t + 1$ modulo
$2^{n+1}$ (see \citeR{Boerger-et-al-97}). Taking into account the
$\forall R_x$ quantifiers in $\mn{XSuccOk}$, it is readily checked
that this concept has just the desired effect: to ensure that, for
every $R_x$-successor $d$ of $e_{i,j}$, we have
$\mn{xpsn}(d)=\mn{xpsn}(e_{(i \oplus_{2^{n+1}} 1),j})=i
\oplus_{2^{n+1}} 1$.  The explanation of $\mn{YSuccOk}$ and how it
enforces the lower line of $(*)$ is analogous to the $\mn{XSuccOk}$
case.
  
  It remains to ensure that every grid position is labeled with
  precisely one tile and that the initial condition as well as the
  horizontal and vertical matching conditions are satisfied. The tiles
  are represented by concept names $D_i$ (where $i$ is from the set of
  tiles $T$) and the described tasks are accomplished in the standard
  way by the concepts \mn{Label}, \mn{Init}, and \mn{CheckMatch}.
  
  It is worth noting that the reduction concept is path-free and the
  key box is simple, i.e., path-free and Boolean.  Path-freeness of
  concepts is often used to tame the complexity of description logics
  with concrete domains, although it largely sacrifices their
  expressive
  power~\cite{Lutz-02e,Baader-et-al-02,Haarslev-et-al-01,Horrocks-Sattler-01}.
  For example, if \ALCD is augmented with general TBoxes, then
  reasoning with arbitrary concepts is undecidable while reasoning
  with path-free concepts is \ExpTime-complete if \Dmc is admissible
  and \Dmc-satisfiability is in \ExpTime~\cite{Lutz-Diss}.  This
  ``taming approach'' does not work in the presence of key boxes
  since, as we have just seen, satisfiability of \ALCD-concepts
  w.r.t.~key boxes is (under some natural assumptions) \NExpTime-hard,
  even if both concept and key box are path-free.

  Since the size of $C_{\Dmf,a}$ and of the used key box is clearly
  polynomial in $n$, we obtain the following proposition.
                                %
  \begin{proposition}
    \label{alckdprop}
    The satisfiability of path-free $\ALCK(\Dsf_1)$-concepts w.r.t.\ 
    simple key boxes is \NExpTime-hard.
  \end{proposition}
       
\noindent                         %
It has been shown that (non path-free) $\ALCD$-concept satisfiability
is \PSpace-complete if \Dmc-satisfiability is in \PSpace
\cite{Lutz-02d}. Hence, it follows from Proposition~\ref{d1compl} that
$\ALC(\Dsf_1)$-concept satisfiability is \PSpace-complete. Thus, there
is a rather dramatic increase of complexity if key boxes are added to
$\ALC(\Dsf_1)$. To stress that this increase is due to the key boxes
themselves and not to the complexity of $\Dsf_1$-satisfiability, we
reformulate Proposition~\ref{alckdprop}:
                                %
  \begin{theorem}
    There exists a concrete domain \Dmc such that \Dmc-satisfiability
    is in \PTime and satisfiability of path-free 
    $\ALCKD$-concepts w.r.t.\ simple key boxes is
    \NExpTime-hard.
  \end{theorem}
                                %
  \noindent 
  Although, due to its very low expressivity, the concrete domain
  $\Dsf_1$ itself is not very natural for knowledge representation, it
  is a fragment of many concrete domains that have been proposed in
  the literature~\cite{Baader-Hanschke-92,Haarslev-Moeller-01b,Lutz-02e,Lutz-02d}.
  Indeed, the presented reduction strategy can be adapted to several
  ``standard'' concrete domains.  Let us formulate a (very
  weak) condition that a concrete domain must satisfy in order for
  the presented reduction strategy to be applicable.
  %
  \begin{theorem}
    Let \Dmc be a concrete domain. If there exist $a,b \in
    \Delta_\Dmc$ with $a\neq b$ and $P_1,P_2 \in \Phi_\Dmc$ such that
    $P_1^\Dmc = \{ a \}$ and $P_2^\Dmc = \{ b \}$, then the
    satisfiability of path-free $\ALCKD$-concepts w.r.t.\ simple key
    boxes is \NExpTime-hard.
  \end{theorem}
  
\noindent 
   We now present the second \NExpTime-hardness result for
   \ALCKD-concept satisfiability. This time, we reduce the
   \NExpTime-complete domino problem to the satisfiability of
   path-free $\ALCK(\Dsf_2)$-concepts w.r.t.\ simple \emph{unary} key
   boxes.  The reduction is very similar to the previous one and we
   only discuss the differences. 
   
   In the first reduction, we represented the individual bits of grid
   positions by individual concrete features $\mn{xpos}_i$ and
   $\mn{ypos}_i$ and used a composite key box to ensure that each
   point in the torus is represented by at most one element. 
                                %   
   In the second reduction, we use a single concrete feature $\mn{bv}$
   and represent an entire position $(i,j)$ in the torus using a bit
   vector from the concrete domain $\Dsf_2$. This allows us to
   enforce the above mentioned uniqueness of representations using a
   \emph{unary} key box.

\psfull
\begin{figure}[t!]
  \begin{boxedminipage}[t]{\textwidth}
  \begin{center}
  \begin{gather*}
    \begin{split}
      \mn{Succs2} &:= \exists R_x . \mn{TransPos} \sqcap \exists R_y . \mn{TransPos} \\
      \mn{TransPos} &:=  \bigsqcap_{i=0..n} \big ( ( 
        X_i \rightarrow \exists \mn{bv} . \mn{bit1}^i_{2(n+1)} ) \sqcap
        \neg X_i \rightarrow \exists \mn{bv}. \mn{bit0}^i_{2(n+1)} )
      \big ) \sqcap \mbox{} \\
      &\phantom{Cc} \bigsqcap_{i=0..n} \big ( ( 
        Y_i \rightarrow \exists \mn{bv} . \mn{bit1}^{n+i+1}_{2(n+1)} ) \sqcap
        \neg Y_i \rightarrow \exists \mn{bv} . \mn{bit0}^{n+i+1}_{2(n+1)} ) \big )
      \\
      C_{\Dmf,a} &:= \mn{TreeX} \sqcap \forall R^{n+1} . \mn{TreeY}  \\
      &\phantom{Cc} \sqcap \forall R^{2(n+1)} . ( \mn{TransPos} \sqcap \mn{Succs2} \sqcap \mn{XSuccOk} \sqcap \mn{YSuccOk}) \\
      &\phantom{Cc} \sqcap \forall R^{2(n+1)} . (\mn{Label} \sqcap \mn{CheckMatch} \sqcap \mn{Init})
    \end{split}      
  \end{gather*}
  \end{center}
  \end{boxedminipage}
  \caption{The $\ALCK(\Dsf_2)$ reduction concept $C_{\Dmf,a}$.}
  \label{fig:alckdred2}
\end{figure}
\psdraft

The modified reduction concept $C_{\Dmf,a}$ can be found in
Figure~\ref{fig:alckdred2}, where %\mn{bv} denotes a concrete feature
%and 
the concepts \mn{TreeX}, \mn{TreeY}, $\mn{DistX}_k$, $\mn{DistY}_k$,
\mn{XSuccOk}, \mn{YSuccOk}, \mn{Label}, \mn{CheckMatch}, and \mn{Init}
are defined as in Figure~\ref{fig:alckdred}.  The translation of the
position in the torus encoded by $X_0,\dots,X_n,Y_0,\dots,Y_n$ into a
bit vector is done by the \mn{TransPos} concept in a straightforward
manner. Given what was said about the first reduction, it is not hard
to see that $C_{\Dmf,a}$ is satisfiable w.r.t.\ the key box $\{
(\mn{bv} \mbox{ keyfor } \top) \}$ iff there exists a solution for
$\Dmf$ and $a$. We thus obtain the following proposition.

\begin{proposition}
  The satisfiability of path-free $\ALCK(\Dsf_2)$-concepts w.r.t.\
  simple unary key boxes is \NExpTime-hard.
\end{proposition}

\noindent
Again, we relate the \NExpTime lower bound to the complexity of 
$\Dsf_2$-satisfiability, which is determined in Proposition~\ref{d2compl}.
%
\begin{theorem}
  There exists a concrete domain \Dmc such that \Dmc-satisfiability is
  in \PTime and the satisfiability of path-free \ALCKD-concepts
  w.r.t.\ simple unary key boxes is {\textnormal {\sc NExp\-Time}}-hard.
\end{theorem}

\noindent
Since the elements of $\Delta_{\Dsf_2}$ are bit vectors, the concrete
domain $\Dsf_2$ cannot be considered a natural choice for many
application areas. But, in the reduction,
$\Dsf_2$ can be replaced by several natural concrete domains. 

The central observation is that we use bit vectors only to injectively
translate sequences of bits into values of the concrete domain, i.e.,
we translate sequences of $2(n+1)$ bits (represented by the concept
names $X_0,\dots,X_n$ and $Y_0,\dots,Y_n$) into elements of
$\Delta_{\Dsf_2}$ such that, for \emph{distinct} sequences, the
results of the translation are also distinct. Due to this restricted
use of bit vectors, there are several ways to replace them by natural
numbers.  For example, we can replace \mn{TransPos} with the following
concept $\mn{TransPos}'$ which ensures that, for each $d \in
\mn{TransPos}'^\Imc$, $s_{2n+1}^\Imc (d)= \mn{xpsn}(d) + 2^{n+1} \cdot
\mn{ypsn}(d)$:
                                %
\begin{gather*}
  \begin{split}
 %      \mn{TransPos}' &:=  \exists \mn{zero} . {=}_0 \sqcap (\neg X_0 \rightarrow \exists s_0 . {=}_0)
%       \sqcap (X_0 \rightarrow \exists s_0 . {=}_1) 
%       \\
%       &\phantom{:=l} \sqcap \bigsqcap_{i=1..n} \Big ( \exists t_i . {=}_{2^i}
% \sqcap \big (\neg X_i \rightarrow
%       \exists (s_{i-1},\mn{zero},s_i).{+} \big ) \sqcap \big ( X_i \rightarrow 
%       \exists (s_{i-1},t_i,s_i).{+} \big ) \Big )
%       \\
%       &\phantom{:=l} \sqcap \bigsqcap_{i=0..n} \Big ( \exists t_{n+i+1} . {=}_{2^{n+i+1}} \sqcap
%       \big ( \neg Y_i \rightarrow \exists (s_{n+i},\mn{zero},s_{n+i+1}).{+} \big ) \sqcap 
%       \\
%       &\phantom{CCCCCCCCCCCCCCCCCCCCC} \big ( Y_i \rightarrow
%       \exists (s_{n+i},t_{n+i+1},s_{n+i+1}).{+} \big ) \big )
     \mn{TransPos}' &:=  
     \begin{array}[t]{cl}
\multicolumn{2}{l}{      \exists \mn{zero} . {=}_0 \sqcap
      \bigsqcap_{i=1\ldots 2n+1} \big (\some {t_i}{{=}_{2^i}} \big  )
      \sqcap (\neg X_0 \rightarrow \exists s_0 . {=}_0)
      \sqcap (X_0 \rightarrow \exists s_0 . {=}_1)  \sqcap~ }
      \\
  \hspace*{-.5cm}     \bigsqcap_{i=1..n} &\Big ( \big (\neg X_i \rightarrow
      \exists (s_{i-1},\mn{zero},s_i).{+} \big ) \sqcap \big ( X_i \rightarrow 
      \exists (s_{i-1},t_i,s_i).{+} \big ) \Big ) \sqcap ~
      \\[1.5ex]
   \hspace*{-.5cm}    \bigsqcap_{i=n+1..2n+1} &\Big ( 
      \big ( \neg Y_{i-(n+1)} \rightarrow \exists (s_{i-1},\mn{zero},s_{i}).{+} \big ) \sqcap 
      ( Y_{i-(n+1)} \rightarrow
      \exists (s_{i-1},t_{i},s_{i}).{+} \big ) \Big )     \end{array}
  \end{split}      
\end{gather*}

\noindent
where $\mn{zero}$, $s_i$, and $t_i$ are concrete features,
$=_{k}$ (with $k \in \mathbbm{N}$) denotes a unary predicate with the
obvious extension, and $+$ denotes a ternary addition predicate such
that, intuitively, the first two arguments are the addends and the third
one is the sum.

It is easy to check that, whenever two objects $d,e \in
{\mn{TransPos}'}^\Imc$ do \emph{not} agree on the interpretation of the
$X_0,\dots,X_n,Y_0,\dots,Y_n$, then $s^\Imc_{2n+1}(d) \neq
s^\Imc_{2n+1}(e)$, and thus the key box $\{ (s_{2n+1} \mbox{ keyfor }
\top) \}$ can be used for the reduction. The size of $\mn{TransPos}'$
is obviously polynomial in $n$ if the numbers $k$ appearing in ${=}_k$
predicates are coded in binary.  We thus obtain the following theorem:

\begin{theorem}
  Let \Dmc be a concrete domain such that 
  %
  \begin{enumerate}
  \item $\mathbbm{N} \subseteq \Delta_\Dmc$, 
 
  \item $\Phi_\Dmc$ contains, for each $k \in \mathbbm{N}$, a
    predicate ${=}_k$ with $({=}_k)^\Dmc=\{k\}$ where the size of (the
    representation of) ${=}_k$ is logarithmic in $k$, and

  \item $\Phi_\Dmc$ contains a predicate $+$ with $({+})^\Dmc \cap \{
    (k_1,k_2,x) \mid k_1,k_2 \in \mathbbm{N} \mbox{ and } x \in
    \Delta_\Dmc \} = \{ (k_1,k_2,k_1+k_2) \mid k_1,k_2 \in \mathbbm{N} \}$. 

  \end{enumerate}
  
\noindent
  Then the satisfiability of path-free \ALCKD-concepts w.r.t.\ simple
  unary key boxes is \NExpTime-hard.
\end{theorem}

\noindent
For example, this theorem yields \NExpTime-lower bounds for \ALCKD
instantiated with the concrete domains proposed
in~\cite{Baader-Hanschke-92,Haarslev-Moeller-01b,Lutz-02e,Lutz-02d}.
An alternative to the addition predicate is to use multiplication to
injectively translate sequences of bits into natural numbers. More
precisely, let $p_1,\dots,p_{2n+1}$ be the first $2n+1$ prime numbers
and define another version of \mn{TransPos} as follows:
%
\begin{gather*}
  \begin{split}
      \mn{TransPos}'' &:=  \exists \mn{one} . {=}_1 \sqcap
      \bigsqcap_{i=1\ldots 2n+1} \big ( \exists t_i . {=}_{p_i} \big )
      \sqcap (\neg X_0 \rightarrow \exists s_0 . {=}_0) 
      \sqcap (X_0 \rightarrow \exists s_0 . {=}_1) \sqcap ~
      \\
      &\phantom{:=l}
      \begin{array}[t]{cl} \bigsqcap_{i=1..n} & \Big ( 
\big (\neg X_i \rightarrow
      \exists (s_{i-1},\mn{one},s_i).{*} \big ) \sqcap \big ( X_i \rightarrow 
      \exists (s_{i-1},t_i,s_i).{*} \big ) \Big ) \sqcap ~
      \\[1.5ex]
       \bigsqcap_{i=n+1..2n+1} & \Big (\big ( \neg Y_{i-(n+1)} \rightarrow
      \exists (s_{i-1},\mn{one},s_{i}).{*} \big ) \sqcap \big ( Y_{i-(n+1)} \rightarrow
      \exists (s_{i-1},t_{i},s_{i}).{*} \big ) \Big )      \end{array}
  \end{split}      
\end{gather*}

\noindent
where $*$ is a ternary multiplication predicate. 

Since the factorization of natural numbers into prime numbers is
unique, we can again use the key box $\{ (s_{2n+1} \mbox{ keyfor }
\top) \}$ for the reduction. Moreover, it is well-known that the
$k$'th prime is polynomial in $k$~\cite{Graham-90}, and thus the size
of the concept $\mn{TransPos}''$ is polynomial in $n$ even if the
numbers $k$ in $=_k$ predicates are coded unarily. We thus obtain
another theorem concerning quite natural concrete domains:

\begin{theorem}
  Let \Dmc be a concrete domain such that 
  %
  \begin{enumerate}

  \item $\mathbbm{N} \subseteq \Delta_\Dmc$, 
    
  \item $\Phi_\Dmc$ contains, for each $k \in \mathbbm{N}$, a
    predicate ${=}_k$ with $({=}_k)^\Dmc=\{k\}$, and
  
  \item $\Phi_\Dmc$ contains a predicate $*$ with $({*})^\Dmc \cap \{
  (k_1,k_2,x) \mid k_1,k_2 \in \mathbbm{N} \mbox{ and } x \in
  \Delta_\Dmc \} = \{ (k_1,k_2, k_1 \cdot k_2) \mid k_1,k_2 \in \mathbbm{N} \}$.

 \end{enumerate}
 
\noindent
 Then the satisfiability of path-free
  \ALCKD-concepts w.r.t.\ simple unary key boxes is
  \NExpTime-hard.
\end{theorem}


\subsection{\NExpTime-hardness of \ALCOD}
\label{sect:alcodhard}

As we already pointed out in Section~\ref{sect:intro}, the
relationship between key boxes and nominals is rather close: the
latter can be ``simulated'' by the former if the concrete domain
provides predicates that can be used to uniquely describe elements
of~$\Delta_\Dmc$. For example, in $\ALCK(\Dsf_1)$ the concept $\exists
g . {=}_0$ behaves as a nominal if we use the key assertion $(g
\text{ keyfor } \top)$. We can even define $n$ nominals using $n$
single concrete features in unary-key assertions. In the logics
$\ALCK(\Dsf_2)$ and $\ALCK(\Dsf_3)$, a single concrete feature and
unary key assertions are sufficient to simulate an arbitrary number
of nominals: for example, in $\ALCK(\Dsf_2)$ the concept $C=\exists g
.  \mn{bit0}^0_2 \sqcap \exists g .  \mn{bit1}^1_2$ uniquely describes
the bit vector $(0,1) \in \mn{BV}_2 \subseteq \Delta_{\Dsf_2}$, i.e.,
$a\in C^\Imc$ implies $g^\Imc(a)=(0,1)$. Obviously, any other bit
vector (of any length!)  can be described in a similar way.

This illustrates that, for most non-trivial concrete domains \Dmc, the
logic \ALCKD is (at least) as expressive as \ALCOD. Although the
converse does not hold, the expressive power of \ALCOD is still
sufficient to prove \NExpTime-hardness of concept satisfiability,
provided that a suitable concrete domain \Dmc is used.  Since \ALCO
concept satisfiability is \PSpace-complete \cite{Areces-et-al-99},
this is yet another example of a DL where an even seemingly harmless
extension with concrete domains has a dramatic effect on the
computational complexity \cite{Lutz-02e}.

In this section, we reduce the \NExpTime-complete domino-problem to
$\ALCO(\Dsf_3)$-concept satisfiability.
                                %
Again, let $\Dmf=(T,H,V)$ be a domino system and $a=a_0,\dots,a_{n-1}$
an initial condition. The modified reduction concept $C_{\Dmf,a}$ is
defined in Figure~\ref{fig:alcodred},
%
\psfull
\begin{figure}[t!]
  \begin{boxedminipage}[t]{\textwidth}
  \begin{center}
  \begin{gather*}
    \begin{split}
      \mn{Nominal} &:= \exists f . N
      \\[1.5ex]
      \mn{XSucc} &:= \bigsqcap_{k=0..n} \big ( \bigsqcap_{j=0..k} X_j \big )
       \rightarrow (X_k \leftrightarrow \neg X'_k )  \sqcap
      \bigsqcap_{k=0..n} \big ( \bigsqcup_{j=0..k} \neg X_j \big )
       \rightarrow (X_k \leftrightarrow X'_k )
      \\
      \mn{YSucc} &:= \bigsqcap_{k=0..n} \big ( \bigsqcap_{j=0..k} Y_j \big )
       \rightarrow (Y_k \leftrightarrow \neg Y'_k )  \sqcap
      \bigsqcap_{k=0..n} \big ( \bigsqcup_{j=0..k} \neg Y_j \big )
       \rightarrow (Y_k \leftrightarrow Y'_k )
      \\[1.5ex]
      \mn{TransXPos} &:=  \bigsqcap_{i=0..n} \big ( ( 
        X_i \rightarrow \exists \mn{bvx} . \mn{pos1}^i_{n+1} ) \sqcap
        (\neg X_i \rightarrow \exists \mn{bvx}. \mn{pos0}^i_{n+1} ) \big ) 
      \\
      \mn{TransYPos} &:=  \bigsqcap_{i=0..n} \big ( ( 
        Y_i \rightarrow \exists \mn{bvy} . \mn{pos1}^i_{n+1} ) \sqcap
        (\neg Y_i \rightarrow \exists \mn{bvy}. \mn{pos0}^i_{n+1} ) \big ) 
      \\[1.5ex]
      \mn{TransXSucc} &:=  \bigsqcap_{i=0..n} \big ( ( 
        X'_i \rightarrow \exists \mn{bvxs} . \mn{pos1}^i_{n+1} ) \sqcap
        (\neg X'_i \rightarrow \exists \mn{bvxs}. \mn{pos0}^i_{n+1} ) \big ) 
      \\
      \mn{TransYSucc} &:=  \bigsqcap_{i=0..n} \big ( ( 
        Y'_i \rightarrow \exists \mn{bvys} . \mn{pos1}^i_{n+1} ) \sqcap
        (\neg Y'_i \rightarrow \exists \mn{bvys}. \mn{pos0}^i_{n+1} ) \big ) 
      \\[1.5ex] 
      \mn{CheckHMatch} &:= \bigsqcup_{i,j \in H} ( \exists(\mn{bvx}, \mn{bvy}, f \circ \mn{darr}).\mn{tile}^{i}_{n+1} \sqcap \exists(\mn{bvxs}, \mn{bvy}, f \circ \mn{darr}).\mn{tile}^{j}_{n+1} )
      \\
      \mn{CheckVMatch} &:= \bigsqcup_{i,j \in V} ( \exists(\mn{bvx}, \mn{bvy}, f \circ \mn{darr}).\mn{tile}^{i}_{n+1} \sqcap \exists(\mn{bvx}, \mn{bvys}, f \circ \mn{darr}).\mn{tile}^{j}_{n+1} )
      \\[1.5ex]
%      \mn{Label2} &:= \bigsqcup_{i \in T} \exists ( f \circ \mn{darr}, \mn{bv} ).\mn{tile}^i_{2(n+1)}
%      \\
      \mn{Init2} &:= \bigsqcap_{i=0..n-1}  \Big ( \big ( 
        \bigsqcap_{j=0..n, \mn{bit}_j(i) = 0} \neg X_j \; \sqcap
        \bigsqcap_{j=0..n, \mn{bit}_j(i) = 1} X_j \; \sqcap \bigsqcap_{j=0..n}
        \neg Y_j \big ) \\
      &\hspace*{3cm}\rightarrow \exists (\mn{bvx}, \mn{bvy}, f \circ \mn{darr}) . \mn{tile}^{a_i}_{n+1} \Big )
      \\[1.5ex]
      C_{\Dmf,a} &:= \mn{TreeX} \sqcap \forall R^{n+1} . \mn{TreeY}
        \sqcap \forall R^{2(n+1)} . \mn{Nominal} \sqcap ~ \\
      &\phantom{Cc}  \forall R^{2(n+1)} . (  \mn{TransXPos}
        \sqcap \mn{TransYPos}  \sqcap ~ \\
      &\phantom{Cc \forall R^{2(n+1)} . (} \mn{XSucc} \sqcap
        \mn{YSucc} \sqcap \mn{TransXSucc} \sqcap \mn{TransYSucc}
        \sqcap ~ \\
      &\phantom{Cc  \forall R^{2(n+1)} . (} \mn{Init2} \sqcap \mn{CheckHMatch}
%      &\phantom{Cc \sqcap \forall R^{2(n+1)} . (} \mn{Init2} \sqcap \mn{Label2} \sqcap \mn{CheckHMatch}
      \sqcap \mn{CheckVMatch})
    \end{split}      
  \end{gather*}
  \end{center}
  \end{boxedminipage}
  \caption{The $\ALCO(\Dsf_3)$ reduction concept $C_{\Dmf,a}$.}
  \label{fig:alcodred}
\end{figure}
\psdraft
%
where \mn{bvx}, \mn{bvy}, \mn{bvxs}, \mn{bvys}, and \mn{darr} denote
concrete features, $N$ denotes a nominal, and the concepts \mn{TreeX},
\mn{TreeY}, $\mn{DistX}_k$, and $\mn{DistY}_k$ are defined as in
Figure~\ref{fig:alckdred}. As in the previous reductions, we now give
a detailed explanation of the reduction strategy to show that
$C_{\Dmf,a}$ is satisfiable iff there exists a solution for \Dmf and
$a$. Formal details can then easily be worked out by the interested
reader.

Let \Imc be a model for $C_{\Dmf,a}$. To explain the structure of
\Imc, it is convenient to start with the first line of $C_{\Dmf,a}$.
As in the previous reductions, the \mn{TreeX} and \mn{TreeY} concepts
are used to ensure that \Imc contains a tree-shaped substructure of
depth $n+1$ whose leaf nodes are the roots of additional trees of
depth $n+1$ such that the set of the leafs of the latter trees
correspond to the positions in the $2^{n+1} \times 2^{n+1}$-torus,
i.e., for each position, there is a leaf node representing it. The
torus positions are binarily encoded by the concept names
$X_0,\dots,X_n$ and $Y_0,\dots,Y_n$ and we use $e_{i,j}$ to refer to
the leaf with $\mn{xpsn}(e_{i,j})=i$ and $\mn{ypsn}(e_{i,j})=j$ (see
Section~\ref{sect:alckdhard}).

As in the previous reductions, the numbers coded by $X_0,\dots,X_n$ and
$Y_0,\dots,Y_n$ are translated into concrete domain values, which
 is done by the \mn{TransXPos} and \mn{TransYPos} concepts. Note that, in contrast to
the $\ALCK(\Dsf_2)$-reduction, the x-position and the y-position are
not stored in the same bit vector, but rather in the two distinct ones
\mn{bvx} and \mn{bvy}. Also in contrast to the previous reduction, the
actual tiling of the torus is \emph{not} represented by the leaf nodes
$e_{i,j}$, but rather by a domino array: the last conjunct in the first
line of $C_{\Dmf,a}$ ensures that every leaf $e_{i,j}$ is connected
via the abstract feature $f$ to the (unique) element $w \in N^\Imc$.
%
\psfull
\begin{figure}[t!]
  \begin{boxedminipage}[t]{\textwidth}
  \begin{center}
    \input{models.pdftex_t}
  \end{center}
  \end{boxedminipage}
  \caption{The structure of models of  $C_{\Dmf,a}$.}
  \label{fig:modstruct}
\end{figure}
\psdraft

\noindent
The domain element $w$ is associated with a domino array via the concrete
feature \mn{darr} (as we shall see later, this is guaranteed by the
\mn{CheckHMatch} and \mn{CheckVMatch} concepts). This domino array
represents the tiling of the $2^{n+1} \times 2^{n+1}$-torus. Summing up,
the structure of \Imc is roughly as shown in
Figure~\ref{fig:modstruct}.

Since the tiling is stored in a domino array, we need to explain the
purpose of the leaf nodes $e_{i,j}$: these nodes are used to enforce
the initial condition and the horizontal and vertical matching
condition.  Let us discuss the horizontal matching condition (the
vertical matching condition is enforced analogously): the $\mn{XSucc}$
concept is the DL reformulation of the propositional logic formula for
incrementation modulo $2^{n+1}$ and ensures that, for each\ $e_{i,j}$,
the concept names $X'_0,\dots,X'_n$ encode the number $i
\oplus_{2^{n+1}} 1$, i.e., the horizontal position of $e_{i,j}$'s
horizontal neighbor.  In addition to the storage of the horizontal and
vertical position of $e_{i,j}$ in $\mn{bvx}(e_{i,j})$ and
$\mn{bvy}(e_{i,j})$, we also store the horizontal position
$i\oplus_{2^{n+1}} 1$ of $e_{i,j}$'s horizontal successor in
$\mn{bvxs}(e_{i,j})$.
%
Finally, \mn{CheckHMatch} verifies that the tiles at positions
$(i,j)$ and $(i\oplus_{2^{n+1}} 1,j)$, which are both stored in the
domino array, are compatible with the horizontal matching condition.

Note that \mn{CheckHMatch} also ensures that the domain element $w$
(with $\{w\} = N^\Imc$) has a domino array attached via the concrete
feature $\mn{darr}$ and that, for each position $(i,j)$, the (unique!)
tile stored in the domino array is from the set $T$.  The initial
condition is ensured via the \mn{Init2} concept in a similar way. We
(again) use $\mn{bit}_j(i)$ to denote the $j$'th bit of the binary
encoding of the natural number $i$.

Using the above considerations, the correctness of the reduction is
readily checked. Moreover, the size of $C_{\Dmf,a}$ is at most
polynomial in $n$. Note that $C_{\Dmf,a}$ is \emph{not} path-free:
paths of length two appear in the concepts \mn{CheckHMatch},
\mn{CheckVMatch}, and \mn{Init2}. Summing up, the reduction described
yields the following result:

\begin{proposition}
  The satisfiability of $\ALCO(\Dsf_3)$-concepts is
  \NExpTime-hard.
\end{proposition}

\noindent
Again, we relate the \NExpTime lower bound to the complexity of
$\Dsf_3$-satisfiability, which is determined in Proposition~\ref{d3compl}.

\begin{theorem}
  There exists a concrete domain \Dmc such that \Dmc-satisfiability is
  in \PTime and the satisfiability of \ALCOD-concepts is
  \NExpTime-hard.
\end{theorem}

\noindent
Note that the reduction uses only a \emph{single nominal} $N$. This is
a dramatic increase of complexity since it has been shown that
satisfiability of \ALCD-concepts (i.e., without nominals and key
boxes) is \PSpace-complete provided that \Dmc is admissible and
\Dmc-satisfiability is in \PSpace \cite{Lutz-02d}.

As in previous sections, we note that $\Dsf_3$ can be replaced by more
natural concrete domains in the \NExpTime-hardness proof presented.
The idea is to represent the whole domino array by a single natural
number and then to use arithmetic operations to access the individual
positions: a natural number $k$ can be viewed as a domino array by
partitioning its binary representation into $2^{n+1} \cdot 2^{n+1} =
2^{2(n+1)}$ ``sections'' of length $\lceil \log(\#T)\rceil$, where
$\#T$ denotes the cardinality of the set of tile types $T$. Each such
section describes the tile of a single position in the torus. The
sections can be accessed by using integer division and reminder
operations: if $k$ is the natural number representing the torus, then
the tile of posisition $i$ is computed by
%
$$
(k \; \text{div} \; 2^{i \cdot
  \lceil \log(\#T)\rceil}) \!\! \mod 2^{\lceil \log(\#T)\rceil}+1.
$$
%
Thus, we introduce ternary predicates \mn{div} for integer division
and \mn{mod} for computing the remainder of a division, and a binary
predicate $\mn{2^x}$ expressing exponentiation with basis~2. Then we
modify the reduction as follows: we replace \mn{TransXPos} and
\mn{TransYPos} by the $\mn{TransPos}'$ concept from
Section~\ref{sect:alckdhard} to translate the two numbers encoded by
$X_1,\dots,X_n$ and $Y_1,\dots,Y_n$ into a single natural number that
is stored in the concrete feature $s_{2n+1}$. We then devise a new
concept $\mn{Tile}[i]$ (for each $i \in T$) enforcing that the
position identified by the feature $s_{2n+1}$ is labeled with tile
$i$:
%
\begin{gather*}
  \begin{split}
      \mn{Tile}[i] := & \; \exists r . {=}_{\lceil \log(\#T)\rceil} \sqcap \exists s_{2n+1}, r, r' . {*} \sqcap \exists r' , r'' . \mn{2^x}
      \sqcap  \exists \mn{one} . {=}_1 \sqcap \exists r, \mn{one}, t . {+} \sqcap \exists t , t' . \mn{2^x}
      \\
      &\sqcap  \exists f  \mn{torus} ,r'', u . \mn{div}
       \sqcap \exists u ,t'', \mn{tile} . \mn{mod}
      \sqcap  \exists \mn{tile} . {=}_i.
  \end{split}      
\end{gather*}

\noindent
Here, $r,r',r'', t, t', u, \mn{one}, \mn{torus}$, and \mn{tile} are
concrete features.  The \mn{torus} feature is the counterpart of the
\mn{darr} feature in the original reduction, i.e., it stores the
natural number that represents the tiling array. We can use the
$\mn{Tile}[i]$ concept in the obvious way inside the \mn{CheckHMatch},
\mn{CheckVMatch}, and \mn{Init2} concepts. The size of the resulting
reduction concept is polynomial in $n$ if the numbers $k$ appearing in
${=}_k$ predicates are coded in binary.  We thus obtain the following
theorem:
%
\begin{theorem}
  Let \Dmc be a concrete domain such that 
  %
  \begin{enumerate}
  \item $\mathbbm{N} \subseteq \Delta_\Dmc$, 
    
    
  \item $\Phi_\Dmc$ contains the predicates a predicate ${=}_k$ (for
    each $k \in \mathbbm{N}$), $\mn{2^x}$, $+$, $*$,  \mn{div},
    \mn{mod}
                                %
    with the following extensions
                                %
$$
\begin{array}[t]{rcl}
  ({=}_k)^\Dmc&=&\{k\}\\
  (\mn{2^x})^\Dmc \cap \{ (k,x) \mid k \in
       \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} &=& \{ (k, 2^k) \mid
       k \in \mathbbm{N} \}\\
  ({+})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
      \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} &=& \{
      (k_1,k_2,k_1+k_2) \mid k_1,k_2 \in \mathbbm{N} \}\\
      ({*})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
      \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} &=& \{
      (k_1,k_2,k_1\cdot k_2) \mid k_1,k_2 \in \mathbbm{N} \}\\
      

   (\mn{div})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
      \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} &=& \{
      (k_1,k_2,k_1\;\textnormal{div}\; k_2) \mid k_1,k_2 \in \mathbbm{N} \}\\

   (\mn{mod})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
      \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} &=& \{
      (k_1,k_2,k_1\;\textnormal{mod}\;  k_2) \mid k_1,k_2 \in \mathbbm{N} \}\\
\end{array}
$$




%     \begin{itemize}
%     \item for each $k \in \mathbbm{N}$, a predicate ${=}_k$ with
%       $({=}_k)^\Dmc=\{k\}$ such that the size of (the representation
%       of) ${=}_k$ is logarithmic in $k$,
 
%     \item $+$ with $({+})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
%       \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{
%       (k_1,k_2,k_1+k_2) \mid k_1,k_2 \in \mathbbm{N} \}$,
    
%     \item $*$ with $({*})^\Dmc \cap \{ (k_1,k_2,x) \mid k_1,k_2 \in
%       \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{ (k_1,k_2, k_1
%       \cdot k_2) \mid k_1,k_2 \in \mathbbm{N} \}$,
      
%     \item \mn{2^x} with $(\mn{2^x})^\Dmc \cap \{ (k,x) \mid k \in
%       \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{ (k, 2^k) \mid
%       k \in \mathbbm{N} \}$,
      
%     \item \mn{div} with $(\mn{div})^\Dmc \cap \{ (k_1,k_2,x) \mid
%       k_1,k_2 \in \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{
%       (k_1,k_2, k_1 \; \textnormal{div} \; k_2) \mid k_1,k_2 \in
%       \mathbbm{N} \}$,
      
%     \item \mn{mod} with $(\mn{mod})^\Dmc \cap \{ (k_1,k_2,x) \mid
%       k_1,k_2 \in \mathbbm{N} \mbox{ and } x \in \Delta_\Dmc \} = \{
%       (k_1,k_2, {k_1 \!\!\mod k_2}) \mid k_1,k_2 \in \mathbbm{N} \}$.
%       \end{itemize}
  \end{enumerate}

\noindent
  Then the satisfiability of \ALCOD-concepts is \NExpTime-hard.
\end{theorem}

\section{Reasoning Procedures}\label{reasoningprocedures}

This section is devoted to developing reasoning procedures for
DLs with concrete domains, nominals, and keys. We start
with devising a tableau algorithm that decides the satisfiability of
\ALCOKD-concepts w.r.t.\ Boolean key boxes. This algorithm yields
a \NExpTime upper complexity bound matching the lower bounds
established in Section~\ref{sect:alckdhard}. 

Then we consider the rather powerful description logic \SHOQKD. This
DL, which is an extension of \SHOQD
\cite{Horrocks-Sattler-01,Pan-Horrocks-02}, provides a wealth of
expressive means such as transitive roles, role hierarchies, nominals,
and qualifying number restrictions. Moreover, \SHOQKD is equipped with
a restricted variant of the concrete domain constructor and with key
boxes. We develop a tableau algorithm for deciding the satisfiability
of \SHOQKD-concepts w.r.t.~path-free key boxes. Due to the
restrictedness of \SHOQKD's concrete domain constructor, we can even
admit general rather than only Boolean key boxes. Again, the algorithm
yields a tight \NExpTime upper complexity bound.

\subsection{A Tableau Algorithm for \ALCOKD with Boolean Key Boxes}
\label{sect:alcokdtableau}

Tableau algorithms decide the satisfiability of the input concept (in
our case w.r.t.\ the input key box) by attempting to construct a model
for it. More precisely, a tableau algorithm starts with an initial
data structure induced by the input concept and then repeatedly
applies so-called completion rules to it.  This rule application can
be thought of as 
%making implicit knowledge explicit or as 
attempting to construct a model for the input concept.  Finally,
either the algorithm will find an obvious contradiction or it will
encounter a situation that is contradiction-free and in which no more
completion rules are applicable. In the former case, the input concept
is unsatisfiable, while it is satisfiable in the latter.

When devising a tableau algorithm for a description logic with
concrete domains but without committing to a \emph{particular}
concrete domain, it is commonly assumed that the concrete domain is
admissible, which implies decidability of the satisfiability of
\Dmc-conjunctions.  In the presence of keys, however, this is not
enough: if a \Dmc-conjunction is satisfiable, we also want to know
which of its variables take the same values in an arbitrary but fixed
solution. As an example, consider the concrete domain
$\mathsf{N}=(\mathbbm{N},\{ <_n \mid n \in \mathbbm{N} \})$ and the
$\mathsf{N}$-conjunction
\label{npage}
$$
c = {<}_2(v_1) \wedge {<}_2(v_2) \wedge {<}_2(v_3).
$$
                                
\noindent
Obviously, one solution $\delta$ for $c$ satisfies
$\delta(v_1)=\delta(v_2)$, another satisfies
$\delta(v_1)=\delta(v_3)$, and so on.
                                %
Our tableau algorithm uses such identity information passed from
the concrete domain reasoner since, in the presence of key boxes, it
can have an impact on the structure of the constructed model. For
example, this information  reveals the unsatisfiability of
$$
\exists R.A \sqcap \exists R.(\neg A \sqcap B) \sqcap \exists
R.(\neg A \sqcap \neg B) \sqcap \forall R.\exists g.{<}_2\text{
w.r.t.\ }(g \text{ keyfor } \top).
$$ 

\noindent
To formalize this requirement, we strengthen the notion of
admissibility into \emph{key-admissibility}. Since the tableau
algorithm developed in this section is non-determin\-is\-tic, we
formulate key-admissibility in a non-deterministic way.

\begin{definition}[Key-admissible]
\label{keyadm}
A concrete domain \Dmc is \emph{key-admissible} iff it satisfies the
following properties:
%
\begin{enumerate}

  \item $\Phi_\Dmc$ contains a name $\top_\Dmc$ for $\Delta_\Dmc$;
    
  \item $\Phi_\Dmc$ is closed under negation;

    
  \item there exists an algorithm that takes as input a
    \Dmc-conjunction $c$, returns \mn{clash} if $c$ is unsatisfiable,
    and otherwise non-deterministically outputs an equivalence
    relation $\sim$ on the set of variables $V$ used in $c$ such that
    there exists a solution $\delta$ for $c$ with the following
    property: $\text{ for all } v,v' \in V$
  $$
  \delta(v)=\delta(v') \text{ iff } v \sim v'.
  $$
  \end{enumerate}
                                %
\noindent
An algorithm showing the behaviour described in item~3 above is called
a \emph{\Dmc-tester}, and the equivalence relations $\sim$
are called \emph{concrete equivalences}.
                                %
We say that \emph{extended \Dmc-satisfiability is in NP} if there
exists a \Dmc-tester running in polynomial time.
\end{definition}

\noindent
Please note that key-admissibility is less esoteric than it might
seem: any concrete domain that is admissible and provides for an
equality predicate is also key-admissible. Due to admissibility, the
presence of an equality predicate implies that an inequality predicate
is also available. We can thus construct a \Dmc-tester from an
algorithm for \Dmc-satisfiability: when presented with a predicate
conjunction $c$, we simply ``guess'' an equivalence relation $\sim$ on
the set of variables used in $c$. Then we decide the (non-extended)
satisfiability of the conjunction $c \wedge \bigwedge_{v \sim v'}
{=}(v,v') \wedge \bigwedge_{v \not\sim v'} {\neq}(v,v')$, return
\mn{clash} if it is unsatisfiable and $\sim$ otherwise. The rather
weak condition that an equality predicate should be present is
satisfied by almost all concrete domains proposed in the literature
(see,
e.g.~\cite{Lutz-02e,Baader-Hanschke-91-TR,Kamp-Wache-96,Haarslev-et-al-98,Baader-Sattler-98}).


Throughout this chapter, we assume that any concrete domain is
equipped with an equality predicate. This assumption is w.l.o.g.\ 
since any \Dmc-conjunction using equality can be translated into an
equivalent one without equality by identifying variables according to
the stated equalities. This assumption must not be confused with what
was discussed in the previous paragraph: even if the concrete domain
\Dmc is admissible and its set of predicates is thus closed under
negation, this assumption does \emph{not} imply the presence of an
inequality predicate.

We need some more prerequisites before we can start the presentation
of the tableau algorithm: a concept is in \emph{negation normal form
(NNF)} if negation occurs only in front of concept names and nominals.
It is easily seen that, if the concrete domain \Dmc is admissible,
then every \ALCOKD-concept can be converted into an equivalent one in
NNF by exhaustively applying the rewrite rules displayed in
Figure~\ref{fig:nnfrules}. We use $\nneg C$ to denote the result of
converting $\neg C$ to NNF. A key box is in NNF if all concepts
occurring in key assertions are in NNF. In what follows, we generally
assume input concepts and key boxes to be in NNF.
                                %
\psfull
\begin{figure}[t]
  \begin{boxedminipage}[t]{\textwidth}
$$
\begin{array}{c}
\begin{array}{rclrcl}
    \neg(C \sqcap D) & \leadsto & \neg C \sqcup \neg D &
    \neg(C \sqcup D) & \leadsto & \neg C \sqcap \neg D  \quad\quad \neg\neg C  \leadsto  C \\
    \neg(\exists R . C) & \leadsto & \forall R. \neg C &
    \neg(\forall R . C) & \leadsto & \exists R. \neg C \\
\end{array}
\\[6mm]
\begin{array}{rcl}
  
    \neg (\exists u_1,\dots,u_n . P) &\leadsto& 
    \exists u_1,\dots,u_n . \overline{P} \sqcup u_1 {\uparrow} \sqcup \dots
    \sqcup u_n {\uparrow}
    \\
    \neg (g {\uparrow}) &\leadsto& \exists g . \top_\Dmc
\end{array}
\end{array}
$$
  \end{boxedminipage}
  \caption{The NNF rewrite rules.}
  \label{fig:nnfrules}
\end{figure}
\psdraft
                                %
Let $C$ be an \ALCOKD-concept and \Kmc a key box. We use
$\mn{sub}(C)$ to denote the set of subconcepts of $C$ (including $C$
itself) and $\mn{con}(\Kmc)$ to denote the set of concepts appearing
on the right-hand side of key assertions in \Kmc. For a set of
concepts $\Gamma$, $\mn{sub}(\Gamma)$ denotes the set $\bigcup_{C \in
\Gamma} \mn{sub}(C)$. Moreover, we write $\mn{cl}(C,\Kmc)$ as
abbreviation for the set
$$
\mn{sub}(C) \cup \mn{sub}(\mn{con}(\Kmc)) \cup \{ {\nneg} D \mid
D \in \mn{sub}(\mn{con}(\Kmc)) \}.
$$
                                
\noindent
We now start the presentation of the tableau algorithm by introducing
the underlying data structure.
%
\begin{definition}[Completion System]
  Let $\OA$ and $\OC$ be disjoint and countably infinite sets of
  \emph{abstract} and \emph{concrete nodes}.  A \emph{completion tree}
  for an \ALCOKD-concept $C$ and a key box \Kmc is a finite, labeled
  tree $\Tbf = (V_a,V_c,E,\Lmc)$ with nodes $V_a \cup V_c$ such that
  $V_a \subseteq \OA$, $V_c \subseteq \OC$, and all nodes from $V_c$
  are leaves. The tree is labeled as follows:
  %
  \begin{itemize}
    
  \item each node $a \in V_a$ is labeled with a subset $\Lmc(a)$ of
    $\mn{cl}(C,\Kmc)$;

  \item  each edge $(a,b)\in E$ with $a,b \in V_a$ is labeled with a
    role name $\Lmc(a,b)$ occurring in $C$ or \Kmc;
    
  \item each edge $(a,x)\in E$ with $a\in V_a$ and $x \in V_c$ is
    labeled with a concrete feature $\Lmc(a,x)$ occurring in $C$ or
    \Kmc.
  \end{itemize}
       
\noindent                         
  For $a \in V_a$, we use $\mn{lev}_\Tbf(a)$ to denote the depth at
  which $a$ occurs in \Tbf (starting with the root node on depth 0).
                                %
  A \emphindex{completion system} for an \ALCOKD-concept $C$ and a key
  box \Kmc is a tuple $(\Tbf, \Pmc, \prec, \sim)$, where
                                %
  \begin{itemize}
  \item $\Tbf=(V_a,V_c,E,\Lmc)$ is a completion tree for $C$ and \Kmc,
    
  \item \Pmc is a function mapping each $P \in \Phi_\Dmc$ of arity
    $n$ in $C$ to a subset of~$V_c^n$, 
    
  \item $\prec$ is a linear ordering of $V_a$ such that
    $\mn{lev}_\Tbf(a) \leq \mn{lev}_\Tbf(b)$ implies $a \prec b$, and

  \item $\sim$ is an equivalence relation on $V_c$.

  \end{itemize}
  
\noindent
Let $(V_a,V_c,E,\Lmc)$ be a completion tree. A node $b \in V_a$ is an
\emph{$R$-successor} of a node $a \in V_a$ if $(a,b) \in E$ and
$\Lmc(a,b)=R$, while a node $x \in V_c$ is a \emph{$g$-successor} of
$a$ if $(a,x) \in E$ and $\Lmc(a,x)=g$.  For a path $u$, the notion of
\emph{$u$-successor} is defined in the obvious way.
\end{definition}

\noindent

Intuitively, the relation $\sim$ records equalities between concrete
nodes found during the (non-deterministic) model construction process.
The recording is necessary since equalities between concrete nodes
can induce equalities between abstract nodes which, in turn, can imply
more equalities between concrete nodes. This can be seen in the
following example: assume the completion tree contains, for $i\in
\{1,2\}$, an abstract node $a_i$ with a concrete $g$-successor $x_i$
and a concrete $g'$-successor $y_i$. Now assume that the key box
contains $(g \keyfor \top)$, and that the \Dmc-tester returns $x_1
\sim x_2$. As a consequence, $a_1$ and $a_2$ represent the same
element and thus functionality of $g'$ implies that also $y_1$ and
$y_2$ represent the same (concrete) element.
To deal with such effects, we define an
equivalence relation $\approxa$ on abstract nodes and a second
equivalence relation $\approxc$ on concrete nodes.

\begin{definition}[$\approxa$ and $\approxc$ Relations]
\label{approx}
Let $S=(\Tbf,\Pmc,{\prec},{\sim})$ be a completion system for a
concept $C$ and a key box \Kmc with $\Tbf=(V_a,V_c,E,\Lmc)$, and let
$\approx$ be an equivalence relation on $V_a$.  For each $R \in \NR$,
a node $b \in V_a$ is an \emph{$R/{\approx}$-neighbor} of a node $a
\in V_a$ if there exists a node $c \in V_a$ such that $a \approx c$
and $b$ is an $R$-successor of $c$.  Similarly, for each $g \in \NcF$, 
a node $x \in V_c$ is a \emph{$g/{\approx}$-neighbor} of $a$ if there
exists a node $c \in V_a$ such that $a \approx c$ and $x$ is a
$g$-successor of $c$.  For paths $u$, the notion of
\emph{$u/{\approx}$-neighbor} is defined in the obvious way.
  
We define a sequence of equivalence relations ${\approxam 0} \subseteq
{\approxam 1} \subseteq \cdots$ on $V_a$ as follows:
$$
\begin{array}{rcl@{}l}
    {\approxam 0} &=& \{(a,a) \in V_a^2\} &\; \cup\\[.5mm]
&& \{ (a,b) \in V_a^2 \mid &\text{ there is an $N \in \NO$ such that }
    N \in \Lmc(a) \cap \Lmc(b) \} \\[1mm] %\; \cup \\[1mm]
    {\approxam{i+1}} &=& {\approxam{i}} \; \cup \\[.5mm]
    &&\{ (a,b) \in V_a^2 \mid &\text{ there is a $c \in \V_a$ 
    and an $f \in \NaF$ such that} \\[1mm]
    &&&\text{ $a$ and $b$ are $f/{\approxam i}$-neighbors of $c$} \} \; \cup \\[1mm]
    &&\{ (a,b) \in V_a^2 \mid &\text{ there is a } (u_1,\dots,u_n \text{ keyfor } C) \in \Kmc,\\[1mm]
    &&&\text{ $u_i/{\approxam i}$-neighbors $x_i$ of $a$ for $1 \leq i \leq n$, and} \\[1mm]
    &&&\text{ $u_i/{\approxam i}$-neighbors $y_i$ of $b$ for $1 \leq i \leq n$ } \\[1mm]
    &&&\text{ such that } C \in \Lmc(a) \cap \Lmc(b) \text{ and } x_i \sim y_i \text{ for } 1 \leq i \leq n\}.
  \end{array}
  $$

\noindent
  Finally, set ${\approxa} = \bigcup_{i \geq 0} {\approxam i}$. Then define
  $$
  \begin{array}{rcl}
   {\approxc} &=& {\sim} \cup \{ (x,y) \in V_c^2 \mid \text{ there is an $a \in V_a$ and a $g \in \NcF$ such that} \\[1mm]
  && \hspace*{3,2cm} \text{$x$ and $y$ are $g/{\approxa}$-neighbors of $a$} \}.
  \end{array}
  $$
\end{definition}


\noindent
This definition reflects the above mentioned tight coupling between
the concrete and abstract equalities: if the \Dmc-tester finds (or
guesses) that two concrete nodes are equal, the tableau algorithm may
use this to deduce (via the computation of $\approxa$ and $\approxc$)
even more equalities between concrete nodes.

Let \Dmc be a key-admissible concrete domain.  To decide the
satisfiability of an \ALCOKD-concept $C_0$ w.r.t.\ a Boolean key box
\Kmc (both in NNF), the tableau algorithm is started with the
\emphindex{initial completion tree}
$$
\Tbf_{C_0}=(\{a_0\},\emptyset,\emptyset, \{ a_0 \mapsto \{ C_0 \} \})
$$

\noindent
in the \emphindex{initial completion system}
$$
S_{C_0}=(\Tbf_{C_0},\Pmc_\emptyset,\emptyset,\emptyset),
$$

\noindent
where $\Pmc_\emptyset$ maps each $P \in \Phi_\Dmc$ occurring in $C_0$ to
$\emptyset$. We now introduce an operation that is used by the
completion rules to add new nodes to completion trees.
%
\begin{definition}[``+'' Operation]
  \label{plusop}
  An abstract or concrete node is called \emph{fresh} in a completion
  tree \Tbf if it does not appear in \Tbf.  Let
  $S=(\Tbf,\Pmc,{\prec},{\sim})$ be a completion system with
  $\Tbf=(V_a,V_c,E,\Lmc)$. We use the following notions:
  %
  \begin{itemize}
  \item Let $a \in V_a$, $b \in \OA$ fresh in \Tbf, and $R \in \NR$.
    We write $S + aRb$ to denote the completion system $S'$ that can
    be obtained from $S$ by adding $b$ to $V_a$ and $(a,b)$ to $E$ and
    setting $\Lmc(a,b)=R$ and $\Lmc(b)=\emptyset$. Moreover, $b$ is
    inserted into $\prec$ such that $b \prec c$ implies
    $\mn{lev}_\Tbf(b) \leq \mn{lev}_\Tbf(c)$.
   
  \item Let $a \in V_a$, $x \in \OC$ fresh in \Tbf and $g \in \NcF$.
    We write $S + agx$ to denote the completion system $S'$ that can
    be obtained from $S$ by adding $x$ to $V_c$ and $(a,x)$ to $E$ and
    setting $\Lmc(a,x)=g$.

  \end{itemize}
 
\noindent
When nesting the $+$ operation, we omit brackets, writing, for
example, $S + aR_1b + bR_2c$ for $(S + aR_1b) + bR_2c$.  Let $u=f_1
\cdots f_n g$ be a path. When $a \in V_a$ and $x \in \OC$ is fresh in
\Tbf, we use $S + aux$ to denote the completion system that is
obtained from $S$ by taking distinct nodes $b_1,\dots,b_n \in \OA$
which are fresh in \Tbf and setting
  %
  \begin{eqnarray*}
      S+aux &:=& S + a f_1 b_1 + \cdots + b_{n-1} f_n b_n + b_n g x.
  \end{eqnarray*}
\end{definition}

\noindent
Strictly speaking, the $S + aRb$ operation is non-deterministic since
we did not specify how precisely the node $b$ is inserted into
$\prec$.  However, since this is \emph{don't care} non-determinism, we
will view the ``+'' operation as being deterministic. 
%
\psfull
\begin{figure}[t!]
  \begin{center}
\begin{boxedminipage}[t]{\textwidth}
  \begin{center}
    \begin{tabular}{ll}
      \textbf{\Rand} & if $C_1 \sqcap C_2 \in \Lmc(a)$ and  $\{C_1,C_2\} \not \subseteq \Lmc(a)$
      \\
      & then $\Lmc(a) := \Lmc(a) \cup \{C_1,C_2\}$
      %
      \\[2mm]
      \textbf{\Ror} & if $C_1 \sqcup C_2 \in \Lmc(a)$ and $\{ C_1, C_2 \}
      \cap \Lmc(a) = \emptyset$
      \\
      & then $\Lmc(a) := \Lmc(a) \cup \{C\}$ for some $C \in \{C_1,C_2\}$
      %
      \\[2mm]
      \textbf{\Rex} & if $\exists R . C \in \Lmc(a)$ and there is no
      $R/{\approxa}$-neighbor $b$ of $a$ such that $C \in \Lmc(b)$,\\
      & then set $S := S + aRb$ for a fresh $b
      \in \OA$ and $\Lmc(b):= \{C\}$
      %
      \\[2mm]
      \textbf{\Rall} & if $\forall R . C \in \Lmc(a)$,
      $b$ is an $R/{\approxa}$-neighbor of $a$, and $C \notin \Lmc(b)$
      \\
      & then set $\Lmc(b) := \Lmc(b) \cup \{ C\}$
      %
      \\[2mm]
      \textbf{\Rexc} & if $\exists u_1,\dots,u_n . P \in \Lmc(a)$ 
      and there exist
      no $x_1, \dots, x_n \in V_c$ such that \\
      &\phantom{if} $x_i$ is $u_i$/$\approx_a$-neighbor of $a$ for $1 \leq i \leq n$ and
      $(x_1,\dots,x_n) \in \Pmc(P)$ \\
      & then set $S:=(S + au_1x_1 + \cdots + au_nx_n)$ with 
        $x_1,\dots,x_n \in \OC$ fresh  \\
      &\phantom{then} and $\Pmc(P) := \Pmc(P) \cup \{(x_1,\dots,x_n)\}$
      %
      \\[2mm]
      \textbf{\Rch} & if $(u_1,\dots,u_n \text{ keyfor } C) \in \Kmc$
      and there exist $x_1, \dots, x_n \in V_c$ such that \\
      &\phantom{if} $x_i$ is $u_i/{\approxa}$-neighbor of $a$ for $1 \leq i \leq n$ and
      $\{C, {\nneg}C\} \cap \Lmc(a) = \emptyset$
      \\
      & then set $\Lmc(a) := \Lmc(a) \cup \{ D \}$ for some $D \in \{C, {\nneg}C\}$
      %
      \\[2mm]
      \textbf{\Rp} & if $\Lmc(b) \not\subseteq \Lmc(a)$ and
      $a \in V_a$ is minimal w.r.t.\ $\prec$ such that $a \approxa b$
      \\
      & then set $\Lmc(a) := \Lmc(a) \cup \Lmc(b)$
    \end{tabular}
  \end{center}
  \end{boxedminipage}
  \end{center}
  %
    \caption{Completion rules for \ALCOKD.}
    \index{completion rules}
    \label{fig:rules}
\end{figure}
\psdraft
%

The completion rules can be found in Figure~\ref{fig:rules}.  Note
that the $\Ror$ and $\Rch$ rules are non-deterministic, i.e., they
have more than one possible outcome (this is true \emph{don't know}
non-determinism).  Some further remarks on the completion rules are in
order: the upper five rules are well-known from existing tableau
algorithms for \ALCD-concept satisfiability (see,
e.g.,~\citeR{Lutz-Diss}).  Only the use of $R/\approx_a$-neighbors and
$u/\approx_a$-neighbors in the rules \Rall, \Rex, and \Rexc deserves a
comment. Take for example \Rall: intuitively, if we have $a \approxa
b$ for two abstract nodes $a$ and $b$ of the completion tree, then $a$
and $b$ describe the same domain element of the constructed model (and
similarly for the $\approxc$ relation on concrete nodes).  Thus if $a
\approxa b$ and $c$ is an $R$-successor of $a$, then $c$ should also
be an $R$-successor of $b$.  However, since we want the completion
tree to be a tree, we do not make the latter successorship explicit.
To compensate for this, the \Rall rule talks about
$R/{\approxa}$-neighbors rather than about $R$-successors.

The lower two rules are necessary for dealing with key boxes. The \Rch
rule is a so-called ``choose
rule'' \cite{HollunderBaader-91,Horrocks-et-al-00c}: intuitively, it
guesses whether or not an abstract node $a$ satisfies $C$ if there
exists a key assertion $(u_1,\dots,u_n \text{ keyfor } C) \in \Kmc$
such that there are neighbors of $a$ for all the paths $u_i$. This is
necessary since both possibilities may have ramifications: if $a$
satisfies $C$, then it must be taken into account in the construction
of the relation $\approxa$; if $a$ does not satisfy $C$, then we must
deal with the consequences of it satisfying ${\nneg} C$ (e.g.\ in case
that $C$ is $\top$).

The \Rp rule deals with equalities between abstract nodes as
recorded by the $\approxa$ relation: since $a \approxa b$ means that
$a$ and $b$ describe the same node in the constructed model, their
node labels should be identical. It suffices, however, to choose one
representative for each equivalence class of $\approxa$ and make sure
that this representative's node label contains the labels of all its
 $\approxa$-equivalent nodes. As the representative, we use the node
that is minimal w.r.t.\ the ordering $\prec$, which has been
introduced solely for this reason. The \Rp rule does the appropriate
copying of node labels.

Let us now formalize what it means for a completion system to contain
a contradiction.
%
\begin{definition}[Clash]
\label{clash}
Let $S=(\mathbf{T}, \Pmc, \prec, \sim )$ be a completion system for a
concept~$C$ and a key box \Kmc with $\Tbf=(V_a,V_c,\prec,\sim)$. We
say that the completion system $S$ is \emph{concrete domain
  satisfiable} iff the conjunction
  $$
  \begin{array}{rcl}
  \zeta_S & = & \displaystyle\bigwedge_{P \text{ used in } C} \ 
  \bigwedge_{(x_1,\dots,x_n) \in \Pmc(P)} P(x_1,\dots,x_n) \wedge 
  \displaystyle\bigwedge_{x \approxc y} {=}(x,y)
  \end{array}
  $$

\noindent
  is satisfiable.  $S$ is said to contain a \emph{clash} iff
  
  \begin{enumerate}
    
  \item there is an $a \in V_a$ and an $A \in \NC$ such that $\{ A, \neg A\} \subseteq \Lmc(a)$,
    
  \item there are $a \in V_a$ and $x \in V_c$ such that $g{\uparrow}
    \in \Lmc(a)$ and $x$ is $g/{\approxa}$-neighbor of $a$,
    
  \item $S$ is not concrete domain satisfiable.

  \end{enumerate}
  
\noindent
  If $S$ does not contain a clash, $S$ is called
  \emphindex{clash-free}. $S$ is called \emphindex{complete} iff no
  completion rule is applicable to $S$.
\end{definition}

\noindent
The tableau algorithm is described in Figure~\ref{fig:alcokdalgo} in
pseudo-code notation.
%
\begin{figure}[t]
  \begin{center}
\begin{boxedminipage}[t]{\textwidth}
    \begin{center}
      \begin{minipage}{9cm}
    {\bf define procedure} $\mn{sat}(S)$ \\
    \ind{1} {\bf do} \\
    \ind{2} {\bf if} $S$ contains a clash {\bf then} \\
    \ind{3} {\bf return} \mn{unsatisfiable} \\
   \ind{2} {$\sim$} := $\mn{test}(\zeta_S)$ \\ 
   \ind{2} compute $\approxa$\\
    \ind{2} compute $\approxc$\\
    \ind{1} {\bf while} ${\sim} \neq {\approxc}$ \\
    \ind{1} {\bf if} $S$ contains a clash {\bf then} \\
    \ind{2} {\bf return} \mn{unsatisfiable} \\
    \ind{1} {\bf if} $S$ is complete {\bf then} \\
    \ind{2} {\bf return} \mn{satisfiable} \\
    \ind{1} $S':= $ the application of  a completion rule to $S$\\
    \ind{1} {\bf return} $\mn{sat}(S')$
      \end{minipage}
  \end{center}
  \end{boxedminipage}
  \end{center}
  %
  \caption{The \ALCOKD tableau algorithm.}
  \label{fig:alcokdalgo}
\end{figure}
%
In this figure, \mn{test} calls a \Dmc-tester as specified in
Definition~\ref{keyadm}. Let us say a few words about the while loop.
There obviously exist close relationships between the relations $\sim$
and $\approxc$ and the predicate conjunction $\zeta_S$:
%
\begin{itemize}
  
\item ${\sim} \subseteq {\approxc}$ (note that both $\approxa$ and
  $\approxc$ depend on $\sim$ and are thus recomputed in each step of
  the while loop);
  
\item by definition of $\zeta_S$ and \Dmc-tester, the result of
  $\mn{test}(\zeta_S)$ yields a relation containing $\approxc$ (and
  thus also~$\sim$).

\end{itemize}

\noindent
Using these facts, one may check that, in each step of the while loop,
new tuples are added to the $\sim$ relation, but none are deleted (see
the proof of Lemma~\ref{termlem2} in the appendix). The while loop is
needed because (i) $\approxa$ is defined using $\sim$, (ii),
$\approxc$ is defined using $\approxa$, and (iii) new concrete
equalities in $\approxc$ may then imply even more concrete and/or
abstract equalities, and so on.

A similar concrete-abstract interplay takes place in the course of
several recursion steps: equalities between concrete nodes provided by
the \Dmc-tester may make new rules applicable (for example \Rp and
\Rexc) which changes \Pmc and thus also $\zeta_S$.  This may
subsequently lead to the detection of more equalities between concrete
nodes by the \Dmc-tester, and so on. These considerations show
that, in the presence of keys, there exists a close interplay between
the concrete domain reasoner and the tableau algorithm, which is not
needed if keys are not present: without keys, it suffices to apply the
concrete domain satisfiability check only once after the completion
rules have been exhaustively applied~\cite{Baader-Hanschke-91}.

The detailed proof of termination, soundness, and completeness together
with a complexity analysis of the tableau algorithm defined in this
section is given in Appendix~\ref{ap1}.

\begin{theorem}\label{theo:alcokdtableau}
  Let \Dmc be a key-admissible concrete domain. If extended
  \Dmc-satisfiability is in \NP, then \ALCOKD-concept satisfiability
  w.r.t.\ Boolean key boxes is in \NExpTime.
\end{theorem}

\noindent
We should note that, in the way it is presented here, the algorithm
leaves considerable room for optimizations. One possible optimization
concerns the ``re-use'' of $f$-successors (for abstract features $f$):
for example, when applying the \Rex rule to a concept $\exists f . C
\in \Lmc(a)$, where $a$ already has an $f$-successor $b$, we could
simply add $C$ to $\Lmc(b)$ instead of adding a new $f$-successor $c$
and recording that $b \approxa c$. 

Another candidate for optimizations is the \mn{test} function. Recall
that this function takes a predicate conjunction $c$ with set of
variables $V$ and non-deterministically returns a concrete
equivalence, i.e., a relation $\sim$ such that there exists a solution
$\delta$ for $c$ with $v_i
\sim v_j$ iff $ \delta(v_i)=\delta(v_j)$ (see
Definition~\ref{keyadm}). It is not hard to devise an \ALCD-concept
that forces completion systems to have exponentially many concrete
nodes by slightly adapting well-known \ALC-concepts that require
models of exponential size~\cite{Halpern-Moses-92}. Hence, the size
of input conjunctions $c$ to \mn{test} can be exponential in the size
of the input concept. Even for trivial
\Dmc-conjunctions
$$
  c = \top_\Dmc(v_1) \wedge \cdots \wedge \top_\Dmc(v_k)
$$

\noindent
we have an exponential number of distinct concrete equivalences
$\sim$. Thus, the number of possible outcomes of a call to the
\mn{test} function may be \emph{double exponential} in the size of the
input concept.  Considering the above example, a natural response to
this problem is to require \mn{test} to return only
\emph{minimal} concrete equivalences: intuitively, an equivalence is
minimal if only those variables are equivalent whose equality is
enforced by the conjunction.

More precisely, $\sim$ is called \emph{minimal} if there exists no
concrete equivalence $\sim'$ such that $\{(x,y)\mid x \sim' y\} \subset \{(x,y)\mid x \sim y\}$.
%(i)~$x \sim' y$ implies $x \sim
%y$ and (ii) there are $x,y$ with $x \sim y$ and $x
%\not\sim' y$. 
We conjecture that restricting \mn{test} in this way
does not destroy the soundness and completeness of the tableau algorithm.
However, although this definitely is a worthwhile optimization, it
does not help to overcome the existence of doubly exponentially many
outcomes of \mn{test} in the worst case---at least not for all
concrete domains \Dmc: consider the concrete domain \Nsf from
Page~\pageref{npage} and conjunctions of the form
$$
  c_i = {<}_{i}(v_1) \wedge \cdots \wedge {<}_i(v_{2i}). 
$$
                                
\noindent
It is readily checked that, for each $i \geq 1$, the number of minimal
concrete equivalences for $c_i$ is exponential in $i$.  Moreover, it
is not hard to devise a concept $C_i$ of size logarithmic in $i$ that
leads to completion systems $S$ such that $\zeta_S=c_i$. Hence, there
are still doubly exponentially many possible outcomes of the \mn{test} function.

In the example just discussed, the exponential branching of \mn{test}
is clearly due to the discreteness of the natural numbers.  Indeed, if
we use a dense structure for defining concrete domains, it seems that
the restriction to minimal concrete equivalences can have the desired
effect, namely that the number of \mn{test}'s possible outcomes
becomes polynomial in the size of its input and thus exponential in
the size of the input concept.  For example, consider the concrete
domain \Qsf, which is defined as follows:
%
\begin{itemize}

\item $\Delta_\Qsf$ is the set $\mathbbm{Q}$ of rational numbers;
  
\item $\Phi_\Qsf$ contains unary predicates $\top_\Qsf$ and its
  negation $\bot_\Qsf$, unary predicates $=_q$ and $\neq_q$ for each
  $q \in \mathbbm{Q}$, binary comparison predicates $\{ <, \leq, =,
  \neq, \geq, > \}$, a ternary addition predicate $+$, and its
  negation $\overline{+}$ (all with the obvious semantics).

\end{itemize}

\noindent
It is readily checked that \Qsf is key-admissible (note that it
provides a binary equality predicate) and thus falls into our
framework.  We conjecture that there exists only one minimal concrete
equivalence for every $\Qsf$-predicate conjunction $c$: intuitively,
it seems possible to (inductively) determine a relation $\sim$ on the
set of variables $V$ used in $c$ such that (i)~$x \sim y$ implies that
$\delta(x) = \delta(y)$ for \emph{every} solution $\delta$ for $c$ and
(ii)~there exists a solution $\delta$ for $c$ such that $v \not\sim
v'$ implies $\delta(v) \neq \delta(v')$. Clearly, $\sim$ is a minimal
concrete equivalence. Moreover, due to (i) it is the only one.

\subsection{A Tableau Algorithm for \SHOQKD}\label{shoqkd}

Although \ALCOKD is a quite powerful DL, it lacks several expressive
means that can be found in most state-of-the-art description logic
systems such as \FaCT and
\RACER~\cite{Horrocks-98,Horrocks-et-al-00c,Haarslev-Moeller-01b}. In
this section, we consider the very expressive description logic
\SHOQKD which provides for concrete domains, key boxes, and nominals,
but also for many other means of expressivity such as transitive
roles, role hierarchies, qualifying number restrictions, and general
TBoxes.  Modulo some details, \SHOQKD can be viewed as the extension
of the DL \SHOQD with key boxes.  \SHOQD was proposed by Horrocks and
Sattler \citeyear{Horrocks-Sattler-01} (see
also~\citeR{Pan-Horrocks-02}) as a tool for ontology reasoning in the
context of the semantic
web~\cite{Berners-Lee-et-al-01,Baader-et-al-02b}.

One very important feature of \SHOQKD are so-called TBoxes, i.e.\ 
concept equations\footnote{Some TBox formalisms also allow for concept
  inclusions $C \sqsubseteq D$, but these can be re-written into
  equivalent equations, see Section 2.2.2.5 of
  \cite{Baader-et-al-01}.}  of the form $C \doteq D$ that are used as
a ``background theory'' in reasoning. Since it is well-known that
combining general TBoxes and the concrete domain constructor easily
leads to undecidability~\cite{Baader-Hanschke-92,Lutz-02f}, \SHOQKD
only offers a path-free variant of the concrete domain
constructor---i.e.\ only concrete features are admitted inside this
constructor rather than paths of arbitrary length. This restriction
indeed regains decidability
\cite{Haarslev-et-al-01,Horrocks-Sattler-01}.  Path-freeness of the
concrete domain constructor obviously renders abstract features
unnecessary, and thus this syntactic type is not available in \SHOQKD.

\subsubsection{The Description Logic \SHOQKD}\label{dlshoqkd}

Let us now define \SHOQKD in a formal way, starting with the syntax.
                                %
\begin{definition}[\SHOQKD Syntax] \label{def:shoqkdsyn}
  A \emph{role axiom} is either a \emph{role inclusion}, which is of
  the form $R \sqsubseteq S$ with $R,S \in \NR$, or a
  \emph{transitivity axiom} $\Tr(R)$ where $R \in \NR$.  A \emph{role
    box} \Rmc is a finite set of role axioms. Let $\sss$ be the
  reflexive-transitive closure of the role inclusions in \Rmc. 
                                %
  A role name $R$ is called \emph{simple} if $S \sss R$ implies
  $\Tr(S) \notin \Rmc$ for all role names $S$.  Let \Dmc be a concrete
  domain.  The set of \SHOQKD-concepts is the smallest set such that
  %
  \begin{itemize}
  
  \item every concept name and every nominal is a concept, and 
    
  \item if $C$ and $D$ are concepts, $R$ is a role name, $S$ a simple
    role name, $n$ and $k$ are natural numbers, $g_1,\dots,g_n$ are
    concrete features, and $P \in \Phi_\Dmc$ is a predicate of arity
    $n$, then the following expressions are also concepts:
    $$
    \neg C,~C \sqcap D,~C \sqcup D,~\exists R . C,~\forall R .
    C,~\qnrgeq k S C,~\qnrleq k S C,~\exists g_1,\dots,g_n.P,\text{
      and } g_1{\uparrow}.
  $$
  \end{itemize}

\noindent
  A \emph{concept equation} is an expression $C \doteq D$ with $C$ and
  $D$ concepts. A \emph{TBox} is a finite set of concept equations.
\end{definition}

\noindent
For \SHOQKD, we consider key boxes that differ in two aspects from the
ones we considered for \ALCOKD: in the following, we assume key boxes
to be path-free, but we admit complex concepts to occur in key
assertions.  Note that abstract features and paths do not occur in the
syntax of \SHOQKD---as will become clear after the semantics has been
defined, the former can be ``simulated'' by the more general number
restrictions $\qnrleq n R C$.  

As usual in description logics of the
\SHIQ/\SHOQ family, we require role names in number restrictions to be
simple since admitting arbitrary roles yields undecidability of
reasoning~\cite{Horrocks-et-al-00c,Horrocks-Sattler-01}.  If the
role box \Rmc is clear from the context, we will usually write
$\Tr(R)$ instead of $\Tr(R) \in \Rmc$.  We now introduce the semantics
of \SHOQKD and the relevant reasoning problems.
%
\begin{definition}[\SHOQKD Semantics]  \label{def:shoqkdsem}
  Interpretations $\Imc=(\Delta_\Imc, \cdot^\Imc)$ are defined as in
  Definition~\ref{def:semantics}, where the function $\cdot^\Imc$ is
  extended to the novel \SHOQKD-concepts as follows:
                                %
  \begin{gather*}
    \begin{split}
%       (\neg C)^\Imc &:= \Delta_\Imc \setminus C^\Imc \\
%       (C \sqcap D)^\Imc &:= C^\Imc \cap D^\Imc \\
%       (C \sqcup D)^\Imc &:= C^\Imc \cup D^\Imc \\
%       (\exists R . C)^\Imc &:= \{ d \in \Delta_\Imc \mid \{ e \mid
%       (d,e) \in R^\Imc \} \cap C^\Imc \neq \emptyset \}
%       \\
%       (\forall R . C)^\Imc &:= \{ d \in \Delta_\Imc \mid \{ e \mid
%       (d,e) \in
%       R^\Imc \} \subseteq C^\Imc \} \\
      {\qnrleq k R C}^\Imc &:= \{ d \in \Delta_\Imc \mid \sharp \{ e
      \mid (d,e) \in R^\Imc \} \leq k \}
      \text{ and}\\
      {\qnrgeq k R C}^\Imc &:= \{ d \in \Delta_\Imc \mid \sharp \{ e
      \mid (d,e) \in R^\Imc \} \geq k \}.
      \\
    %   (\exists g_1,\dots,g_n.P)^\Imc &:= \{ d \in \Delta_\Imc \mid
%       \exists x_1,\dots,x_n \in \Delta_\Dmc: g_i^\Imc(d)=x_i \mbox{
%         and } (x_1,\dots,x_n) \in P^\Dmc \}
%       \\
%       (g {\uparrow})^\Imc &:= \{ d \in \Delta_\Imc \mid g^\Imc(d)
%       \text{ undefined} \}.
    \end{split}
  \end{gather*}
  
\noindent
  Let \Imc be an interpretation. Then \Imc \emph{satisfies} a concept
  equation $C \doteq D$ if $C^\Imc = D^\Imc$. \Imc~is a \emph{model}
  of a TBox \Tmc if \Imc satisfies all concept equations in \Tmc.
  Similarly, \Imc satisfies a role inclusion $R \sqsubseteq S$ if
  $R^\Imc \subseteq S^\Imc$ and a transitivity axiom $\Tr(R)$ if
  $R^\Imc$ is a transitive relation. \Imc~is a \emph{model} of a role
  box \Rmc if \Imc satisfies all role inclusions and transitivity
  axioms in \Rmc.
  
  Let \Tmc be a TBox, \Rmc a role box, and \Kmc a key box.  A concept
  $C$ is \emph{satisfiable w.r.t.\ \Tmc, \Rmc, and \Kmc} iff $C$,
  \Tmc, \Rmc, and \Kmc have a common model. $C$ is \emph{subsumed by}
  a concept $D$ \emph{w.r.t.\ \Tmc, \Rmc, and \Kmc} (written $C
  \sqsubseteq_{\Tmc,\Rmc,\Kmc} D$) iff $C^\Imc \subseteq D^\Imc$ for
  all common models \Imc of \Tmc, \Rmc, and \Kmc.
\end{definition}

\noindent
Note that, due to the requirement that role names used inside number
restrictions should be simple, existential and universal value
restrictions are not just syntactic sugar: in contrast to number
restrictions, they can be used on \emph{all} roles.

It is well-known that, in many expressive description logics,
reasoning with TBoxes can be reduced to reasoning without
them~\cite{Schild-91,Horrocks-Sattler-01}: for \SHOQKD, a concept $C$
is satisfiable w.r.t.\ \Tmc, \Rmc, and \Kmc iff the concept
$$
\some RC \sqcap \forall R . \big( \bigsqcap_{D \doteq E \in \Tmc} D
\leftrightarrow E \big )  \sqcap \hspace{-0.5cm}\bigsqcap_{\text{
    \begin{tabular}[t]{c}
nominal $N$
    used\\ in $C$, \Tmc, or \Kmc    \end{tabular}}} \hspace{-0.5cm}\big ( \exists R . N \big )
$$

\noindent
is satisfiable w.r.t.~to $\Rmc'$, \Kmc, and the empty TBox, where $R$ is a
fresh role not appearing in $C$, \Rmc, and \Tmc, and
$$
\Rmc' := \Rmc \cup \{ \Tr(R) \} \cup \hspace{-0.5cm}\bigcup_{\text{\begin{tabular}[t]{c}role name $S$ used\\ in
    $C$, \Tmc, \Rmc, or \Kmc\end{tabular}}}\hspace{-0.5cm} \{ S \sqsubseteq R \}.
$$

\noindent
Since subsumption can be reduced to satisfiability as described in
Section~\ref{sect:dl}, in the following we will only consider 
satisfiability of concepts w.r.t.\ role boxes and key boxes, but
without TBoxes. We will also generally assume role boxes \Rmc to be
\emph{acyclic}, i.e.\ to satisfy the following condition: for each
role name $R$, there are no role names $R_1,\dots,R_k$ such that
$R=R_1=R_k$ and $R_i \sqsubseteq R_{i+1} \in \Rmc$ for $1 \leq i <k$.
It is not hard to see that this is not a restriction since cycles can be
eliminated: if $R_1,\dots,R_k$ is a cycle in \Rmc, then we have
$R_1^\Imc = \cdots = R_k^\Imc$ for all interpretations \Imc. Thus we
can simply remove the cycle from \Rmc and replace every occurrence of
$R_2,\dots,R_k$ in $C$, \Rmc, and \Kmc with~$R_1$,
and add $\Tr(R_1)$ if, before the cycle
elimination, we had $\Tr(R_i)$ for some $i$ with $1 \leq i \leq n$.

Before we turn our attention to the construction of a tableau
algorithm for \SHOQKD, let us comment on a few minor differences
between \SHOQKD as introduced here and the original version of \SHOQD
as described in~\cite{Horrocks-Sattler-01}. The main difference is
that our logic, like the extensions investigated
in~\cite{Haarslev-et-al-01,Pan-Horrocks-02}, allows $n$-ary predicates
while Horrocks and Sattler restrict themselves to unary predicates.
Moreover, \SHOQD as introduced in~\cite{Horrocks-Sattler-01} uses
\emph{concrete roles} rather than concrete features, the difference
being that concrete roles are not necessarily functional. Due to this
non-functionality, the original \SHOQD admits two variants $\exists T
. P$ and $\forall T .  P$ of the concrete domain constructor (where
$T$ is a concrete role and $P$ a unary predicate). In \SHOQKD, we can
simulate the universal variant by writing $\exists g . P \sqcup
g{\uparrow}$ since concrete features $g$ are interpreted as partial
functions and, in contrast to Horrocks and Sattler, we have the
undefinedness constructor $g{\uparrow}$ available. Except for the
$n$-ary predicates which provide important additional expressivity, we
view these deviations as minor ones since it is easy to see that they
do not affect decidability and complexity of reasoning.

\subsubsection{A Tableau Algorithm for \SHOQKD}\label{shoqkdtableaualgorithm}
\label{shoqkdtableau}

The basic intuitions of the \SHOQKD tableau algorithm are similar to
the \ALCOKD algorithm, with one exception: to deal with the various
expressive means of \SHOQKD, it is convenient to introduce a certain
abstraction of models, so-called \emph{tableaux}. The main difference
between tableaux and models is that, in tableaux, roles declared to be
transitive are not necessarily described by transitive relations.  We
show that there exists a tableau for a given concept and key box if
and only if they have a common model. The aim of the \SHOQKD algorithm
is then to construct a tableau for its input rather than trying to
construct a model. To do this, the algorithm employs completion
forests as its underlying data structure.

We first introduce tableaux. Let us start by discussing some
preliminaries.  As for \ALCOKD, we assume all concepts and key boxes
to be in NNF, i.e.\ negation occurs only in front of concept names and
nominals. We again use $\nneg C$ to denote the NNF of $\neg C$. The
additional NNF rewrite rules for \SHOQKD can be found in
Figure~\ref{fig:shoqkdnnfrules} and complete those given for \ALCOKD
in Figure~\ref{fig:nnfrules}.

\psfull
\begin{figure}[t]
  \begin{boxedminipage}[t]{\textwidth}
$$
\begin{array}{c}
%\begin{array}{rclrcl}
%    \neg(C \sqcap D) & \leadsto & \neg C \sqcup \neg D &
%    \neg(C \sqcup D) & \leadsto & \neg C \sqcap \neg D \\
%    \neg(\exists R . C) & \leadsto & \forall R. \neg C &
%    \neg(\forall R . C) & \leadsto & \exists R. \neg C \\
%    \neg\neg C & \leadsto & C &
%    \neg (g {\uparrow}) &\leadsto& \exists g . \top_\Dmc
%\end{array}
%\\[6mm]
\begin{array}{rcl}
    \neg\qnrgeq n R C  & \leadsto & \qnrleq {(n-1)} R C \text{ if $n\geq1$} \\
    \neg\qnrgeq 0 R C  & \leadsto & \bot \\
    \neg\qnrleq n R C  & \leadsto & \qnrgeq {(n+1)} R C \\
%    \neg (\exists g_1,\dots,g_n . P) &\leadsto& 
%    \exists g_1,\dots,g_n . \overline{P} \sqcup g_1 {\uparrow} \sqcup \dots
%    \sqcup g_n {\uparrow}
%    \\
\end{array}
\end{array}
$$
  \end{boxedminipage}
  \caption{The \SHOQKD NNF rewrite rules.}
  \label{fig:shoqkdnnfrules}
\end{figure}
\psdraft


For a concept $D$, role box \R, and key box \Kmc, we define
$$
\begin{array}{r@{\;}c@{\;}l}
\cl(D,\Kmc)&:=&\mn{sub}(D) \cup \mn{sub}(\mn{con}(\Kmc)) \cup \{ {\nneg} C \mid
C \in \mn{sub}(D) \cup \mn{sub}(\mn{con}(\Kmc)) \}\\[1mm]
\cl(D,\R,\Kmc)&:=&\cl(D,\Kmc) \cup \{\all RC\mid R\sss S \text{ and
}\all SC\in \cl(D,\Kmc) \}.
\end{array}
$$

\noindent
Obviously, the cardinality of $\cl(D,\R,\Kmc)$ is linear in the size
of $D$, \Rmc, and \Kmc. In what follows, we write $\NRDRK$ to denote
the set of role names occurring in $D$, \Rmc, or \Kmc, and $\NcFDK$ to
denote the sets of concrete features occurring in $D$ or \Kmc.  We are
now ready to define tableaux.
%
\begin{definition}[Tableau] \label{def:shof-tableau}
  Let $D$ be a \SHOQKD-concept in NNF, \R a role box, and \Kmc a
  path-free key box in NNF. A \emph{tableau} $T$ for $D$ w.r.t.\ \R
  and \Kmc is a tuple $(\S_a,\S_c,\Lmc,\Et,\Etc,\Pmc)$ such that
  %                                %
  \begin{itemize}

  \item $\mathbf{S}_a$, $\mathbf{S}_c$ are sets of \emph{abstract} and
    \emph{concrete individuals},

  \item $\Lmc:\mathbf{S}_a \rightarrow 2^{\cl(D,\R,\Kmc)}$ maps each
    abstract individual to a subset of $\cl(D,\R,\Kmc)$,
    
  \item $\Et: \S_a\times \S_a \rightarrow 2^{\NRDRK}$ maps pairs of
    abstract individuals to sets of roles,
    
  \item $\Etc: \S_a\times \NcFDK \rightarrow \mathbf{S}_c $ maps pairs of
    abstract individuals and concrete features to concrete individuals,

  \item $\Pmc$ maps each $n$-ary concrete predicate in
    $\cl(D,\R,\Kmc)$ to a set of $n$-tuples over $\S_c$, 

  \item there is an abstract individual $s_0 \in \S_a$ such that $D \in
    \Lmc(s_0)$, and

  \end{itemize}
       
\noindent
  for all $s,t \in \mathbf{S}_a$, $C,C_1,C_2\in \cl(D,\R,\Kmc)$, $R,S
  \in \NRDRK$, and for 
                                %
  \[
  S^T(s,C) := \{ t \in \S_a \mid S\in \Et\tuple s t \text{ and }
  C\in\Lmc(t)\},
  \]
                                %
  it is the case that:
                                %
\begin{description}
\item[\tabl 1] if $C \in \Lmc(s)$, then $\nneg C \notin \Lmc(s)$,
  
\item[\tabl 2] if $C_1 \sqcap C_2 \in \Lmc(s)$, then $C_1 \in \Lmc(s)$
  and $C_2 \in \Lmc(s)$,

\item[\tabl 3] if $C_1 \sqcup C_2 \in \Lmc(s)$, then $C_1 \in \Lmc(s)$ or $C_2 \in \Lmc(s)$,
  
\item[\tabl 4] if $R\in \Et\tuple s t$ and $R\sss S$, then $S\in
  \Et\tuple s t$, 

\item[\tabl 5] if $\all{R}{C} \in \Lmc(s)$ and $R\in \Et\tuple{s}{t}$,
  then $C \in \Lmc(t)$,
  
\item[\tabl 6] if $\some{R}{C} \in \Lmc(s)$, then there is some $t \in
  \mathbf{S}_a$ such that $R\in \Et\tuple{s}{t} $ and $C \in \Lmc(t)$,
  
  
\item[\tabl 7] if $\all{S}{C} \in \Lmc(s)$ and $R\in \Et\tuple{s}{t}$
  for some $R \sss S$ with $\Tr(R)$, then $\all{R}{C} \in \Lmc(t)$,

  
\item[\tabl 8] if $\atleastq nSC\in \Lmc(s)$, then $\sharp S^T(s,C)
  \geqslant n$,

  
\item[\tabl 9] if $\atmostq n S C \in \Lmc(s)$, then $\sharp S^T(s,C)
  \leqslant n$,

  
\item[\tabl{10}] if either $\atmostq n S C \in \Lmc(s)$ and $S\in
  \Et\tuple{s}{t}$ or $(g_1,\ldots,g_n \keyfor C) \in \Kmc$ and
  $\Etc(t,g_i)$ is defined for all $1\leq i \leq n$, then $ \{C, \nneg
  C\} \cap \Lmc(t) \neq\emptyset$,

\item[\tabl{11}] if $N \in \Lmc(s) \cap \Lmc(t)$, then $s=t$,
  
\item[\tabl{12}] if $\exists g_1,\ldots,g_n.P\in \Lmc(s)$, then there
  are $x_1,\ldots,x_n\in \S_c$ with $\Etc(s,g_i)=x_i$ and
  $(x_1,\ldots,x_n) \in \Pmc(P)$,
  
\item[\tabl{13}] $\bigwedge_{P\text{ used in
  }D,\Kmc}\bigwedge_{(x_1,\ldots,x_n) \in \Pmc(P)} P (x_1,\ldots,x_n)
  \wedge \bigwedge_{x\neq y}x\neq y$ is satisfiable,
  
\item[\tabl{14}] if $(g_1,\ldots,g_n \keyfor C) \in \Kmc$, $C\in
  \Lmc(s)\cap \Lmc(t)$, and $\Etc(s,g_i)= \Etc(t,g_i)$ for all $1\leq i
  \leq n$, then $s=t$,

\item[\tabl{15}] if $g{\uparrow} \in \Lmc(s)$, then $e(s,g)$ is undefined.

\end{description}
\end{definition}

\noindent
Note that the predicate conjunction in \tabl{13} uses a binary
inequality predicate. In general, we do not require the concrete
domain \Dmc to be equipped with such a predicate and thus this
predicate conjunction is not necessarily a \Dmc-conjunction. 
%
However, it is nevertheless ``safe'' to use \tabl{13} in the given
form since tableaux are only used in proofs and we do not need a
concrete domain reasoner that is capable of deciding the
satisfiability of this conjunction.  The following lemma, whose proof
is provided in Appendix~\ref{ap2}, shows that our definition of
tableaux provides an adequate abstraction of models.

\begin{lemma}\label{lem:shof-tableau-sat-criterion}
  Let $D$ be a \SHOQKD-concept in NNF, \Rmc a role box, and \Kmc a key
  box in NNF. Then $D$ is satisfiable w.r.t.\ \R and \Kmc iff $D$ has
  a tableau w.r.t.\ \R and \Kmc.
\end{lemma}

\noindent
Given Lemma~\ref{lem:shof-tableau-sat-criterion}, in order to
decide satisfiability of \SHOQKD-concepts w.r.t.\ role and key boxes,
we may use a (tableau) algorithm that tries to construct a tableau for
the input. In the following, we will describe such an algorithm in
detail. 

As in the previous section, the algorithm works on completion systems.
However, in the case of \SHOQKD the core component of completion
systems is a completion forest rather than a completion tree. The
reason for this is that some completion rules remove nodes and edges
from the completion system and in this way can disconnect one tree
into two subtrees.

\begin{definition}[Completion System]\label{def:shof-tableau-algorithm}
  Let $D$ be a \SHOQKD-concept in NNF, $\R$ a role box, and \Kmc a
  path-free key box in NNF. For each concept $\qnrgeq n R C \in
  \cl(D,\Rmc,\Kmc)$ and $1 \leq i \leq n$, we reserve a concept name
  $A^{nRC}_i$ not appearing in $\cl(D,\Rmc,\Kmc)$ and define 
  an \emph{extended closure} 
    $$
   {\cl}^+(D,\R,\Kmc):=\cl(D,\R,\Kmc)
    \cup\{A^{nRc}_1,\ldots,A^{nRc}_n \mid \atleastq nRC\in
    \cl(D,\R,\Kmc)\}.
$$

\noindent
    Let \OA and \OC be disjoint and countably infinite sets of
    \emph{abstract} and \emph{concrete nodes}.  A \emph{completion
      forest} for $D$, $\R$, and \Kmc is a finite forest
   %
  $\Fbf =(V_a,V_c,E,\Lmc)$
                                %  
  with nodes $V_a \cup V_c$ such that $V_a \subseteq \OA$, $V_c \subseteq \OC$,
  and all nodes from $V_c$ are leaves. The forest is labelled as follows:

  \begin{itemize}
    
%  \item there is a node $s_0 \in V_a$ such that $D \in \Lmc(s_0)$,
    
  \item each node $a \in V_a$ is labelled with a subset $\Lmc(a)$ of
    $\cl^+(D,\R,\Kmc)$,
 
  \item each edge $(a,b)\in E$ with $a,b\in V_a$ is labeled with a
    non-empty set of role names $\Lmc(a,b)$ occurring in $D$, $\R$, or
    \Kmc, and
  \item each edge $(a,x)\in E$ with $a\in V_a$ and $x\in V_c$ is
    labeled with a concrete feature $\Lmc(a,x)$ occurring
    in $D$, $\R$, or \Kmc. 
  \end{itemize}
  
\noindent
  A \emph{completion system} for $D$, $\R$, and \Kmc is a tuple $S
  =(\Fbf,\Pmc,\sim_c,\prec)$ such that

  \begin{itemize}
    
  \item $\Fbf =(V_a,V_c,E,\Lmc)$ is a completion forest for
    $D$, \Rmc, and \Kmc,

  \item $\Pmc$ maps each $n$-ary concrete predicate  in
    $\cl(D,\Rmc,\Kmc)$ to a set of $n$-tuples in $V_c$, 
    
%  \item $\sim_a$ is an equivalence relation on $\S_a$, 
    
  \item $\simc$ is an equivalence relation on $V_c$, and

%  \item $\ndoteq$ is a symmetric relation on $\S_a$, and
    
  \item $\prec$ is a linear ordering on $V_a$.

  \end{itemize}

\noindent
  A node $t\in V_a$ is called an $R$-\emph{successor} of a node $s\in
  V_a$ if, for some $R'$ with $R'\sss R$, we have $R'\in
  \Lmc\tuple{s}{t}$. A node $x \in V_c$ is called a \emph{$g$-successor}
  of a node $s \in V_a$ if $\Lmc\tuple{s}{x} = g$. Finally, we write
  $s \ndoteq t$ if $s$ and $t$ are $R$-successors of the same node and
  there is some $A_i^{nRC}\in \Lmc(s)$ and $A_j^{nRC}\in \Lmc(t)$ with
  $i\neq j$.
  \end{definition}

\noindent
Some remarks are in order here.  Firstly, in contrast to the \ALCOKD
case, the relation $\prec$ is no longer required to respect the level
of a node. This is due to the fact that (a) we have to enforce
termination artificially and the mentioned property of $\prec$ was
used to ensure ``automatic'' termination, and (b) the level of a node
might change since a node might become a root node because some
completion rules will remove nodes and edges.
  
Secondly, the relation $\simc$ will be returned by a \Dmc-tester, and
is used to compute a relation $\approxa$ which is then used by the
tableau algorithm. However, we do not need to compute the relation
$\approxc$ from $\approxa$ as in the \ALCOKD case since all concepts and
key boxes are assumed to be path-free.
  
  Thirdly, the new concept names $A_i^{nRC}$ will be used to ensure
  that successors of a node $x$ generated for some $\atleastq nRC\in
  \Lmc(x)$ will not be merged later due to a concept $\atmostq
  {n'}R{C'}\in \Lmc(x)$: each generated successor is labelled with a
  different concept $A_i^{nRC}$; since merging two nodes means
  unifying their node labels, it then suffices to disallow the
  occurrence of distinct concepts $A_i^{nRC}$ in the same node label
  through a suitable definition  of ``clash''.
%
%---neither by the completion rules,
%  nor when we construct a tableau. Intuitively, we construct a finite,
%  cyclic tableau for a complete and clash-free completion system, and
%  we re-use nodes: sometimes, instead of having an edge to an
%  $R$-successor $y$ of $x$, we will have an edge to ``a node $z$
%  similar to $y$''. Now, if a node $z$ could be ``similar'' to two
%  $R$-successor $y_1$, $y_2$ of $x$, we might not have enough
%  $R$-successors of $x$ to satisfy a restriction $\atleastq nRC\in
%  \Lmc(x)$.


% % THIS FOOTNOTE DOES NOT SUFFICE SINCE THE READER DOES NOT EVEN KNOW
% % WHAT BLOCKING IS---LEAVE ALONE AN INTUITION FOR WHY TWO NODES MUST
% % NOT BE BLOCKED BY THE SAME NODE (which is, in general, not even true)
% %
%   \footnote{Please note that using the standard explicit
%     inequality relation on nodes as usual is not a solution for
%     \SHOQKD: we will build a \emph{finite} model from a clash-free and
%     complete completion forest, and must thus avoid that two
%     ``different'' nodes are blocked by the same node.}

Since \SHOQKD provides for transitive roles, we need some
cycle-detection mechanism in order to guarantee termination of our
algorithm: roughly speaking, if we encounter a node which is ``similar''
to an already existing one, then this node does not need to be further
explored. Speaking in terms of~\cite{Horrocks-et-al-00c,Baader-Sattler-00}, we employ a mechanism
called \emph{subset blocking}.
                                %
\begin{definition}[Blocked]
  Let $\preceq$ be the reflexive closure of $\prec$.
                                %
  A node $t\in V_a$ is \emph{blocked by} a node $s\in V_a$ if
  $\Lmc(t)\subseteq \Lmc(s)$, and $s\preceq s'$, for all $s'$ with
  $\Lmc(t)\subseteq \Lmc(s')$.
\end{definition}

\noindent
Note that, unlike to what is done, e.g.,\ 
in~\cite{Horrocks-et-al-00c}, the blocking node is not necessarily an
ancestor of the blocked node, but can be anywhere in the forest. It
may even be that blocked nodes have unblocked successors. This
modification is used later to obtain a \NExpTime upper bound. 
  
To decide the satisfiability of an \ALCOKD-concept $D$ w.r.t.\ a role
box \Rmc and a path-free key box \Kmc (where $D$ and \Kmc are in NNF),
the tableau algorithm is started with the \emphindex{initial
completion system}
$$
\begin{array}[t]{rcl}
S_{D}&=&(\Fbf_{D},\Pmc_\emptyset,\emptyset,\emptyset), \text{ where }\\
\Fbf_{D}&=&(\{s_0\},\emptyset, \emptyset, \{ s_0 \mapsto \{ D
\}\})\text{ and }\\
\Pmc_\emptyset & & \text{ maps each }P \in \Phi_\Dmc \text{ occurring in $D$ and
\Kmc to $\emptyset$}.
\end{array}
$$

\noindent
Then the algorithm repeatedly applies completion rules. Before the
actual rules are given, we introduce some new notions: % we use
% $S^\Fbf(s,C)$ to denote the set
% $$
% \{ t \in \S_a \mid t\text{ is an $S$-successor of $s$ in \Fbf and }
% C\in\Lmc(t)\}.
% $$
%
\noindent
firstly, we define the equivalence relation $\approxa$ over $V_a$ as
follows: $s \approxa t$ if one of the following conditions is
satisfied:
                                %
\begin{itemize}
  \item $N\in \Lmc(s)\cap \Lmc(t)$ for some nominal $N$ or
  \item $(g_1\ldots,g_n\keyfor C) \in \Kmc$, $C\in \Lmc(s)\cap
    \Lmc(t)$, and there are $x_i, y_i$ such that $g_i\in E(s,x_i) \cap
    E(t,y_i)$ and $x_i \simc y_i$ for $1\leq i \leq
    n$.
\end{itemize}

\noindent
Intuitively, two abstract nodes related via the $\approxa$ relation
describe the same individual in a tableau. 

%Note that $\approxa$ might change after each rule
%application. However, as mentioned above, we do not use the $\approxa$
%relation to compute a relation $\approxc$ as we have done in the
%previous section for \ALCOKD.  Intuitively, we do not need $\approxc$
%since, if $s \approxa t$, then we only ``keep'' the one smaller w.r.t.
%$\prec$ and hence do not care if both $s$ and $t$ have a $g$-successor
%for a concrete feature $g$.

Secondly, we use the following abbreviations in the formulation of the
rules (written in italic):
%
\begin{itemize}
  
\item To \emph{remove an abstract node $s$ and all its incoming and
  outgoing edges}, remove $s$ from $V_a$ and each $(s,t)$ and $(t,s)$
  from $E$ for all $t \in V_a\cup V_c$.
  
\item \emph{Adding a $g$-successor} of an abstract node $s$ means
  doing nothing if there exists a $g$-successor $x \in V_c$ of $s$
  and, otherwise, adding $E(s,x)= g$ for some $x\in \OC$ that does not
  yet occur in the completion forest.
  
\item To \emph{update the relation $\simc$}, a \Dmc-tester is asked to
  decide the satisfiability of the \Dmc-conjunction
  $$\zeta_S := \bigwedge_{\scriptstyle P\text{ used in}D,\Kmc \atop \scriptstyle
    (x_1,\ldots,x_n)\in \Pmc(P)} P(x_1,\ldots,x_n) \wedge \bigwedge_{x
    \sim_c y} x= y$$ and returns, in case that this conjunction is
  satisfiable, an ``updated'' concrete equivalence $\simc$ as defined
  in Definition~\ref{keyadm}.

\end{itemize}
%
Concerning the predicate conjunction used in updates, recall that we 
can w.l.o.g.\ assume the concrete domain to contain an equality predicate
as discussed after Definition~\ref{keyadm}.


The completion rules are given in Figure~\ref{table:shoq}. We generally
assume that new nodes $x$ are introduced into the completion forest such
that $y \prec x$ for all already existing nodes $y$.
%
\begin{figure*}[p!]
  \begin{center}\leavevmode
    \framebox[\textwidth]{\begin{tabular}{@{}l@{\hspace*{4mm}}l@{}}
      \Rand & if $C_1\sqcap C_2 \in\Lmc(s)$, $s$ is not
         blocked, and $\{C_1,C_2\}\not\subseteq \Lmc(s)$,
      \\
                                %
      & then  $\Lmc(s) := \Lmc(s)\cup\{C_1,C_2\}$\\[1ex]


      \Ror & if $C_1\sqcup C_2 \in\Lmc(s)$, $s$ is not
         blocked, and $\{C_1,C_2\}\cap\Lmc(s) = \emptyset$,
      \\
                                %
      & then $\Lmc(s) := \Lmc(s)\cup\{C\}$ for some $C\in
      \{C_1,C_2\}$\\[1ex]
                                %
      \Rex & if  $\some{R}{C} \in \Lmc(s)$,  $s$ is not blocked, and
      $s$ has no $R$-successor $t$ with $C\in \Lmc(t)$ \\
                                %
      & then create a new node  $t$  such that $t' \prec t$ for all $t' \in V_a$ \\
      & \phantom{then} and set $E
      \tuple{s}{t}:=\{R\}$ and $\Lmc(t):=\{C\}$ \\[1ex] 
                                %
      \Rgeq & if   $\atleastq n S C \in \Lmc(s)$, $s$ is not
      blocked, and there are no $n$ $S$-successors \\ 
      & \phantom{if} $t_1,\dots,t_n$
      of $s$ with $C \in\Lmc(t_i)$ and $t_i \ndoteq t_j$ for $1
      \leq i < j \leq n$, \\ 
      & then create $n$ new nodes $t_1,\dots,t_n$ s.t.\ $t' \prec t_i$ for $1 \leq i \leq n$ and  all $t' \in V_a$, \\
      & \phantom{then}
      and set $E \tuple s {t_i} := \{S\}$ and $\Lmc(t_i) :=
      \{C,A_i^{nSC}\}$ for $1 \leq i \leq n$\\[1ex] 
                                %
      \Rleq & if $\atmostq n S C\in\Lmc(s)$, $s$ is not blocked, 
                                %
        $s$  has $n+1$ $S$-successors $t_0,\ldots,t_n$ \\
        & \phantom{if} with $C\in\Lmc(t_i)$ for $0\leq i \leq n$, \\
       & then choose $i,j$ such that $t_i \prec t_j$, 
         set $\Lmc(t_i) := \Lmc(t_i) \cup \Lmc(t_j)$, \\
       & \phantom{then} $\Lmc(s,t_i) := \Lmc(s,t_i) \cup \Lmc(s,t_j)$, \emph{ and 
       remove $t_j$ and all its incoming} \\
     &\phantom{then} \emph{and outgoing edges} \\[1ex]
                                %
     \Rexco & if $\exists g_1,\ldots, g_n.P\in \Lmc(s)$, $s$ is not
      blocked,  and\\ & \phantom{if} there are
      no $g_i$-successors $x_i$ with $(x_1,\ldots,x_n)\in \Pmc(P)$ \\
      & then \emph{add a $g_i$-successor of $s$} for each $1\leq i
      \leq n$,\\ 
      & \phantom{then}for $y_i$ the $g_i$-successor of $s$, add
      $(y_1,\ldots,y_n)$ to 
      $\Pmc(P)$,  and \\
      & \phantom{then}\emph{update} $\sim_c$\\[1ex] 
                                %
      \Rall & if  $\all{R}{C} \in \Lmc(s)$, $s$ is not
      blocked, and \\ 
      & \phantom{if} there is an $R$-successor $t$ of $s$ with $C \notin
      \Lmc(t)$,  \\ 
      & then  $\Lmc(t) := \Lmc(t) \cup \{C\}$ \\[1ex]
                                %
      \Rallplus & if $\all{S}{C} \in \Lmc(s)$,  $s$ is not
      blocked, there is some $R$ with \\ & \phantom{if} $\Tr(R)$ and
      $R\sss S$,  
      and an  $R$-successor $t$ of $s$ with $\all{R}{C}
      \notin \Lmc(t)$,  \\ 
      & then $\Lmc(t) := \Lmc(t) \cup \{\all{R}{C}\}$\\[1ex]
                                %
      \Rch & if $s$ is an $S$-successor of $s'$ and
      $\atmostq nSC \in \Lmc(s')$ or \\
      & \phantom{if} $s$ has $g_i$-successors $x_i$  for all $1\leq i
      \leq n$ and $(g_1,\ldots g_n \keyfor C) \in \Kmc$ and\\
      & \phantom{if} $s$ is not blocked and $\{ C,\nneg C\}
      \cap  \Lmc(s)= \emptyset$, \\
      & then  $\Lmc(s) := \Lmc(s) \cup \{E\}$
      for some $E \in \{C,\nneg C \}$\\[1ex]
      
                        %
      \Rsima & if $s \approxa t$, $\Lmc(t) \not\subseteq \Lmc(s)$,
      $s\prec t$, and $s$ is not blocked,\\
      & then set $\Lmc(s) := \Lmc(s) \cup \Lmc(t)$
      \end{tabular}
      }
    \caption{The completion rules for
    \SHOQKD.}\label{table:shoq} \vspace{-0.6cm}
  \end{center}
\end{figure*}
%
\noindent
Before further describing the tableau algorithm, we comment on
the completion  rules. The rules \Ror, \Rleq, \Rexco, and \Rch are
non-deterministic, i.e., their application has more than one possible
outcome. For the \Rexco rule, this is due to the update operation
performed on $\simc$ using the \Dmc-tester: as discussed at the end of
Section~\ref{sect:alcokdtableau}, computing a concrete equivalence for
a given \Dmc-conjunction may result in a high degree of
non-determinism. Please note that, in contrast to \ALCOKD, we now only
need to call the \Dmc-tester in this rule---and not after each rule
application.

Next, the \Rsima rule takes care of abstract nodes related via
$\approxa$. Since all the nodes from a $\approxa$-equivalence class
denote the same individual, we choose only one representative whose
node label contains the labels of all other nodes in the class. This
representative simply is the $\prec$-minimal node of the equivalence
class and the \Rsima rule performs the appropriate copying of node
labels.

The \Rleq rule is the only rule to remove nodes and edges: it removes
a surplus $R$-successor $t$ of a node $s$ with $\atmostq nRC\in
\Lmc(s)$. Since the subtree below $t$ is not removed, $t$'s successors
are new, additional root nodes. This behavior is the reason why we
work on a completion forest.

As in the \ALCOKD case, the tableau algorithm stops applying rules
if it finds an obvious contradiction, a ``clash'', or if no more
completion rules are applicable.
                                %
\begin{definition}[Clash]
  Let $S =(\Fbf,\Pmc,\sim_c,\prec)$ be a completion system for $D$,
  \Rmc and \Kmc, and $\Fbf =(V_a,V_c,E,\Lmc)$. Then $S$ is said
  to contain a \emph{clash} if one of the following conditions
  applies:
                                %
  \begin{enumerate}
  \item[\clash 1] for some concept name $A \in \NC$ and some node $s
    \in V_a$, $\{A, \neg A\} \subseteq \Lmc(s)$;
    
  \item[\clash 2] the \Dmc-conjunction $\zeta_S$ defined above is not
    satisfiable;
    
  \item[\clash 3] $s\ndoteq s$ for some $s\in V_a$;
    
  \item [\clash 4] for some $s \in V_a$ and $g \in \NcF$, we have
    $g{\uparrow} \in \Lmc(s)$ and $s$ has a $g$-successor.

  \end{enumerate}
  A completion system not containing a clash is called
  \emph{clash-free}.  The completion system is \emph{complete} if % it
  %contains a clash or if 
  none of the completion rules is applicable.
\end{definition}

\noindent
Due to the simplicity of the algorithm, we refrain from describing it
in pseudo-code notation: the algorithm starts with the initial
completion system and then repeatedly applies the completion rules,
checking for clashes after each rule application.  If a clash is
detected, it returns \mn{unsatisfiable}. If a complete and clash-free
completion system is found, then the algorithm returns
\mn{satisfiable}. Note that, since some of the completion rules are
non-deterministic, the algorithm is also non-deterministic.

Details of the proof of termination, soundness, and completeness are
given in Appendix~\ref{ap2}. Unfortunately, we have to leave the
complexity of the algorithm as an open problem: it is not hard to
prove that it runs in double exponential time, but it is not clear
whether exponential time also suffices. However, we can still use the
algorithm to obtain a tight complexity bound for \SHOQKD: the
following corollary is an easy by-product of the correctness proofs
(for a proof see again Appendix~\ref{ap2}).
%
\begin{corollary}
  If a \SHOQKD-concept $D$ is satisfiable w.r.t.\ a role box \Rmc and
  a path-free key box \Kmc, then $D$ is satisfiable w.r.t.\ \Rmc and
  \Kmc in a model of size at most $|\Delta_\Imc| \leq 2^m$ for $m=\#
  \cl^+(D, \R, \Kmc)$.
\end{corollary}
%
\noindent
Thus the following is an alternative algorithm for deciding
satisfiability of a \SHOQKD-concept $D$ w.r.t.\ a role box \Rmc and a
path-free key box \Kmc: first, guess an interpretation \Imc with
cardinality of $\Delta_\Imc$ bounded by $2^m$, using placeholder
variables from $\OC$ instead of concrete values in the interpretation
of concrete features. Let $V_c$ be the set of variables from $\OC$
occuring in \Imc. Additionally guess an ``interpretation'' \Pmc for
the concrete domain predicates: just as in completion forests, \Pmc
maps each $n$-ary concrete predicate used in $D$ or \Kmc to an $n$-ary
relation on $V_c$.  Then perform standard (polynomial-time) model
checking to ensure that \Imc is a model of $D$. In doing this, treat
concepts of the form $\exists g_1,\ldots,g_n.P$ using the
interpretation of predicates \Pmc. It is easily checked in polynomial
time that \Imc is also a model of \Rmc and \Kmc---for the latter,
assume that all placeholder variables stand for different values.
Finally, use the concrete domain \Dmc-tester to check whether the
conjunction
%
$$
  \bigwedge_{\scriptstyle P\text{ used in}D,\Kmc \atop \scriptstyle
  (x_1,\ldots,x_n)\in \Pmc(P)} P(x_1,\ldots,x_n)
$$
%
is satisfiable. Answer ``yes'' if it is and ``no'' otherwise.
%
Since this algorithm can clearly be implemented
in \NExpTime provided that there is a \Dmc-tester running in
non-deterministic polynomial time, we obtain the following:
%                                
\begin{theorem}\label{theo:shoqkdtableau}
  Let \Dmc be a key-admissible concrete domain such that extended
  \Dmc-satisfiability is in \NP, then \SHOQKD-concept satisfiability
  w.r.t.\ TBoxes, role boxes, and path-free key boxes is in
  \NExpTime.
\end{theorem}

\section{Conclusion}\label{conclusions}

In this paper, we have identified key constraints as an interesting
extension of description logics with concrete domains. Starting from
this observation, we introduced a number of natural description logics
and provided a comprehensive analysis of the decidability and
complexity of reasoning. The main observation of our investigations is
that key boxes can have dramatic consequences on the complexity of
reasoning: for example, the \PSpace-complete DL \ALCD becomes
\NExpTime-complete if extended with path-free, unary, Boolean key
boxes and undecidable if extended with path-free, unary, non-Boolean
key boxes. Thus the effect of our key boxes on the complexity are
quite different from the effect of key assertions where only abstract
features are allowed~\cite{Calcanese-et-al-00c}:
these abstract key assertions can be said to be ``for free'' since
they do not increase the complexity for expressive description logics.

We show that the restriction to Boolean key boxes (in the
\ALCOKD case) and to path-free key boxes (in the \SHOQKD case) yield
decidabile and \NExpTime-complete reasoning problems. 
We selected \ALCD and \SHOQD as the basis for our analysis since, in
our opinion, these are the most fundamental description logics with
concrete domains. Going one step further, it would be interesting to
combine key boxes with other extensions of concrete domains, such as
the ones presented by Lutz~\citeyear{Lutz-02e,Lutz-02f}. To name
only one possibility, the extension of both \ALCOKD and \SHOQD with
inverse roles seems to be a natural idea. Note that inverse roles
interact with several of the available means of expressivity: while
\ALC with inverse roles is \PSpace complete~\cite{Horrocks-et-al-99},
\ALCO with inverse roles is \ExpTime-complete~\cite{Areces-et-al-99} and
\ALCD with inverse roles even \NExpTime-complete~\cite{Lutz-02f}.

Other options for future research are more closely related to the
material presented in this paper. For example, is \SHOQKD-concept
satisfiability still decidable if we drop the requirement of key boxes
to be path-free? Moreover, we had to leave the exact time requirements
of our tableau algorithm as an open problem. 
%% I checked the following sentence with the useful page
%% http://www.edufind.com/english/grammar/IF1.cfm 
If this algorithm runs in (non-deterministic) exponential time, it
directly yields Theorem~\ref{theo:shoqkdtableau} rather than via a
bounded model property.

\acks{%
%
  We would like to thank the anonymous reviewers for valuable
  comments.  This paper is an extended version
  of~\cite{Areces-et-al-02b}.}

  \appendix

\section{Proofs of Section~\ref{subsect:redprelim}}
\label{applower}

We prove that $\Dsf_2$-satisfiability can be decided in \PTime.
%
\begin{proposition}
  $\Dsf_2$-satisfiability is in \PTime.
\end{proposition}
%
\begin{proof}
  Let $c$ be a $\Dsf_2$-conjunction. We show that $c$ is
  satisfiable iff none of the following conditions applies:
  %
  \begin{enumerate}

  \item $c$ contains a conjunct $\bot_{\Dsf_2}(x)$;

  \item $c$ contains conjuncts $\mn{bit0}^i_k(x)$ and $\mn{bit1}^i_k(x)$;
    
  \item $c$ contains conjuncts $\mn{bit}n^i_k(x)$ and
    $\mn{bit}m^j_{\ell}(x)$ with $k \neq \ell$;
    
  \item $c$ contains conjuncts $\mn{bit}n^i_k(x)$ and
    $\overline{\mn{bit}n^i_k} (x)$;
    
  \item $c$ contains conjuncts $\mn{bit}n^i_k(x)$,
    $\overline{\mn{bit0}^j_k}(x)$, and
    $\overline{\mn{bit1}^j_{k}}(x)$.
  \end{enumerate}
                                %
  It is easily seen that $c$ is unsatisfiable if one of the conditions
  applies. Assume now that Conditions~1 to~5 do \emph{not} apply to
  $c$ and let $X$ be the set of variables used in $c$. For each $x \in
  X$, set $t(x) = k$ if $\mn{bit}n^i_k(x) \in c$ for some $n,i \in
  \mathbbm{N}$.\footnote{We use ``$P(x)\in c$'' as an abbreviation for
  ``$P(x)$ is a conjunct in $c$''.} If $\mn{bit}n^i_k(x) \notin c$ for
  all $n,i,k \in \mathbbm{N}$, then set $t(x)=r$ for some $r$ not
  appearing as an index $\cdot_r$ to a predicate in~$c$. The mapping
  $t$ is well-defined since $c$ is finite, Condition~3 does not apply,
  and the only predicates  available are $\mn{bit}n^i_k(\cdot)$,
  $\bot_{\Dsf_2}(\cdot)$, and $\top_{\Dsf_2}(\cdot)$. 
                                %  
  We define a solution $\delta$ for $c$ as follows: for each $x \in
  X$, set $\delta(x)$ to the bit vector $v \in \mn{BV}_{t(x)}$ in
  which the $i$'th bit is 1 if $\mn{bit1}^i_{t(x)}(x) \in c$ or
  $\overline{\mn{bit0}^i_{t(x)}}(x) \in c$, and 0 otherwise. It
  remains to prove that $\delta$ is indeed a solution for $c$:
  %
  \begin{itemize}
  
  \item Let $\mn{bit0}^i_k(x) \in c$. Then $t(x)=k$ and thus
    $\delta(x) \in \mn{BV}_k$. Since Condition~2 does not apply, we
    have $\mn{bit1}^i_k(x) \notin c$. Moreover, non-applicability of
    Condition~4 implies $\overline{\mn{bit0}^i_k}(x) \notin c$. By 
    definition of $\delta$, the $i$'th bit of $\delta(x)$ is thus 0.
   
  \item Let $\mn{bit1}^i_k(x) \in c$. Then $t(x)=k$ and $\delta(x) \in
    \mn{BV}_k$. By definition of $\delta$, the $i$'th bit of
    $\delta(x)$ is 1.
    
  \item Let $\overline{\mn{bit0}^i_k}(x) \in c$. If $t(x) \neq k$,
    then $\delta(x) \notin \mn{BV}_k$. Thus $\delta(x) \in
    (\overline{\mn{bit0}^i_k})^{\Dsf_2}$ and we are done. If $t(x)=k$,
    then the $i$'th bit of $\delta(x)$ is 1 by definition of $\delta$
    and thus again $\delta(x) \in
    (\overline{\mn{bit0}^i_k})^{\Dsf_2}$.
  
  \item Let $\overline{\mn{bit1}^i_k}(x) \in c$.  If $t(x) \neq k$,
    then $\delta(x) \notin \mn{BV}_k$ and we are done. If $t(x) = k$,
    then $\mn{bit}n^j_k(x) \in c$ for some $n,j \in \mathbbm{N}$.
    Since Condition~5 does not apply, we thus have
    $\overline{\mn{bit0}^i_k}(x) \notin c$. Moreover,
    non-applicability of Condition~4 yields $\mn{bit1}^i_k(x) \notin
    c$. Thus, by definition of $\delta$, the $i$'th bit of $\delta(x)$
    is 0.

  \end{itemize}
  %
  It is obvious that the listed properties can be checked in
  polynomial time.
\end{proof}


\section{Proofs of Section~\ref{sect:alcokdtableau}}\label{ap1}

We prove termination, soundness, and completeness of the \ALCOKD
tableau algorithm presented in Section~\ref{sect:alcokdtableau},
starting with termination. We start with establishing a few notions
and technical lemmas.

Let $C$ be a concept and \Kmc a key box. We use $|C|$ to denote the
length of $C$, i.e.\ the number of symbols used to write it down, and
$|\Kmc|$ to denote $\sum_{(u_1,\dots,u_k \text{ keyfor } C) \in \Kmc}
|C|$. For a path $u=f_1 \cdots f_k g$, we use $|u|$ to denote $k+1$.
The \emph{role depth} of concepts is defined inductively as follows:
$$
\begin{array}{l}
  \mn{rd}(A) = \mn{rd}(N) = \mn{rd}(g{\uparrow}) = 0\\
  \mn{rd}(\exists u_1,\dots,u_n . P) = \max\{|u_i|  \mid 1\leq i \leq
  n \} -1  \\[1mm]
  \mn{rd}(C \sqcap D) = \mn{rd}(C \sqcup D) = \max\{\mn{rd}(C),\mn{rd}(D)\} \\[1mm]
  \mn{rd}(\exists R . C) =  \mn{rd}(\forall R . C) = \mn{rd}(C) + 1. 
\end{array}
$$

\noindent
The following series of lemmas will eventually allow us to prove termination.

\begin{lemma}
\label{termlem1} There is a constant $k$ such that, if the tableau
algorithm is started on input $C_0, \Kmc$ and $\Tbf=(V_a,V_c,E,\Lmc)$
is a completion tree constructed during the run of the algorithm, then
$\#V_a \leq 2^{|C_0|^k}$ and $\#V_c \leq 2^{|C_0|^k}$.

% Let the tableau algorithm be started on input $C_0, \Kmc$ and let
% $\Tbf=(V_a,V_c,E,\Lmc)$ be a completion tree constructed during the
% run of the algorithm. Then there is a constant $k$ such that $\#V_a
% \leq 2^{|C_0|^k}$ and $\#V_c \leq 2^{|C_0|^k}$.
\end{lemma}


\begin{proof}
  Using induction on the number of rule applications and a case
  distinction according to the applied rule, it is straightforward to
  show that
  %
  \begin{equation*}
    C \in \Lmc(a) \text{ implies } \mn{rd}(C) \leq |C_0| -
  \mn{lev}_\Tbf(a) 
  \tag{$*$}
  \end{equation*}
  
\noindent
  for all constructed completion trees \Tbf.  We omit the details but
  note that, (1) for treating the \Rch rule, one needs to employ the
  fact that \Kmc is Boolean and thus only adds concepts of role depth
  0 to node labels, and (2) for treating the \Rp rule, we use
  that $a \prec b$ implies $\mn{lev}_\Tbf(a) \leq \mn{lev}_\Tbf(b)$.
  
  This implies an upper bound on the depth of constructed completion
  trees: first, only the \Rex and \Rexc rules generate new nodes, and
  an application of either rule to a node $a \in V_a$ implies $\Lmc(a)
  \neq \emptyset$ and thus $\mn{lev}_\Tbf(a) \leq |C_0|$ by ($*$).
  Second, each new (abstract or concrete) node $b$ generated by an
  application of these rules to a node $a \in V_a$ clearly satisfies
  $\mn{lev}_\Tbf(b) \leq \mn{lev}_\Tbf(a) +
  \mn{max}(1,\mn{mpl}(C_0))$, where $\mn{mpl}(C_0)$ denotes the
  maximum length of paths in $C_0$ (note that concepts in \Kmc may not
  contain any paths since it is Boolean). Since $\mn{mpl}(C_0) \leq
  |C_0|$, the above observations imply that the depth of constructed
  completion trees is bounded by $2 \cdot |C_0|$.
  
  Now for the out-degree. If a node $a$ is generated, then this is due
  to the application of a rule \Rex or \Rexc and, initially, $a$ has
  at most one successor. Let us analyze the number of successors
  generated by later applications of the rules \Rex and \Rexc to $a$:
  these rules can be applied at most once for each concept of the form
  $\exists R . C$ or $\exists u_1,\dots,u_n . P$ in $\Lmc(a)$. By
  definition of $\mn{cl}(C_0,\Kmc)$ and since \Kmc is Boolean, the
  number of such concepts per node label is bounded by
  $\#\mn{sub}(C_0) \leq |C_0|$. Moreover, each rule application
  creates at most $|C_0|$ successors. Hence, the out-degree of
  constructed completion trees is bounded by \mbox{$|C_0|^2 + 1$}.
\end{proof}


\begin{lemma}
\label{termlem2}
There is a constant $k$ such that, if the tableau algorithm is
started with $C_0,\Kmc$, then, in every recursion step, the while loop
terminates after at most $2^{|C_0|^k}$ steps. 
\end{lemma}


\begin{proof}
  Fix an argument $S=(\Tbf,\Pmc,\prec,\sim)$ with
  $\Tbf=(V_a,V_c,E,\Lmc)$ passed to the \mn{sat} function, let
  ${\sim}_1, {\sim}_2, \dots$ be the sequence of concrete equivalences
  computed in the while loop, and let ${\approxcm 1}, {\approxcm
    2},\dots$ be the corresponding $\approxc$ relations. Since
  $\mathsf{test}(\zeta_S)$ calls a \Dmc-tester, each of these calls
  indeed terminates.
  
  We show that
  %
  \begin{equation*}
    {\sim}_1 \subsetneq {\sim}_2 \subsetneq \cdots,
    \tag{$*$}
  \end{equation*}
  
\noindent
which implies Lemma~\ref{termlem2}: by Lemma~\ref{termlem1}, there
exists a constant $k$ such that $\#V_c \leq 2^{|C_0|^k}$.  Hence, we
have $\#{\sim}_i \leq 2^{2 \cdot |C_0|^{k}}$ which, together with
($*$), implies that the number of steps performed by the while loop is
also bounded by $2^{2 \cdot |C_0|^{k}}$.
  
  Now for the proof of ($*$). If the while loop reaches the $i$-th
  step, then we had ${\sim}_{i-1} \neq {\approxcm {i-1}}$ after step
  $i-1$. Since ${\sim}_{i-1} \subseteq {\approxcm {i-1}}$ by
  definition, this implies ${\sim}_{i-1} \subsetneq {\approxcm {i-1}}$.
  By definition of $\zeta_S$, it is easy to see that
  ${\approxcm{i-1}} \subseteq {\sim}_i$ for $i \geq 1$. Hence
  ${\sim}_{i-1} \subsetneq {\sim}_i$.
\end{proof}

\begin{lemma}
\label{termlem3}
There is a constant $k$ such that, if the tableau algorithm is started
with $C_0,\Kmc$, then the number of recursive calls is bounded by
$2^{(|C_0|+|\Kmc|)^k}$. 
\end{lemma}


\begin{proof}
  It obviously suffices to establish an appropriate upper bound on the
  number of rule applications. The \Rand, \Ror, \Rex, and \Rexc rules
  can be applied at most once for each concept in a node label. By
  Lemma~\ref{termlem1}, the number of nodes is at most exponential in
  $|C_0|+|\Kmc|$.  Since neither nodes nor concepts in node labels are
  ever deleted, the fact that node labels are subsets of
  $\mn{cl}(C_0,\Kmc)$ thus implies that the number of applications of these
  rules is at most exponential in $|C_0|+|\Kmc|$. The same holds for
  the rules \Rall and \Rp, which can be applied at most once for every
  concept $C \in \mn{cl}(C_0,\Kmc)$ and every pair of (abstract)
  nodes. Finally, the number of \Rch applications is at most
  exponential in $|C_0|+|\Kmc|$ since this rule can be applied at most
  once for every abstract node and every key assertion in \Kmc.
\end{proof}

\noindent
Termination is now an obvious consequence of Lemmas~\ref{termlem2}
and~\ref{termlem3}.

\begin{corollary}[Termination]
  \label{term}
  The tableau algorithm terminates on any input.
\end{corollary}

\noindent
Let us now prove soundness of the algorithm.

\begin{lemma}[Soundness]
\label{sound}
  If the tableau algorithm returns \mn{satisfiable}, then the input
  concept $C_0$ is satisfiable w.r.t.\ the input key box \Kmc.
\end{lemma}

\begin{proof}
  If the tableau algorithm returns \mn{satisfiable}, then there exists
  a complete and clash-free completion system
  $S=(\Tbf,\Pmc,\prec,\sim)$ for $C_0$. Let $\Tbf=(V_a,V_c,E,\Lmc)$.
  By definition of the tableau algorithm, there is a completion system
  \mbox{$S'=(\Tbf,\Pmc,\prec,\sim')$} such that a call to
  $\mn{test}(\zeta_{S'})$ returned $\sim$.  Moreover, we have
  ${\sim}={\approxc}$ in $S$. Thus, there exists a solution $\delta$
  for $\zeta_{S'}$ such that
  %
  \begin{equation*}
    \delta(x) = \delta(y) \text{ iff } x \approxc y.
    \tag{$\dagger$}
  \end{equation*}
  
\noindent
Clearly, $\delta$ is also a solution for $\zeta_S$: since the second
component \Pmc is the same in $S$ and $S'$, $\delta$ is a solution for
the first part $\displaystyle\bigwedge_{P \text{ used in } C}
\bigwedge_{(x_1,\dots,x_n) \in \Pmc(P)} P(x_1,\dots,x_n)$ of
$\zeta_S$. Moreover, for each conjunct ${=}(x,y)$ from the second part
of $\zeta_S$, we have $x \approxc y$ by definition of $\zeta_S$ and
thus $\delta(x)=\delta(y)$ by ($\dagger$).


  We now use $S$ and $\delta$ to construct an interpretation \Imc by
  setting
  $$
  \begin{array}{rcl}
  \Delta_\Imc &=& \{ a \in V_a \mid \text{ there is no $b \in V_a$ such that }
  a \approxa b \text{ and } b \prec a \} \cup \{ w \}
  \\[1mm]
  A^\Imc &=& \{ a \in \Delta_\Imc \mid A \in \Lmc(a) \}
  \\[1mm]
  N^\Imc &=& 
  \left \{
    \begin{array}{ll}
     \{ a \in \Delta_\Imc \mid N \in \Lmc(a) \} & \text{if there is an $a \in \Delta_\Imc$ such that $N \in \Lmc(a)$} \\
     \{ w \} & \text{otherwise}
    \end{array}
  \right .
  \\[5mm]
  R^\Imc &=& \{ (a,b) \in \Delta_\Imc \times \Delta_\Imc \mid 
  \text{ there are $a',b' \in V_a$ such that $a \approxa a'$, $b \approxa b'$,
  and} \\[1mm]
  &&\hspace*{3,5cm} \text{$b'$ is an $R$-successor of $a'$} \}
  \\[1mm]
  g^\Imc &=& \{ (a,\delta(x)) \in \Delta_\Imc \times \Delta_\Dmc \mid 
  \text{ $x$ is a $g/{\approxa}$-neighbor of $a$} \}
  \end{array}
  $$

\noindent
  for all $A \in \NC$, $N \in \NO$, $R \in \NR$, and $g \in \NcF$.
  We first show that \Imc is well-defined:
  %
  \begin{itemize}
    
  \item $N^\Imc$ is a singleton for each $N \in \NO$. Assume that
    there exist $a,b \in \Delta_\Imc$ such that $a \neq b$ and $N \in
    \Lmc(a) \cap \Lmc(b)$. By definition of $\approxa$
    (Definition~\ref{approx}), $N \in \Lmc(a) \cap \Lmc(b)$ implies $a
    \approxa b$. This, together with $a,b \in \Delta_\Imc$, yields $a
    \prec b$ and $b \prec a$, contradicting $\prec$ being a linear
    ordering.
    
  \item $f^\Imc$ is functional for each $f \in \NaF$. Assume that
    there exist $a,b,c \in \Delta_\Imc$ such that $\{(a,b),(a,c)\}
    \subseteq f^\Imc$ and $b \neq c$. Then there exist $a_1,a_2,b',c'
    \in V_a$ such that $a \approxa a_1 \approxa a_2$, $b \approxa b'$,
    $c \approxa c'$, $b'$ is an $f$-successor of $a_1$, and $c'$ is an
    $f$-successor of $a_2$. By definition of $\approxa$, we thus have
    $b' \approxa c'$ implying $b \approxa c$. Since $b,c \in
    \Delta_\Imc$, this yields $b \prec c$ and $c \prec b$, a
    contradiction.
    
  \item $g^\Imc$ is functional for each $g \in \NcF$.  Assume that
    there exist an $a \in \Delta_\Imc$ and $x,y \in \V_c$ such that
    $\{(a,\delta(x)),(a,\delta(y))\} \subseteq f^\Imc$ and $\delta(x)
    \neq \delta(y)$.  Then $x$ and $y$ are both
    $g/{\approxa}$-neighbors of $a$. By definition of $\approxc$, we
    thus have $x \approxc y$ implying $\delta(x)=\delta(y)$ by
    ($\dagger$), a contradiction.

  \end{itemize}
  
  \noindent
  Now we show the following claim. In the proof, we use the notion of
  \emph{$f_1 \cdots f_k$/$\approx_a$-neighbors} (with $f_1,\dots f_k$
  abstract features), which is defined analogously to
  $u$/$\approx_a$-neighbors for paths~$u$.
  \\[2mm]
  {\bf Claim 1}: For all $a \in \Delta_\Imc$ and all paths $u$, we
  have $u^\Imc(a)=\alpha$ iff there is a $u_i/\approx_a$-neighbor $x$
  of $a$ with $\delta(x)=\alpha$.
  \\[2mm]
  Proof: Let $u=f_1 \cdots f_k g$. Using induction on $i$ it is easily
  proved that, for all $i$ and all $b \in \Delta_\Imc$, we have
  $f_i^\Imc(\cdots(f_1^\Imc(a))\cdots)=b$ iff there is a $f_1 \cdots
  f_i$/$\approx_a$-neighbor $b'$ of $a$ with $b \approx_a b'$. Thus we
  have in particular that $f_k^\Imc(\cdots(f_1^\Imc(a))\cdots)=b$ iff
  there is an $f_1 \cdots f_k$/$\approx_a$-neighbor $b'$ of $a$ with $b
  \approx_a b'$. To prove the claim, it hence remains to use the
  definition of~$g^\Imc$ together with ($\dagger$).

  \medskip
\noindent
The following claim is central for showing that \Imc is a model for
$C_0$ and \Kmc.
\\[2mm]
{\bf Claim 2}: For all $a \in \Delta_\Imc$ and $C \in
\mn{cl}(C_0,\Kmc)$, if $C \in \Lmc(a)$, then $a \in C^\Imc$.
\\[2mm]
Since $C_0$ is in the label of the root node, Claim~2 clearly
implies that \Imc is a model for $C_0$. Moreover, we can use it to
prove that \Imc satisfies all key assertions \mbox{$(u_1,\dots,u_n
  \text{ keyfor } C)$} in \Kmc: fix $a,b \in C^\Imc$ such that
$u_i^\Imc(a)=u_i^\Imc(b)$ for $1 \leq i \leq n$. Non-applicability of
\Rch yields $\{ C, \nneg C \} \cap \Lmc(a) \neq \emptyset$. If $\nneg
C \in \Lmc(a)$, then Claim~2 implies $a \in (\nneg C)^\Imc$ in
contradiction to $a \in C^\Imc$. Thus we obtain $C \in \Lmc(a)$.  In
an analogous way, we can argue that $C \in \Lmc(b)$. Since
$u_i^\Imc(a)$ and $u_i^\Imc(b)$ are defined for $1 \leq i \leq n$,
Claim~1 yields that $a$ has a $u_i/{\approxa}$-neighbor $x_i$ with
$\delta(x_i)=u_i^\Imc(a)$ and $b$ a $u_i/{\approxa}$-neighbor $y_i$
with $\delta(y_i)=u_i^\Imc(b)$ for $1 \leq i \leq n$. Thus the fact
that $u_i^\Imc(a)=u_i^\Imc(b)$ yields $\delta(x_i)=\delta(y_i)$ for $1
\leq i \leq n$. By ($\dagger$) we obtain $x_i \approxc y_i$ and thus
$x_i \sim y_i$ for $1 \leq i \leq n$.  By definition of $\approx_a$,
we thus get $a \approxa b$. Since $a,b \in \Delta_\Imc$, we obtain $a
\not\prec b$ and $b \not\prec a$ by definition of $\Delta_\Imc$ and
thus $a = b$.
  
  It remains to prove Claim~2, which we do using structural
  induction:
  %
  \begin{itemize}

  \item $C$ is a concept name or a nominal. Easy by construction of \Imc.
    
  \item $C=\neg D$. Since $C \in \mn{cl}(C_0,\Kmc)$, $C$ is in NNF and
    $D$ is a concept name. Since $S$ is clash-free, $C \in \Lmc(a)$
    implies $D \notin \Lmc(a)$. Thus, $a \notin D^\Imc$ by
    construction of \Imc, which yields $a \in (\neg D)^\Imc$.
    
  \item $C=\exists u_1,\dots,u_n.P$. Since the \Rexc rule is not
    applicable, there exist $x_1,\dots,x_n \in V_c$ such that $x_i$ is
    a $u_i$/$\approx_a$-neighbor of $a$ for $1 \leq i \leq n$ and
    $(x_1,\dots,x_n) \in \Pmc(P)$. Claim~1 yields
    $u_i^\Imc(a)=\delta(x_i)$ for $1 \leq i \leq n$. Since
    $(x_1,\dots,x_n) \in \Pmc(P)$ and $\delta$ is a solution for
    $\zeta_S$, we have $(\delta(x_1),\dots,\delta(x_n)) \in P^\Dmc$
    and thus $a \in C^\Imc$.
    
  \item $C=g{\uparrow}$. Since $S$ is clash-free, there exists no $x
    \in V_c$ such that $x$ is $g/{\approxa}$-neighbor of $a$. Thus by
    Claim~1 there is no $\alpha$ such that $(a,\alpha)
    \in g^\Imc$.
    
  \item $C=D\sqcap E$ or $C=D\sqcup E$. Straightforward using
    completeness and the induction hypothesis.
    
  \item $C=\exists R . D$. Since the \Rex rule is not applicable, $a$
    has an $R/{\approxa}$-neighbor $b$ such that $D \in \Lmc(b)$. Let
    $b'$ be minimal w.r.t.\ $\prec$ such that $b \approxa b'$. By
    definition of \Imc, we have $(a,b') \in R^\Imc$. Non-applicability
    of the \Rp rule yields $D \in \Lmc(b')$. By induction, we get $b'
    \in D^\Imc$ and thus $a \in C^\Imc$.
    
  \item $C=\forall R . D$. Let $(a,b) \in R^\Imc$. By definition of
    \Imc, this implies that there exist $a',b' \in V_a$ such that $a$
    is minimal w.r.t.\ $\prec$ and $a \approxa a'$, $b$ is minimal
    w.r.t.\ $\prec$ and $b \approxa b'$, and $b'$ is an $R$-successor
    of $a'$. Since $b'$ is clearly an $R/{\approxa}$-neighbor of $a$,
    non-applicability of \Rall yields $D \in \Lmc(b')$, which implies
    $D \in \Lmc(b)$ due to the non-applicability of \Rp. By induction,
    we get $b \in D^\Imc$.  Since this holds independently of the
    choice of $b$, we obtain $a \in (\forall R . D)^\Imc$.

  \end{itemize}
\end{proof}


\begin{lemma}[Completeness]
\label{complete}
  If the input concept $C_0$ is satisfiable w.r.t.\ the input key box
  \Kmc, then the tableau algorithm returns \mn{satisfiable}.
\end{lemma}

\begin{proof}
  Let \Imc be a model of $C_0$ and \Kmc. We use \Imc to ``guide''
  (the non-deterministic parts of) the algorithm such that it constructs a
  complete and clash-free completion system. A completion system
  $S=(\Tbf,\Pmc,\prec,\sim)$ with $\Tbf=(V_a,V_c,E,\Lmc)$ is called
  \emph{\Imc-compatible} if there exist mappings $\pi: V_a \rightarrow
  \Delta_\Imc$ and $\tau: V_c \rightarrow \Delta_\Dmc$ such that
  %
  \begin{enumerate}
  \item [\ca] $C \in \Lmc(a) \Rightarrow \pi(a) \in C^\Imc $
  \item [\cb] $b \text{ is an $R$-successor of } a \Rightarrow (\pi(a)
    ,\pi(b)) \in R^\Imc $
  \item [\cc] $x \text{ is a $g$-successor of $a$ } \Rightarrow g^\Imc(\pi(a))=\tau(x) $
  \item [\cd] $(x_1,\dots,x_n) \in \Pmc(P) \Rightarrow (\tau(x_1),\dots,\tau(x_n)) \in P^\Dmc$
  \item [\ce] $x \sim y \Rightarrow \tau(x)=\tau(y)$.
  \end{enumerate}
  
\noindent
  We first establish the following claim:
  %
  \\[2mm]
  {\bf Claim 1:} If a completion system $S$ is \Imc-compatible, then
  (i)~$a \approxa b$ implies $\pi(a) = \pi(b)$ and (ii)~$x \approxc
  y$ implies $\tau(x) = \tau(y)$.
  \\[2mm]
  Proof: We show by induction on $i$ that $a \approxam i b$ implies
  $\pi(a) = \pi(b)$ (see Definition~\ref{approx}), which yields (i).
  %
  \begin{itemize}
    
  \item Start. If $a \approxam 0 b$, then there exists a nominal $N$
    such that $N \in \Lmc(a) \cap \Lmc(b)$. By \ca we obtain $\pi(a)
    \in N^\Imc$ and $\pi(b) \in N^\Imc$, which yields $\pi(a)=\pi(b)$
    by definition of the semantics.
    
  \item Step. For $a \approxam i b$, we distinguish three cases:
    %
    \begin{enumerate}
      
    \item If $a \approxam{i-1} b$, then $\pi(a) = \pi(b)$ by
      induction.
      
    \item There is a $c \in V_a$ and an $f \in \NaF$ such that both
      $a$ and $b$ are $f/{\approxam {i-1}}$-neighbors of $c$. Hence,
      there exist $c_1,c_2 \in V_a$ such that $c \approxam{i-1} c_1
      \approxam{i-1} c_2$, $a$ is an $f$-successor of $c_1$, and $b$
      is an $f$-successor of $c_2$.  By induction, we have
      $\pi(c)=\pi(c_1)=\pi(c_2)$.   Thus \cb yields $\{
      (\pi(c),\pi(a)), (\pi(c),\pi(b))\} \subseteq f^\Imc$, which
      implies $\pi(a)=\pi(b)$ by definition of the semantics.
      
    \item There exist $(u_1,\dots,u_n \text{ keyfor } C) \in \Kmc$,
      $u_i/{\approxam{i-1}}$-neighbors $x_i$ of $a$ and
      $u_i/{\approxam{i-1}}$-neighbors $y_i$ of $b$ for $1 \leq i \leq
      n$ such that $C \in \Lmc(a) \cap \Lmc(b)$ and $x_i\sim y_i$ for
      $1 \leq i \leq n$. \ca yields $a,b \in C^\Imc$.  Using
      induction, \cb, and \cc, it is straightforward to show that
      $u_i^\Imc(\pi(a))=\tau(x_i)$ and $u_i^\Imc(\pi(b))=\tau(y_i)$
      for $1 \leq i \leq n$. By \ce, this implies
      $u_i^\Imc(\pi(a))=u_i^\Imc(\pi(b))$ for $1 \leq i \leq k$.
      Since \Imc is a model of the key box \Kmc, this yields
      $\pi(a)=\pi(b)$ by definition of the semantics.
    \end{enumerate}
  \end{itemize}
  
\noindent
  Now for Part~(ii) of Claim~1. If $x \approxc y$, then either $x \sim
  y$ or there is an $a \in V_a$ and a $g \in \NcF$ such that both $x$
  and $y$ are $g/{\approxa}$-neighbors of $a$. In the former case, \ce
  yields $\tau(x)=\tau(y)$. In the latter case, Part~(i) of the claim
  and \cc yields $\{ (\pi(a),\tau(x)), (\pi(a),\tau(y))\} \subseteq
  g^\Imc$ which implies $\tau(x)=\tau(y)$.  This finishes the proof of
  Claim~1.
  %
  \\[2mm]
  We can now show that the completion rules can be applied such that
  \Imc-compatibility is preserved.
  % 
  \\[2mm]
  {\bf Claim 2:} If a completion system $S$ is \Imc-compatible and a
  rule \Rsf is applicable to $S$, then \Rsf can be applied such that
  an \Imc-compatible completion system $S'$ is obtained.
  \\[2mm]
  Proof: Let $S$ be an \Imc-compatible completion system, let $\pi$
  and $\tau$ be functions satisfying \ca to \ce, and let \Rsf be a
  completion rule applicable to $S$.  We make a case distinction
  according to the type of \Rsf.
  %
  \begin{itemize}
    
  \item [\Rand] The rule is applied to a concept $C_1 \sqcap C_2 \in
    \Lmc(a)$.  By \ca, $C_1 \sqcap C_2 \in \Lmc(a)$ implies $\pi(a)
    \in (C_1 \sqcap C_2)^\Imc$ and hence $\pi(a) \in C_1^\Imc$ and
    $\pi(a) \in C_2^\Imc$.  Since the rule adds $C_1$ and $C_2$ to
    $\Lmc(a)$, it yields a completion system that is \Imc-compatible
    via the same $\pi$ and $\tau$.
    
  \item [\Ror] The rule is applied to $C_1 \sqcup C_2 \in \Lmc(a)$.
    $C_1 \sqcup C_2 \in \Lmc(a)$ implies $\pi(a) \in C_1^\Imc$ or
    $\pi(a) \in C_2^\Imc$. Since the rule adds either $C_1$ or $C_2$
    to $\Lmc(a)$, it can be applied such that it yields a completion
    system that is \Imc-compatible via the same $\pi$ and $\tau$.
    
  \item [\Rex] The rule is applied to a concept $\exists R .  C \in
    \Lmc(a)$, generates a new $R$-successor $b$ of $a$ and sets
    $\Lmc(b) = \{ C \}$.  By \ca, we have $\pi(a) \in (\exists R .
    C)^\Imc$ and, hence, there exists a $d \in \Delta_\Imc$ such that
    $(\pi(a),d) \in R^\Imc$ and $d \in C^\Imc$. Set $\pi' := \pi \cup
    \{ b \mapsto d \}$. It is readily checked that the resulting
    completion system is \Imc-compatible via $\pi'$ and $\tau$.
    
  \item [\Rall] The rule is applied to a concept $\forall R .  C \in
    \Lmc(a)$ and adds $C$ to $\Lmc(b)$ of an existing
    $R/{\approxa}$-neighbor $b$ of $a$. Hence, there exists an $a'$
    such that $a \approxa a'$ and $b$ is an $R$-successor of $a'$.  By
    Part~(i) of Claim~1, we have $\pi(a)=\pi(a')$. Thus, by \ca we
    have $\pi(a') \in (\forall R .  C)^\Imc$ while \cb yields
    $((\pi(a'),\pi(b)) \in R^\Imc$. By definition of the semantics,
    $\pi(b) \in C^\Imc$ and thus the resulting completion system is
    \Imc-compatible via $\pi$ and $\tau$.
    
  \item [\Rexc] The rule is applied to a concept $\exists
    u_1,\dots,u_n .P \in \Lmc(a)$ with $u_i=f^{(i)}_1 \cdots
    f^{(i)}_{k_i} g_i$ for $1 \leq i \leq n$. The rule application
    generates new abstract nodes $b^{(i)}_j$ and $x_j$ for $1 \leq i
    \leq n$ and $1 \leq j \leq k_i$ such that
    %
    \begin{itemize}
    \item $b^{(i)}_1$ is an $f^{(i)}_1$-successor of $a$ for $1 \leq i \leq n$,
    \item $b^{(i)}_j$ is an $f^{(i)}_j$-successor of $b^{(i)}_{j-1}$ for
      $1 \leq i \leq n$ and $2 \le j \leq k_i$,
    \item $x_i$ is $g_i$-successor of $b^{(i)}_{k_i}$ for $1 \leq i
      \leq n$, and
    \item $(x_1,\dots,x_n) \in \Pmc(P)$.
    \end{itemize}
    
\noindent
    By \ca, we have $\pi(a) \in (\exists u_1,\dots,u_n . P)^\Imc$.
    Hence, there exist $d^{(i)}_j \in \Delta_\Imc$ for $1 \leq i \leq
    n$ and $1 \leq j \leq k_i$ and $\alpha_1,\dots,\alpha_n \in
    \Delta_\Dmc$ such that
    %
    \begin{itemize}
    \item $(\pi(a),d^{(i)}_1) \in (f^{(i)}_1)^\Imc$ for $1 \leq i \leq n$,
    \item $(d^{(i)}_{j-1},d^{(i)}_{j}) \in (f^{(i)}_j)^\Imc$ for $1
      \leq i \leq n$ and $2 \le j \leq k_i$, 
    \item $g_i^\Imc(d^{(i)}_{k_i}) = \alpha_i$ for $1 \leq i \leq n$, and
    \item $(\alpha_1,\dots,\alpha_n) \in P^\Dmc$.
    \end{itemize}
    
\noindent
    Set 
    $\pi' := \pi \cup \bigcup_{1 \leq i\leq n \text{ and } 1 \leq j \leq
      k_i} \{ b^{(i)}_j \mapsto d^{(i)}_j \} \text{ and } \tau' :=
    \tau \cup \bigcup_{1 \leq i\leq n} \{ x_i \mapsto \alpha_i \}$.
    
    The resulting completion system is \Imc-compatible via $\pi'$ and
    $\tau'$.
    
  \item[\Rch] The rule is applied to an abstract node $a$ and a key
    assertion $(u_1,\dots,u_n \text{ keyfor } C)$ $\in$ $\Kmc$ and
    non-deterministically adds either $C$ or $\nneg C$. By definition
    of the semantics, $\pi(a) \in C^\Imc$ or $\pi(a) \in (\nneg
    C)^\Imc$. Hence, \Rch can be applied such that the resulting
    completion system is \Imc-compatible via $\pi$ and $\tau$.
    
  \item [\Rp] The rule is applied to a concept $C \in \Lmc(a)$ and
    adds $C$ to the label $\Lmc(b)$ of a node $b$ with $a \approxa b$.
    By \ca, we have $\pi(a) \in C^\Imc$. Since Claim~1 yields
    $\pi(a)=\pi(b)$, it follows that the resulting completion system
    is \Imc-compatible via $\pi$ and $\tau$.
  \end{itemize}
  
\noindent
  Finally, we show that \Imc-compatibility implies clash-freeness.
  %
  \\[2mm]
  {\bf Claim 3:} Every \Imc-compatible completion system is
  clash-free.
  \\[2mm]
  Proof: Let $S=(\Tbf,\Pmc,\prec,\sim)$ be an \Imc-compatible
  completion system. Consider the three kinds of a clash:
  %
  \begin{itemize}
    
  \item Due to \ca, a clash of the form $\{A , \neg A \} \in \Lmc(a)$ clearly 
    contradicts the semantics.
    
  \item Assume that there are $a \in V_a$ and $x \in V_c$ such that
    $g{\uparrow} \in \Lmc(a)$ and $x$ is $g/{\approxa}$-neighbor of
    $a$.  Then there exists $b \in V_a$ such that $a \approxa b$ and
    $x$ is $g$-successor of $b$. By Claim~1, $a \approxa b$ implies
    $\pi(a) = \pi(b)$. Thus, $g{\uparrow} \in \Lmc(a)$ and \ca give
    $\pi(b) \in (g{\uparrow})^\Imc$. We obtain a contradiction since
    \cc yields $(\pi(b),\tau(x)) \in g^\Imc$.
    
  \item Properties \cd and \ce and Part (ii) of Claim 1 imply that
    $\tau$ is a solution for $\zeta_S$. Thus, $S$ is concrete domain
    satisfiable.
  \end{itemize}
  
\noindent
  We can now describe the ``guidance'' of the tableau algorithm by the
  model~\Imc in detail: we ensure that, at all times, the considered
  completion systems are \Imc-compatible. This obviously holds for
  the initial completion system
  $$
  S_{C_0}=(\Tbf_{C_0},\Pmc_\emptyset,\emptyset,\emptyset) \text{ with }
  \Tbf_{C_0}=(\{a_0\},\emptyset,\emptyset, \{ a_0 \mapsto \{ C \} \}).
  $$
                                
\noindent
  We guide the non-deterministic \mn{test} function such that, when
  given a predicate conjunction $\zeta_S$ with set of variables $V_c
  \subseteq \OC$ as input, it returns the relation $\sim$ defined by
  setting $x \sim y$ iff $\tau(x) = \tau(y)$ for all $x,y \in V$. The
  relation $\sim$ is a concrete equivalence since $\tau$ is a solution
  for $\zeta_S$ (see above). With this guidance, \ce is
  obviously satisfied after each call to \mn{test}, and the other
  properties are not affected by such a call.  According to Claim~2,
  we can apply the completion rules such that \Imc-compatibility is
  preserved. By Corollary~\ref{term}, the algorithm always terminates,
  hence also when guided in this way. Since, by Claim~3, we will not
  find a clash, the algorithm returns \mn{satisfiable}.
\end{proof}
                                
\noindent
The tableau algorithm yields decidability and a tight upper complexity
bound for \ALCOKD-concept satisfiability w.r.t.\ key boxes.
                                
\begin{theorem}[Theorem~\ref{theo:alcokdtableau} of Section~\ref{sect:alcokdtableau}]
  Let \Dmc be a key-admissible concrete domain. If extended
  \Dmc-satisfiability is in \NP, then \ALCOKD-concept satisfiability
  w.r.t.\ Boolean key boxes is in \NExpTime.
\end{theorem}
                                
\begin{proof}
  Corollary~\ref{term} and Lemmas~\ref{sound} and~\ref{complete} yield
  decidability of \ALCOKD-concept satisfiability w.r.t.\ Boolean key
  boxes.  For complexity, Lemma~\ref{termlem3} provides an exponential
  bound on the number of recursive calls.  Hence, it remains to show
  that each single recursion step needs at most exponential time. By
  Lemma~\ref{termlem2}, the while loop terminates after at most
  exponentially many steps. In each such step, we compute the
  relations $\approxa$ and $\approxc$, which are used in the
  construction of the predicate conjunction $\zeta_S$ and for checking
  termination of the while loop. Since, by Lemma~\ref{termlem1}, there
  exists an exponential bound on the number of abstract and concrete
  nodes in the completion system $S$, this can obviously be done in
  exponential time.  Moreover, Lemma~\ref{termlem1} implies that the
  size of $\zeta_S$ is at most exponential. This together with the
  fact that extended \Dmc-satisfiability is in \NP implies that the
  call to \mn{test} needs at most exponential time.  All remaining
  tasks (checking for clashes, completeness, and rule applicability)
  can clearly also be performed in exponential time.
\end{proof}

\section{Proofs of Section~\ref{shoqkd}}\label{ap2}

We first provide the proof of
Lemma~\ref{lem:shof-tableau-sat-criterion} which shows that the notion
of tableaux introduced in Section~\ref{shoqkd} is an adequate
abstraction of models.

\begin{lemma}[Lemma~\ref{lem:shof-tableau-sat-criterion} in Section~\ref{shoqkd}]
  Let $D$ be a \SHOQKD-concept in NNF, \Rmc a role box, and \Kmc a
  path-free key box in NNF. Then $D$ is satisfiable w.r.t.\ \R and
  \Kmc iff $D$ has a tableau w.r.t.\ \R and \Kmc.
\end{lemma}

\begin{proof}
%  We concentrate on Properties~\tabl{10} to \tabl{15} since \tabl{1}
%  to \tabl{9} are ``standard'' and can also be found in tableaux for
%  \SHIQ and \SHOQ, see~\cite{Horrocks-et-al-00c,Horrocks-Sattler-01}.
  For the ``only-if'' direction, we construct a tableau $T$ from a
  common model $\I$ of $D$, \R, and \Kmc as follows:
$$
\begin{array}[t]{rcl}
\S_a&:=&\Delta_\I\\[1mm]
\S_c&:=&\{  x \in \Delta_\Dmc \mid g\ifunc(s) = x \text{ for some }s\in \S_a \}\\[1mm]
\Lmc(s)&:=& \{C\in \cl(D,\R,\Kmc)\mid s\in C\ifunc\}\\[1mm]
\Et(s,t)&:=&\{ S\in \NRDRK\mid \tuple s t \in S\ifunc\}\\[1mm]
\Etc(s,g)&:=& g\ifunc(s) \text{ if } g\ifunc(s) \text{ is defined}\\[1mm]
\Pmc(P)&:=& \{ (x_1,\ldots, x_n) \in \S_c^n \mid (x_1,\ldots, x_n) \in
P^\Dmc \}. 
\end{array}
$$ 

\noindent
It can be easily verified that $T$ is a tableau for $D$ w.r.t.\ \R and
\Kmc: the proof that $T$ satisfies \tabl1 -- \tabl9 is identical to
the corresponding cases in~\cite{Horrocks-et-al-00c,Horrocks-Sattler-01}; \tabl{10} holds by
definition of \Lmc; \tabl{11} by definition of \Lmc and the fact that
nominals are interpreted as singleton sets; \tabl{12} by definition of
\Lmc, $e$, and \Pmc together with the semantics of concepts $\exists
g_1,\ldots,g_n.P$; \tabl{13} since the identity function on $\S_c$ is
clearly a solution for the listed predicate conjunction; \tabl{14} by
definition of \Lmc and $e$ together with the semantics of key
constraints; and finally \tabl{15} by definition of \Lmc and $e$
together with the semantics of concepts $g{\uparrow}$.

For the ``if'' direction, let $T=(\S_a,\S_c,\Lmc,\Et,\Etc,\Pmc)$ be a
tableau for $D$ w.r.t.\ \R and \Kmc and let $\delta$ be a solution for
the predicate conjunction in \tabl{13}. We construct a model $\I$ for $D$
as follows:
$$
\begin{array}{rcl}
\Delta_\I&:=& \S_a\\[1ex]
A\ifunc&:=& \{ s\in \Delta_\I \mid A\in \Lmc(s)\} \quad \text{ for
  concept names $A$}\\[1ex]
N\ifunc&:=& \{ s\in \Delta_\I \mid N\in \Lmc(s)\}\quad \text{for
  nominals $N$}\\[1ex]
R\ifunc&:=& \left \{ 
\begin{array}[c]{ll}
\bigcup_{S\smallsss R\atop S\neq R}S\ifunc\cup \{\tuple s t \mid R\in \Et\tuple s t\}&\text{ for $R\in
\NR\setminus \NcF$ with
\emph{not} \Tr(R)}\\
\{\tuple s t \mid R\in \Et\tuple s t\}^+&\text{ for  $R\in
\NR\setminus \NcF$ with
\Tr(R)}
\end{array}
\right .\\[4ex]
 g\ifunc(s)&:=& \left \{ 
 \begin{array}[c]{ll}
 \delta(x) &\text{ if }\Etc(s,g)=x\\
 \text{undefined}&\text{ if  } \Etc(s,g)\text{ is undefined} 
 \end{array}
\right . \text{ for }g\in \NcF.
\end{array}
$$

\noindent
Due to \tabl{11}, the interpretation of nominals is a singleton.
Moreover, the interpretation of roles is well-defined since role boxes
are acyclic. The following claim is central for proving that \Imc is
indeed a model for $D$, \Rmc, and \Kmc:
\\[1mm]
\textbf{Claim:} For each $C\in \cl(D,\R,\Kmc)$, $C\in \Lmc(s)$ implies
$s\in C\ifunc$.
\\[1mm]
Proof: We proceed by induction on the \emph{norm} $||C||$ of $C$, 
which is defined as follows:
%
$$
\begin{array}{rclcl}
  ||A|| &:=& ||\neg A|| &:=& 0 \text{ for $A$ concept name}\\
  ||g{\uparrow}|| &:=& ||\exists u_1,\dots,u_n.P|| &:=& 0 \\
  ||C_1 \sqcap C_2|| &:=& ||C_1 \sqcup C_2|| &:=& 1+ ||C_1|| + ||C_2|| \\
  ||\qnrgeq n R C|| &:=& ||\qnrleq n R C|| &:=& 1+ ||C|| \\
\end{array}
$$
%
For concept names $A$ and nominals $N$, the claim follows by
definition of $A^\Imc$ and $N^\Imc$.  For the negation of concept
names $A$ and nominals $N$ (note that $C$ is in NNF), the claim
follows by definition of $A^\Imc$ and $N^\Imc$ together with \tabl{1}.
Concepts $C$ of the form $C_1 \sqcap C_2$ and $C_1 \sqcup C_2$ can be
treated using $\tabl{2}$ and $\tabl{3}$ together with the induction
hypothesis.  For existential, universal, and number restrictions, the
proof is analogous to the one for \shiq in~\cite{Horrocks-et-al-00c}.
%\marginpar{at latest in a journal paper
%  we should be self-contained here and above.}  
For concepts of the
form $C = \exists g_1,\ldots g_n.P\in \Lmc(s)$, $s \in C^\Imc$ is an
immediate consequence of \tabl{12}, the definition of $g_i^\Imc$, and
the fact that $(x_1,\dots,x_n) \in \Pmc(P)$ implies
$(\delta(x_1),\dots,\delta(x_n)) \in P^\Dmc$ by \tabl{13}. Finally,
for concepts $C = g{\uparrow}$, $s \in C^\Imc$ is an immediate
consequence of the definition of $g^\Imc$ together with \tabl{15}.
This finishes the proof of the claim.
\\[1mm]
By definition of tableaux, there exists an $s_0 \in \Sbf_a$ such that
$C \in \Lmc(s_0)$. By the claim, $s_0 \in C^\Imc$ and thus \Imc is a
model of $C$.

Next, we show that \Imc is a model of \Rmc. By definition of $R^\Imc$,
it is obvious that $\Tr(R) \in \Rmc$ implies that $R^\Imc$ is a
transitive relation. Now let $S \sqsubseteq R \in \Rmc$. If
\mbox{$\Tr(R) \notin \Rmc$}, then we have $S^\Imc \subseteq R^\Imc$ by
definition of $R^\Imc$. Now let $\Tr(R) \in \Rmc$ and $(s,t) \in
S^\Imc$. If $S\in E(s,t)$, then \tabl 4 implies $R\in E(s,t)$, and
thus $(s,t)\in R^\Imc$. Otherwise, there is an $S' \sss S$ with
$\Tr(S') \in \Rmc$ and $(s,t)\in \{ (u,v)\mid S'\in E(u,v)\}^+$.
Now \tabl4 together with $S'\sss R$ implies that $\{ (u,v)\mid S'\in
E(u,v)\} \subseteq \{ (u,v)\mid R\in
E(u,v)\}$, and thus $\Tr(R) \in \Rmc$ implies that $(s,t)\in R^\Imc$. 

It remains to show that \Imc is a model of \Kmc. To this end, let
\mbox{$(g_1,\ldots,g_n \keyfor C) \in \Kmc$} and $s,t\in C^\Imc$ such
that $g_i\ifunc(s)= g_i\ifunc(t)$ for $1\leq i \leq n$. Since the
predicate conjunction in \tabl{13} contains explicit inequalities for
all distinct concrete individuals, this implies that $\Etc(s,g_i) =
\Etc(t,g_i)$ for $1\leq i \leq n$.  \tabl{10} implies $\{C,\nneg C\}
\cap \Lmc(s) \neq \emptyset$ and \mbox{$\{C,\nneg C\} \cap \Lmc(t)
\neq \emptyset$}. If $\nneg C \in \Lmc(s)$, then the claim yields $s
\in (\nneg C)^\Imc$ contradicting $s \in C^\Imc$. Thus we obtain $C
\in \Lmc(s)$ and, in a similar way, $C \in \Lmc(t)$. Finally,
\tabl{14} implies that $s=t$, and thus $\I$ satisfies \Kmc.
\end{proof}


\noindent
We now proceed to prove termination, soundness, and completeness of the
tableau algorithm presented in Section~\ref{shoqkd}, starting
with termination. In the following, we use $|D,\Rmc,\Kmc|$ to denote
$|\cl^+(D,\Rmc,\Kmc)|$. Recall that this number is polynomial in the
size of $D$, \Rmc, \Kmc.

\begin{lemma}[Termination]\label{lemma:termination}
  Let \Dmc be a key-admissible concrete domain. When started with a
  \SHOQKD concept $D$ in NNF, a role box \R, and a path-free key box
  \Kmc in NNF, the tableau algorithm terminates.
\end{lemma}

\begin{proof}
  Assume that there are $D$, \R, and \Kmc such that the tableau
  algorithm does not terminate. Since \Dmc is key-admissible, this
  means that there is an infinite sequence $S_0, S_1,\ldots $ of
  completion systems such that (a) $S_0$ is the initial completion
  system $S_D$ and (b) $S_{i+1}$ is the result of applying a
  completion rule to $S_i$.
  
  This is only possible if the \Rex or the \Rgeq rules are applied
  infinitely often: it is easily seen that the rules \Rand, \Ror,
  \Rleq, \Rexco, \Rall, \Rallplus, \Rch, and \Rsima can only be
  applied finitely often to completion systems whose set of abstract
  nodes $V_a$ does not increase since they either add concepts into
  node labels (whose size is bounded), or they add concrete nodes
  (whose number is bounded linearly by the number of abstract nodes),
  or they remove abstract nodes from the forest.  Hence there is a
  sub-sequence $S_{i_1}, S_{i_2},\ldots$ of $S_0, S_1,\ldots $ such
  that $S_{i_j}$ is the result of applying the \Rex or the \Rgeq rule
  to $S_{i_j - 1}$. Let $s_{i_\ell}$ be the abstract node to which the
  \Rex or the \Rgeq rule was applied in $S_{i_{\ell} - 1}$. Since $s
  \prec t$ implies that $t$ was \emph{not} generated before~$s$, the
  linear ordering $\prec$ is well-founded. Thus, we find an infinite
  sub-sequence $S_{j_1}, S_{j_2},\ldots$ of $S_{i_1}, S_{i_2},\ldots$
  such that either $s_{j_\ell} = s_{j_{\ell +1}}$ for each $\ell \geq
  1$ or $s_{j_\ell} \prec s_{j_{\ell +1}}$ for each $\ell \geq 1$. The
  former, however, is not possible since the \Rex and the \Rgeq rules
  are applied at most once per node and concept in
  $\mn{cl}(D,\R,\Kmc)$: even if a node is removed, the label copying
  performed by the \Rleq rule together with clashes of type \clash 3
  ensures that the \Rgeq rule is not re-applied to the same concept
  and node. Thus only the second option remains: there is a
  subsequence $S_{j_1}, S_{j_2},\ldots$ of $S_{i_1}, S_{i_2},\ldots$
  such that $s_{j_\ell} \prec s_{j_{\ell +1}}$ for each $\ell \geq 1$.
  Let $\Lmc_j$ be the labeling function in $S_j$. Since each abstract
  node is labeled with a subset $\Lmc_j$ of $\cl^+(D,\R,\Kmc)$, there
  are nodes $s_{j_k} \prec s_{j_\ell}$ with $k \lneq \ell$ and
  $\Lmc_{j_k}({s_{j_k}}) = \Lmc_{j_\ell}({s_{j_\ell}})$. Now node
  labels can only increase and, if a node $t$ is removed, its label is
  conjoined to the label of a node $\hat t$ with $\hat t \prec t$.
  Thus there is a node $t$ in the completion system $S_{j_\ell}$ with
  $t\prec s_{j_\ell}$ and
                                %
$\Lmc_{j_\ell}({s_{j_\ell}}) \subseteq \Lmc_{j_\ell}(t)$. By definition,
$s_{j_\ell}$ is thus blocked in $S_{j_\ell}$, contradicting the
assumption that the \Rex or the \Rgeq rule is applied to $s_{j_\ell}$
in $S_{j_\ell}$. 
\end{proof}

%
%
%  start with showing that the ``generating'' rules \Rex and \Rgeq are
% applied at most $2^n$ times. To do this, assume to the contrary that
% the generating rules are applied $m > 2^n$ times.  Let
% $\Fbf_1,\Fbf_2,\dots$ be the (as of now potentially infinite) sequence
% of completion trees constructed by the algorithm, and, for an abstract
% node $s$ in $\Fbf_i$, let $\Lmc_i(s)$ denote the label $\Lmc(s)$ in
% $\Fbf_i$.  Moreover, let $i_0 < \dots < i_m$ be the indexes and
% $s_0,\dots,s_m$ be the abstract nodes such that, for each $j \leq m$,
% the $j$-th application of a generating rule was to $s_j$ in the
% completion forest $\Fbf_{i_j}$. It is not hard to see that we have
% $s_0 \prec \dots \prec s_m$: assume $s_{j+1} \prec s_j$ for some $j<m$.

% We now show that one can select indices $o_0 < \dots < o_{m'}$ from
% the sequence $i_0,\dots,i_m$ such that $m' = 2^n$ and $s_{o_1} \prec
% \dots \prec s_{o_{m'}}$: start with setting $o_0 := i_0$ and, for $j
% >0$, set $o_j$ to the smallest index $i_r$ such that $s_{o_{j-1}}
% \prec s_{i_r}$. It can be proved that, in this way, we will indeed
% find $2^n$ indexes: for $j<2^n$, let $p_j$ denote the number of
% indices $i \in \{i_0,\dots,i_m\}$ such that $o_{j} < i$ and $s_{o_j}
% \not\prec s_i$.  It is straightforward to show by induction on $j$
% that, for all $j < 2^n$, we have
% %
% $$
% \sum_{i=0..j} p_i \leq k \cdot j.
% $$



% such
% indices: due to the restricted out-degree, for each $j \geq 0$ there
% exist no more than $\mn{od}^{j}-1$ nodes $s$ with $\mn{lev}(s)<j$ and
% thus the node $s_{\mn{od}^j}$ satisfies $\mn{lev}(s_{\mn{od}^j}) \geq
% j$.
  
%   Since $n$ denotes the number of distinct subsets of
%   $\cl^+(D,\Rmc,\Kmc)$, there exist indices $\ell$ and $k$ such that
%   $0 \leq \ell < k \leq n$ and $\Lmc_\ell(s_\ell) = \Lmc_k(s_k)$. We
%   can now distinguish two cases:
%   %
%   \begin{enumerate}
    
%   \item $s_\ell$ is a node in $\Lmc_k$ (i.e., it has not been removed
%     by the \Rleq rule). Since concepts are never deleted from node
%     labels, this implies $\Lmc_\ell(s_\ell) \subseteq \Lmc_k(s_\ell)$.
%     Thus, $\Lmc_\ell(s_\ell) = \Lmc_k(s_k)$. implies $\Lmc_k(s_k)
%     \subseteq \Lmc_k(s_\ell)$. 
%   \item ohk
%   \end{enumerate}
% \bigskip;

%
%
\begin{lemma}[Soundness]\label{lemma:sound}
  If the expansion rules can be applied to a \SHOQKD concept $D$ in
  NNF, a role box $\R$, and a path-free key box \Kmc such that they
  yield a complete and clash-free completion forest, then $D$ has a
  tableau w.r.t.\ $\R$ and \Kmc.
\end{lemma}

\begin{proof}
  Let $S= ((V_a,V_c,E,\Lmc), \Pmc,\sim_c,\prec)$ be a complete and
  clash-free completion system. We can find a solution $\delta$ for
  $\zeta_S$ such that $\delta(x)= \delta(y)$ iff $x \simc y$: only
  the $\Rexc$ rule updates the predicate conjunction $\zeta_S$, and
  after each rule application the $\sim_c$ relation is updated using
  the concrete equivalence that a \Dmc-tester returns for $\zeta_S$
  (note that $\zeta_S$ is satisfiable due to clash-freeness).
  According to Definition~\ref{keyadm}, we can thus find a solution
  $\delta$ as required. From $S$ and $\delta$,
                                %
  we define a finite tableau $T=(\S_a, \S_c, \hat E, \hat\Lmc, \hat
  \Pmc)$ as follows:
                                %
\begin{eqnarray*}
\S_a &:=&\{s\in V_a\mid s\text{ occurs in $S$ and is not
blocked}\} \\
\S_c &:=& \{ \delta(x) \mid (s,x)\in E(g)\text{ for some $s\in 
\S_a$  and some } g\}\\
                                %
\hat \Lmc(s)&:=& \Lmc(s)\cap \cl(D,\R,\Kmc)\text{ (the intersection is due to the auxiliary concepts
  $A_i^{nRC}$)}, \\
\hat \Et(s,t) &:=& 
\{R \mid t \text{ is an $R$-successor of $s$ or $t$ blocks an
$R$-successor $t'$ of $s$}\}\\
                                %
\Etc(s,g) &:= &\left \{ 
  \begin{array}[c]{ll}
    \delta(x) &\text{if $x$ is a $g$-successor of $s$ }\\
    \text{undefined} &\text{if $x$ has no $g$-successor}
  \end{array}
\right .\\
\hat \Pmc &:= &\text{the restriction of \Pmc to $ \S_c$}.
\end{eqnarray*}

\noindent
Note that the function $e$ is well-defined due to the definition of
\emph{adding $g$-successors}.  It remains to show that $T$ satisfies
\tabl1--\tabl {14}, which is basically a consequence of $S$ being
clash-free and complete.
                                %
\begin{itemize}
\item \tabl 1 is satisfied since $S$ does not contain a clash \clash
  1. 
  
\item \tabl 2 is satisfied since the \Rand rule cannot be applied, and
  thus $C_1\sqcap C_2\in \hat\Lmc(s)$ implies $C_1,C_2\in \hat
  \Lmc(s)$.

\item \tabl 3 is satisfied since the \Ror rule cannot be applied, and
  thus $C_1\sqcup C_2\in \hat\Lmc(s)$ implies $\{C_1,C_2\} \cap \hat
  \Lmc(s)\neq \emptyset$.

\item For \tabl 4, consider $s,t\in\S_a$ with $R\in \hat E(s,t)$ and
  $R\sss R'$. Then $R\in \hat E(s,t)$ implies that $t$ is or blocks an
  $R$-successor of $s$. By definition of ``successor'', $t$ is or
  blocks an $R'$-successor of $s$, and thus $R'\in \hat E(s,t)$.

\item For \tabl 5, let $\all RC\in \hat \Lmc(s)$ and $R\in \hat
  \Et(s,t)$. If $t$ is an $R$-successor of $s$, then $s$ not being
  blocked implies $C\in \Lmc(t)$ since the \Rall rule cannot be
  applied. If $t$ blocks an $R$-successor $t'$ of $s$, then $s$ not
  being blocked and the fact that the \Rall rule cannot be applied
  yields $C\in \Lmc(t')$, and the blocking condition implies $C\in
  \Lmc(t)$.

  In both cases, we  thus have $C\in \hat \Lmc(t)$. 

\item \tabl 6 and \tabl 7 are satisfied for the same reasons as \tabl
  5 with \Rall replaced with \Rex and  \Rallplus.
  
\item For \tabl 8, consider $s$ with $\atleastq nRC\in \hat \Lmc(s)$.
  Hence $\atleastq nRC\in \Lmc(s)$ and completeness of $S$ implies the
  existence of $R$-successors $t_1,\ldots,t_n$ of $s$ with $C\in
  \Lmc(t_i)$ and $t_i \ndoteq t_j$ for $i\neq j$. The latter implies,
  for each $i \neq j$, the existence of integers $k,\ell$ such that $k
  \neq \ell$, $A^{n R C}_{k}\in \Lmc(t_i)$, and $A^{n R C }_{\ell}\in
  \Lmc(t_j)$. For \tabl 8 to be satisfied, it remains to verify that
                                
  \begin{itemize}
  \item no $t_i$ can block a $t_j$: if this was the case, the blocking
    condition would imply that $\{A^{n R C }_{k}, A^{n R C
    }_{\ell}\}\subseteq \Lmc(t_i)$.
    
\item no $t$ can block both $t_i$ and $t_j$ with $i\neq j$: similarly,
  this would imply that $\{A^{n R C }_{k}, A^{n R
    C}_{\ell}\}\subseteq \Lmc(t)$.
  \end{itemize}

\noindent
  In each case, we would have a clash \clash 3, in contradiction to $S$
  being clash-free.
  
\item For \tabl 9, consider $s$ with $\atmostq nRC\in \hat \Lmc(s)$.
  Hence $\atmostq nRC\in \Lmc(s)$ and, since the \Rleq rule cannot be
  applied, there are at most $n$ $R$-successors $t_i$ of $s$. Since
  each $t_i$ is either not blocked or blocked by exactly one other
  node (due to $\prec$ being a linear ordering), there are at most $n$
  $u_i\in \S_a$ with $R\in \hat E(s,u_i)$ and $C\in \hat\Lmc(u_i)$.

  
\item For \tabl{10}, let $\atmostq nRC\in\hat\Lmc(s)$ and $R\in \hat
  E(s,t)$. Hence $\atmostq nRC\in \Lmc(s)$ and $t$ either is an
  $R$-successor of $s$ or blocks an $R$-successor of $s$. In the first
  case, non-applicability of the \Rch rule implies that $\{C,\nneg C\}
  \cap \Lmc(t)\neq \emptyset$. In the second case, $\{C,\nneg C\} \cap
  \Lmc(t')\neq \emptyset$ for $t'$ the $R$-successor of $s$ blocked by
  $t$, and thus the blocking condition yields $\{C,\nneg C\} \cap
  \Lmc(t)\neq \emptyset$. In both cases, this implies $\{C,\nneg C\}
  \cap \hat \Lmc(t)\neq \emptyset$.

  Next, consider $(g_1,\ldots, g_n \keyfor C)\in\Kmc$ and $s$
  such that $e(s,g_i)$ is defined for each $i$. Hence $s$ has a
  $g_i$-successor for each $i$, and thus $s$ not being blocked and the
  non-applicability of the \Rch rule imply that $\{C,\nneg C\} \cap \hat
  \Lmc(t)\neq \emptyset$. 
  
\item For \tabl{11}, consider $N\in \hat \Lmc(s)\cap \hat \Lmc(t)$. By
  definition, $N\in \Lmc(s)\cap \Lmc(t)$ and thus $s\approxa t$.
  Moreover, totality of $\prec$ implies that we can assume without
  loss of generality that $s\prec t$ or $s= t$. Thus non-applicability
  of the \Rsima rule implies that $\Lmc(t) \subseteq \Lmc(s)$, and
  thus $t$ not being blocked implies $s = t$.

\item \tabl{12} is satisfied since the rule \Rexco cannot be applied.
  
\item For \tabl{13}, clash-freeness implies the satisfiability of
                                %
%  \begin{equation}
$$
    \bigwedge_{P\text{ used in }D,\Kmc}\bigwedge_{(x_1,\ldots,x_n)\in
    \Pmc(P)}P(x_1,\ldots,x_n).
$$
%  \end{equation}
       
\noindent
  By choice of $\delta$, $\delta(x)= \delta(y)$ iff $x\simc y$, and
  thus \tabl{13} is satisfied. 
  
\item For \tabl{14}, let $(g_1,\ldots,g_n\keyfor C)\in \Kmc$, $C\in
  \hat\Lmc(s)\cap\hat\Lmc(t)$, and $e(s,g_i)=e(t,g_i)$, for all $1\leq
  i \leq n$. Thus $C\in \Lmc(s)\cap \Lmc(t)$ and, by choice of $e$ and
  $\delta$, we have $x_i\simc y_i$ for $g_i\in E(s,x_i)\cap E(t,y_i)
  $.  Hence $s\approxa t$. Without loss of generality, we assume that
  $s\prec t$ or $s= t$. Thus non-applicability of the \Rsima rule
  implies that $\Lmc(t) \subseteq \Lmc(s)$, and thus $t$ not being
  blocked implies $s = t$.
  
\item \tabl{15} is satisfied by definition of $T$ and since $S$ does not
  contain a clash \clash 4.
\end{itemize}
\end{proof}
 

\begin{lemma}[Completeness]\label{lemma:complete}
  If a \SHOQKD-concept $D$ in NNF has a tableau w.r.t.\ a role box \R
  and a path-free key box \Kmc, then the expansion rules can be
  applied to $D$, \R, and \Kmc such that they yield a complete and
  clash-free completion forest.
\end{lemma}

\begin{proof}
  Given a tableau $T = (\S_a, \S_c,\hat \Lmc,\hat E, e,\hat \Pmc)$ for
  $D$ w.r.t.\ \R and \Kmc, we can ``guide'' the non-deterministic rules
  \Ror, \Rch, and \Rsima in such a way that each rule application
  preserves clash-freeness. This together with termination from
  Lemma~\ref{lemma:termination} finishes the proof.
  
  Along with rule application, we perform a stepwise construction of a
  total mapping $\pi$ that takes abstract nodes of the completion forest
  to elements of $\S_a$ and concrete nodes of the completion forest to
  elements of $\S_c$.
                       %
\begin{itemize}
\item $\Lmc(s)\cap \cl(D,\R,\Kmc)\subseteq \hat \Lmc(\pi(s))$ for each
  $s\in V_a$,
\item if $t$ is an $R$-successor of $s$, then $R\in \hat
  \Et\tuple{\pi(s)}{\pi(t)}$,
\item if $x$ is a $g$-successor of $s$, then $
  \Etc(\pi(s),g)=\pi(x)$, 
\item $x\simc y$ iff $\pi(x)=\pi(y)$, and
\item if $s\ndoteq t$, then $\pi(s)\neq \pi(t)$.
\end{itemize}

\noindent
A mapping satisfying these four conditions is called \emph{correct}
in the following. Note that a completion system for which there exists
a correct mapping does not contain a clash:
                                %
due to \tabl 1 and the first property, we do not encounter a clash
\clash 1. A clash \clash 3 cannot occur due to the last property.  The
first and the third property together with \tabl{15} ensure that a
clash \clash 4 does not occur. Finally, a clash \clash 2 cannot occur
for the following reason: by construction of $\Pmc$ and since edges
labelled with abstract features are never removed, for each tuple
$(x_1,\dots,x_n) \in \Pmc(P)$, we find an abstract node $s$ and paths
$u_1,\dots,u_n$ such that $\exists u_1,\dots,u_n . P \in \Lmc(s)$ and
$x_i$ is a $u_i$-successor of $s$ for $1 \leq i \leq n$. Thus, the
first, second, and third property together with \tabl{12} and
\tabl{13} ensure that the conjunction
%
%\begin{equation}
$$
\bigwedge_{\scriptstyle P\text{ used in}D,\Kmc \atop \scriptstyle
  (x_1,\ldots,x_n)\in \Pmc(P)} P(\pi(x_1),\ldots,\pi(x_n))
$$
%\tag{$*$}
%\end{equation}
%
has a solution $\delta$ with $\delta(\pi(x)) \neq \delta(\pi(x))$ iff
$\pi(x) \neq \pi(y)$. By the fourth property, setting $\delta'(x) :=
\delta(\pi(x))$ for all $x \in V_c$ thus yields a solution $\delta'$
for $\zeta_S$.

The total mapping $\pi$ is inductively defined as follows: let
$\delta$ be a solution for the equation in \tabl{13}.
                                %
Choose a node $\hat s_0$ with $D\in \hat\Lmc(\hat s_0)$, and set
$\pi(s_0):= \hat s_0$ for $s_0$ the (only) node of the initial
completion forest.  Obviously, $\pi$ is correct. We will now show that
each completion rule can be applied in such a way that $\pi$ either is
still correct or that $\pi$ can be extended to a correct mapping.

\begin{itemize}
\item An application of the rule \Rand preserves correctness of $\pi$
  due to \tabl2.
\item Due to \tabl 3, the rule \Ror can be applied such that
  correctness is preserved.
\item If the rule \Rex adds a new node $t$ for $\some RC\in \Lmc(s)$,
  then correctness implies $\some RC\in \hat\Lmc(\pi(s))$, and thus
  \tabl 6 implies the existence of some $\hat t\in  \S_a$ with
  $R\in \Et(\pi(s), \hat t)$ and $C\in \hat \Lmc(\hat t)$. Thus
  extending $\pi$ with $\pi(t):= \hat t$ obviously yields a 
  correct mapping.
  
\item If the rule \Rgeq adds $n$ nodes $t_i$ for $\atleastq nRC\in
  \Lmc(s)$, then correctness implies $\atleastq nRC\in
  \hat\Lmc(\pi(s))$, and thus \tabl 8 implies the existence of $\hat
  t_1,\ldots, \hat t_n\in \hat \S_a$ with $\hat t_i\neq \hat t_j$ for
  $i\neq j$, $R\in \Et(\pi(s), \hat t_i)$, and $C\in \hat \Lmc(\hat
  t_i)$. Thus extending $\pi$ with $\pi(t_i):= \hat t_i$ obviously
  yields a correct mapping.
  
\item Assume that the \Rleq rule is applicable to a node $s$ with
  $\atmostq nRC\in \Lmc(s)$ and more than $n$ $R$-successors $t_i$
  with $C\in \Lmc(t_i)$. Then correctness implies that $\atmostq
  nRC\in \hat\Lmc(\pi(s))$, $R\in \hat E(\pi(s), \pi(t_i))$, and $C\in
  \hat \Lmc(t_i)$. Thus, by \tabl 9, there are $i\neq j$ with
  $\pi(t_i) = \pi(t_j)$. Again, correctness implies that \emph{not}
  $t_i\ndoteq t_j$ and, without loss of generality, we can assume that
  $t_i \prec t_j$. Hence applying the rule and thereby merging
  $\Lmc(t_j)$ into $\Lmc(t_i)$ preserves correctness.

  
\item For the rule \Rexco, $\pi$ can be extended in a similar way as
  for $\Rex$: if a new $g_i$-successor $x_i$ of $s$ is added, then
  extending $\pi$ with $\pi(x_i):= \Etc(\pi(s), g_i)$ yields a correct
  $\pi$. Moreover, \tabl{13} ensures that $\simc$ can be updated in
  such a way that the fourth condition is preserved.

\item For the \Rall rule, $\pi$ does not need to be extended, and
  \tabl 5, \tabl 4, and the definition of $R$-successors imply that
  correctness is preserved. 
\item The \Rallplus rule is similar, with the only difference that
  \tabl 7 takes the place of \tabl 5. 
\item Due to \tabl{10}, the rule \Rch can be applied without violating
  correctness.
\item For \Rsima, we consider two reasons for \Rsima to be applicable:
                                %
  \begin{itemize}
  \item $N\in \Lmc(s)\cap \Lmc(t)$. Then correctness of $\pi$ and
    \tabl{11} imply that $\pi(s)=\pi(t)$. 
  \item $(g_1,\ldots,g_n\keyfor C) \in \Kmc$, $C\in \Lmc(s)\cap
    \Lmc(t)$, and $g_i\in E(s,x_i)\cap E(t,y_i)$ and $x_i\simc y_i$
    for $1\leq i \leq n$. 
                                %
    Then correctness implies that $\hat \Etc(\pi(s),g_i)=
    \Etc(\pi(t),g_i)$, and thus \tabl{14} together with the first
    property of correctness imply that $\pi(s)=\pi(t)$.
  \end{itemize}

\noindent
  In both cases, applying \Rsima to $s$ and $t$ preserves
  correctness.
\end{itemize}
\end{proof}

\noindent
As an immediate consequence of
Lemmas~\ref{lem:shof-tableau-sat-criterion}, \ref{lemma:termination},
\ref{lemma:sound}, and \ref{lemma:complete}, the tableau algorithm
always terminates and answers ``$D$ is satisfiable w.r.t.\ \R and
\Kmc'' if and only if the input concept $D$ is satisfiable w.r.t.\ the
input role box \R and the input key box \Kmc.  Since concept
satisfiability w.r.t.\ TBoxes can be reduced to concept satisfiability
without TBoxes, we obtain the following result:
%
\begin{proposition}
  Let \Dmc be a key-admissible concrete domain. The tableau algorithm
  decides satisfiability of \SHOQKD concepts w.r.t.\ TBoxes, role
  boxes, and path-free key boxes.
\end{proposition}

\noindent
It is not hard to verify that the proof of Lemma~\ref{lemma:complete}
together with Lemmas~\ref{lem:shof-tableau-sat-criterion}
and~\ref{lemma:termination} yield a \emph{bounded model property} for
\SHOQKD, where the bound is exponential.
%
\begin{corollary}
  If a \SHOQKD-concept $D$ is satisfiable w.r.t.\ a role box \Rmc and
  a path-free key box \Kmc, then $D$ is satisfiable w.r.t.\ \Rmc and
  \Kmc in a model of size at most $|\Delta_\Imc| \leq 2^m$ for $m=\#
  \cl^+(D, \R, \Kmc)$.
\end{corollary}
%
\begin{proof}
  If a \SHOQKD-concept $D$ is satisfiable w.r.t.\ a role box \Rmc and
  a path-free key box \Kmc, Lemma~\ref{lemma:complete} implies that
  the tableau algorithm constructs a complete and clash-free
  completion forest for $D$, \Rmc, and \Kmc.  By the definition of
  blocking, the number of abstract nodes in a completion forest that
  are not blocked is bounded by $2^m$: if $s\neq t\in V_a$ are
  abstract nodes in a completion forest and $\Lmc(s)= \Lmc(t)$, then
  either $s$ blocks $t$, $t$ blocks $s$, or they are both blocked by
  another node $u$.
                                %
Moreover, it is easily seen that the number of concrete successors per
abstract node is bounded by the number of concrete features in $C$,
\Rmc, and \Kmc.  Now, in the proof of Lemma~\ref{lemma:complete}, the
abstract nodes in the tableau constructed from a complete and clash-free
completion forest coincide with the nodes that are not blocked in the
completion forest. Finally, in the proof of
Lemma~\ref{lem:shof-tableau-sat-criterion} the interpretation domain
of a model constructed from a tableau coincides with the abstract
nodes in the tableau. Summing up, a \SHOQKD-concept that is
satisfiable w.r.t.\ \Rmc and \Kmc has a model of size $|\Delta_\Imc|
\leq 2^m$.
\end{proof}

\bibliography{clu}
\bibliographystyle{theapa}


\end{document}

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