1: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

2: \documentclass[a4paper,twoside,12pt]{article}

3: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

4: 

5: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

6: %           Author's local commands

7: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

8: 

9: \usepackage{xspace}

10: \usepackage{amsmath}

11: \usepackage{amscd}

12: %\usepackage{dl-macros}

13: \usepackage{amssymb}

14: \usepackage{epic}

15: \usepackage{eepic}

16: \usepackage{pifont}

17: \usepackage{rotating}

18: %\usepackage{overpic}

19: \usepackage{color}

20: 

21: 

22: 

23: \topmargin = -0.5in

24: \oddsidemargin = 0.1in

25: \evensidemargin = 0.1in

26: \textwidth = 6.25in

27: \textheight = 9.5in

28: 

29: \renewcommand{\thefootnote}{}

30: 

31: \title{On Decidability of Expressive Description Logics\\

32: with Composition of Roles in Number Restrictions

33: }

34: \author{\bf Fabio Grandi\\

35: IEIIT.BO-CNR and DEIS,\\

36: Alma Mater Studiorum -- Universit\`a di Bologna,\\

37: Viale Risorgimento 2, I-40136 Bologna, Italy\\

38: Email: {\tt fgrandi@deis.unibo.it}}

39: \date{}

40: 

41: 

42: \newcommand{\QED}{\hfill$\Box$}

43: %\newcommand{\N}{\mathbf{ I\!N}}

44: \newcommand{\N}{\mathbb{N}}

45: \newcommand{\Z}{\mathbb{Z}}

46: 

47: \newcommand{\NI}{\textsf{NI}}

48: \newcommand{\NC}{\textsf{NC}}

49: \newcommand{\NR}{\textsf{NR}}

50: 

51: %\newcommand{\choos}{\copyright}

52: \newcommand{\choos}{\Pisymbol{psy}{227}}

53: 

54: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

55: %           DL macros (from: dl-macros.sty)

56: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

57: 

58: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

59: %%% ACRONYMS

60: 

61: \newcommand{\scname}[1]{\textsc{#1}}    % a (small) capitalized name

62: \newcommand{\calig}[1]{%                % calligraphic text

63:         \ensuremath{\mathcal{#1}}}

64: 

65: \newcommand{\set}[1]{\{ #1 \}}          % set

66: \newcommand{\card}[1]{|{#1}|}           % cardinality

67: 

68: %

69: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

70: %%% LANGUAGES and LOGICS

71: 

72: \newcommand{\NRp}{\ensuremath{\text{\sf NR}^+}}

73: \newcommand{\Cdue}{\ALlang{C}{^2}}

74: 

75: %%% AL-languages

76: \newcommand{\ALlang}[2]{\ensuremath{\mathcal{#1}#2}\xspace}

77: 

78: \newcommand{\ALC}{\ALlang{ALC}{}}

79: \newcommand{\ALCN}{\ALlang{ALCN}{}}

80: %\newcommand{\ALCF}{\ALlang{ALCF}{}}

81: \newcommand{\ALCQ}{\ALlang{ALCQ}{}}

82: 

83: 

84: %%% AL-languages with additional features

85: \newcommand{\ALCNoI}{\ALlang{ALCN}{(\comp)\negmedspace}\ALlang{I}{}}

86: \newcommand{\ALCNX}[1]{\ALlang{ALCN}{(#1)}}

87: \newcommand{\ALCNR}{\ALlang{ALCNR}{}}

88: \newcommand{\ALCNN}{\ALlang{ALC\bar N}{}}

89: \newcommand{\ALCNNX}[1]{\ALlang{ALC\bar N}{(#1)}}

90: \newcommand{\ALCQX}[1]{\ALlang{ALCQ}{(#1)}}

91: \newcommand{\ALCQOX}[1]{\ALlang{ALCOQ}{(#1)}}

92: \newcommand{\ALCpN}{\ALlang{ALC}$_+$\ALlang{N}{}}

93: \newcommand{\ALCpNX}[1]{\ALlang{ALC}$_+$\ALlang{N}{(#1)}}

94: \newcommand{\ALCpQX}[1]{\ALlang{ALC}$_+$\ALlang{Q}{(#1)}}

95: \newcommand{\ALCregN}{\ALlang{ALC}{_{\text{reg}}\ALlang{N}}}

96: \newcommand{\ALCregQ}{\ALlang{ALC}{_{\text{reg}}\ALlang{Q}}}

97: \newcommand{\ALCregNX}[1]{\ALlang{ALC}{_{\text{reg}}\ALlang{N}{(#1)}}}

98: \newcommand{\ALCregQX}[1]{\ALlang{ALC}{_{\text{reg}}\ALlang{Q}{(#1)}}}

99: \newcommand{\ALCXY}[2]{\ALlang{ALC#1}{#2}}      % the rest

100: %%                                 % first arg are constructors (calligraphic)

101: %%                                 % second arg are additional stuff

102: 

103: 

104: %%% C and its variants

105: \newcommand{\CIQ}{\ALlang{CIQ}{}}

106: 

107: 

108: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

109: %%% COMPLEXITY CLASSES

110: 

111: \newcommand{\PSPACE}{\textsc{PSpace}\xspace}

112: \newcommand{\NPSPACE}{\textsc{NPSpace}\xspace}

113: \newcommand{\EXPTIME}{\textsc{ExpTime}\xspace}

114: \newcommand{\NEXPTIME}{\textsc{NExpTime}\xspace}

115: \newcommand{\DNEXPTIME}{\textsc{2-NExpTime}\xspace}

116: 

117: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

118: %%% SEMANTICS

119: 

120: %% The following accept an optional parameter (to be put between [ and ])

121: %% to allow the use of an interpretation name different from \I.

122: %% If the optional parameter is missing the default interpretation is \I:

123: %%  e.g.,     $\Int{C}$     becomes $C^{\I}$

124: %%        but $\Int[\J]{C}$ becomes $C^{\J}$.

125: 

126: \newcommand{\I}{\mathcal{I}}           % interpretation (default to use)

127: \newcommand{\dom}[1][\I]{\Delta^{#1}}  % delta^I (domain of interpretation \I)

128: \newcommand{\Int}[2][\I]{#2^{#1}}      % #2^I    (interpretation function)

129: \newcommand{\inter}[1][\I]{(\dom[#1],\Int[#1]{\cdot})}   % (dom^I,.^I)

130: 

131: \newcommand{\tuple}[1]{\langle #1 \rangle}

132: 

133: \newcommand{\true}{\textbf{true}\xspace}

134: \newcommand{\false}{\textbf{false}\xspace}

135: \newcommand{\any}{\textbf{any}\xspace}

136: 

137: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

138: %%% DL CONSTRUCTS

139: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

140: 

141: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

142: %%% Abstract syntax for concepts, roles, knowledge bases

143: 

144: %%% Knowledge base

145: \newcommand{\K}{\mathcal{K}}                         % knowledge base (default)

146: 

147: %%% Knowledge base assertions

148: \newcommand{\Equiv}{\doteq}                          % equivalence assertion

149: \newcommand{\Implies}{\sqsubseteq}                   % inclusion assertion

150: 

151: %%% Subsumption

152: \newcommand{\IsSubs}{\sqsubseteq}          % is subsumed by

153: \newcommand{\Subs}{\sqsupseteq}                      % subsumes

154: \newcommand{\notIssub}{\mathrel{\not\sqsubseteq}}    % is not subsumed by

155: \newcommand{\notSubs}{\mathrel{\not\sqsupseteq}}     % not subsumes

156: \newcommand{\notEquiv}{\mathrel{\not\equiv}}         % is not equivalent

157: 

158: 

159: %%% Concept, role, etc. names

160: %%% we use mathit to ensure proper spacing of two or more capital letters in

161: %%% math mode

162: 

163: \newcommand{\CN}{\mathit{CN}}        % generic concept name

164: \newcommand{\RN}{\mathit{RN}}        % generic role name

165: \newcommand{\AN}{\mathit{AN}}        % generic attribute name

166: \newcommand{\IN}{\mathit{IN}}        % generic individual (name)

167: \newcommand{\AIN}{\mathit{AIN}}      % generic anonymous individual (name)

168: \newcommand{\DIN}{\mathit{DIN}}      % generic distinct individual (name)

169: \newcommand{\GN}{\mathit{GN}}        % generic group name

170: 

171: \newcommand{\Bot}{\ensuremath{\bot}}

172: \newcommand{\Top}{\ensuremath{\top}}

173: 

174: %%% Concept constructors

175: 

176: \renewcommand{\And}{\ensuremath{\sqcap}}

177: \newcommand{\Or}{\ensuremath{\sqcup}}

178: \newcommand{\Not}{\ensuremath{\neg}}

179: 

180: \newcommand{\usome}[1]{\exists #1}

181: \newcommand{\none}[1]{\uparrow #1}

182: \newcommand{\some}[2]{\ensuremath{\exists} #1 . #2}

183: \newcommand{\all}[2]{\ensuremath{\forall} #1 . #2}

184: \newcommand{\atleast}[2]{\ensuremath{\exists^{\geq #1}} #2}

185: \newcommand{\atmost}[2]{\ensuremath{\exists^{\leq #1}} #2}

186: \newcommand{\exactly}[2]{\ensuremath{\exists^{= #1}} #2}

187: \newcommand{\atleastq}[3]{\ensuremath{\exists^{\geq #1}} #2 . #3}

188: \newcommand{\atmostq}[3]{\ensuremath{\exists^{\leq #1}} #2 . #3}

189: \newcommand{\exactlyq}[3]{\ensuremath{\exists^{= #1}} #2 . #3}

190: \newcommand{\notsame}[2]{#1 \neq #2}

191: \newcommand{\subs}[2]{#1 \subseteq #2}

192: \newcommand{\fills}[2]{#1 : #2}

193: 

194: %%% Role constructors

195: 

196: \newcommand{\inv}[1]{#1^{-}}              % inverse role operator

197: \newcommand{\comp}{\circ}                 % compose role operator

198: \newcommand{\trans}[1]{#1^{+}}            % transitive role operator

199: \newcommand{\trr}[1]{#1^{*}}              % transitive-reflexive role operator

200: \newcommand{\restrict}[2]{#1\!\mid_{#2}}  % role restriction

201: \newcommand{\product}[2]{#1 \times #2}    % product

202: \newcommand{\id}[1]{\mathit{id}(#1)}      % identity relation

203: 

204: 

205: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

206: %%% Concrete syntax for concepts, roles, knowledge bases

207: 

208: \newcommand{\syntax}[1]{\mbox{{\tt #1}}}

209: 

210: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

211: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

212: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

213: 

214: \renewcommand{\ding}[1]{\text{\Pisymbol{pzd}{#1}}}

215: 

216: \newtheorem{theorem}{Theorem}

217: \newtheorem{corollary}{Corollary}

218: \newtheorem{Definition}{Definition}

219: \newtheorem{proposition}{Proposition}

220: \newtheorem{lemma}{Lemma}

221: \newtheorem{new_example}{Example}

222: 

223: %\DeclareMathSymbol{\bigsqcap}{\mathop}{symbols}{'165}

224: 

225: \newenvironment{example}

226:         {\begin{new_example}\rm}

227:         {\hfill$\square$\end{new_example}}

228: 

229: \newenvironment{definition}{\begin{Definition} \rm}

230: {\end{Definition}}

231: 

232: \newenvironment{proof}[1]

233: {\par\par\vspace{\topsep}\noindent{\bf Proof #1.}\rm} {\hfill$\square$\\}

234: 

235: \def\|{\ensuremath{\ \mid}}

236: \def\per{\ensuremath{\mathbf .\ }\xspace}

237: 

238: \newcommand{\xput}[2]{\put(#1){\makebox(0,0){$#2$}}}

239: 

240: \newcommand{\biggOr}[1]{\underset{#1}{\text{\begin{huge}$\sqcup$\end{huge}}}}

241: \newcommand{\biggAnd}[1]{\underset{#1}{\text{\begin{huge}$\sqcap$\end{huge}}}}

242: \renewcommand{\bigsqcup}[1]{\underset{#1}{\text{\begin{Large}$\sqcup$\end{Large}}}}

243: \newcommand{\bigOr}[1]{\underset{#1}{\text{\begin{Large}$\sqcup$\end{Large}}}}

244: \newcommand{\bigAnd}[1]{\underset{#1}{\text{\begin{Large}$\sqcap$\end{Large}}}}

245: 

246: \newcommand{\level}{\textsl{level}}

247: \newcommand{\depth}{\textsl{depth}}

248: 

249: \newcommand{\A}{\ensuremath{{\cal A}}}

250: %\newcommand{\I}{\ensuremath{{\cal I}}}

251: \newcommand{\atboth}[2]{\exists^{\Join#1}#2}

252: \newcommand{\atbothq}[3]{\exists^{\Join#1}#2.#3}

253: 

254: 

255: 

256: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

257: %%% INIZIO DOCUMENTO

258: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

259: 

260: \begin{document}

261: 

262: \maketitle

263: 

264: \begin{abstract}

265: Description Logics are knowledge representation formalisms

266: which have been used in a wide range of application domains.

267: Owing to their appealing expressiveness, we consider in this paper

268: extensions of the well-known concept language \ALC allowing for

269: \emph{number restrictions} on complex role expressions.

270: These have been first introduced by Baader and Sattler as

271: \ALCNX{M} languages, with the adoption

272: of role constructors $M\subseteq \set{\comp,\inv{},\Or,\And}$.

273: In particular, they showed in 1999 that, although \ALCNX{\comp}

274: is decidable, the addition of other operators may easily lead

275: to undecidability: in fact, \ALCNX{\comp,\And} and \ALCNX{\comp,\inv{},\Or}

276: were proved undecidable.

277: 

278: In this work, we further investigate the computational properties

279: of the \ALCN\ family, aiming at narrowing the decidability gap left open

280: by Baader and Sattler's results.

281: In particular, we will show that

282: \ALCNX{\comp} extended with inverse roles both in number and in value restrictions

283: %% (\ALCNoI)

284: becomes undecidable, whereas it can be safely extended

285: with qualified number restrictions without losing decidability.

286: \end{abstract}

287: 

288: %\noindent

289: %Categories and Subject Descriptors:

290: %F.2.2 [\textbf{Analysis of Algorithms and Problem Complexity}]:

291: %Nonnumerical Algorithms and Problems---\emph{Complexity of proof procedures};

292: %F.4.1 [\textbf{Mathematical Logic and Formal Languages}]:

293: %Mathematical Logic---\emph{Computational Logic};

294: %I.2.4 [\textbf{Artificial Intelligence}]:

295: %Knowledge Representation Formalisms and Methods---\emph{Modal Logic, Semantic Networks}

296: %

297: %\noindent

298: %General Terms: Theory\\

299: %\noindent

300: %Additional Key Words and Phrases: Description Logic, Decidability, Domino Problem, Tableau Algorithm

301: 

302: \noindent \textbf{Keywords:} Description Logic, Decidability, Domino Problem, Tableau Algorithm

303: 

304: \section{Introduction}

305: 

306: Description Logics (DLs) are a family of first-order formalisms that

307: have been found useful for domain knowledge representation in several

308: application fields \cite{DLbook}, from database design ---including conceptual, object-oriented,

309: temporal, multimedia and semistructured data modeling--- to software engineering

310: and ontology management (e.g. \cite{AF99,BJ92,GHB96,JLC-DL-99,KR-98,DBIS98,franconi-dood00,HS01}).

311: Different DLs provide for \emph{constructors} which can be used to

312: combine atomic \emph{concepts} (unary predicates) and \emph{roles} (binary predicates)

313: to build \emph{complex} concepts and roles. The available constructors

314: characterize the description language as to \emph{expressiveness} and

315: \emph{computational behaviour} (decidability and complexity) of the basic reasoning tasks

316: like concept satisfiability and subsumption.

317: 

318: \footnotetext{This is the extended version of a paper which appeared in

319: \emph{Proceedings of LPAR~2002 -- 9th Intl' Conf. on Logic for Programming,

320: Artificial Intelligence and Reasoning} (Tbilisi, Georgia, October 2002).}

321: \renewcommand{\thefootnote}{\arabic{footnote}}

322: \clearpage

323: 

324: Well-known Description Logics are \ALC \cite{ALC}, which allows for Boolean

325: propositional constructors on concepts and (universal and existential) value restrictions

326: on atomic roles, and its extension \ALCN \cite{ALCN1,ALCN2} introducing (non-qualified)

327: \emph{number restrictions} on atomic roles. Basic inference problems for both

328: these DLs are \PSPACE-complete \cite{ALCN1,ALCN2}.

329: %However, limited expressiveness has been sometimes pointed out as a limitation

330: %of Description Logics \cite{} and, thus,

331: However, in order to better fulfil requirements of real-world application domains,

332: more expressive extensions of the basic concept languages have been investigated.

333: One direction along which useful extensions

334: have been sought is the introduction of \emph{complex} roles under number restrictions.

335: In fact, considering role composition $(\comp)$, inversion $(^-)$, union $(\Or)$ and intersection $(\And)$,

336: %The starting point of our study is the Description Logic \ALCN\ \cite{BS99},

337: %that is the well-known \ALC language \cite{ALC} equipped with (non-qualified)

338: %\emph{number restrictions} on (possibly complex) roles ($\ALlang N$).

339: expressive extensions of \ALCN\ can be defined as \ALCNX{M} with the adoption

340: of role constructors $M\subseteq \set{\comp,\inv{},\Or,\And}$ \cite{BS99}.

341: By allowing (different kinds of) complex roles also in

342: value restrictions, %%in particular by restricting the constructors in the first ones,

343: different families of Logics can also be defined: for example \ALCpN (or \ALCregN) allows the

344: transitive closure of atomic roles (or regular roles, resp.) under value restrictions \cite{BS99,dl-expr-reas:book-99}.

345: Also Logics \ALCNNX{M}, allowing for the same types of role constructors

346: either in value \emph{and} in number restrictions, can be considered \cite{myDL01}.

347: Further extensions involve the introduction of \emph{qualified} number restrictions \cite{HB91}

348: on complex roles, giving rise to \ALCQX{M} Logics.

349: Since qualified number restrictions also allow to express value restrictions,

350: we have the inclusions $\ALCNX{M}\subseteq \ALCNNX{M}\subseteq \ALCQX{M}$ as far as

351: expressiveness (and complexity) are concerned.

352: Therefore, for instance, undecidability of \ALCNX{M} directly extends to \ALCNNX{M} and \ALCQX{M},

353: whereas decidability of \ALCQX{M} implies decidability of \ALCNX{M} and \ALCNNX{M}.

354: \begin{figure}[t]

355: {\small

356: \begin{center}

357:     $\begin{array}%

358:     {r@{\hspace*{+.5ex}}c@{\hspace*{+.5ex}}l@{\hspace*{1em}}rcl}

359:       C,D & \rightarrow\

360:         & A \mid &  \Int A\subseteq\Int\Delta && \text{atomic concept}\\

361:       & & \Top \mid & \Int\Top &=& \Int\Delta \\

362:       & & \Bot \mid & \Int\Bot &=& \emptyset \\

363:       & & \Not C  \mid & \Int{(\Not C)} &=& \Int\Delta \setminus \Int C \\

364:       & & C\And D \mid & \Int{(C\And D)} &=& \Int C \cap \Int D \\

365:       & & C\Or D \mid & \Int{(C\Or D)} &=& \Int C \cup \Int D\\

366:       & & \all{R}{C} \mid & \Int{(\all{R}{C})} &=&

367:           \set{i\in\Int\Delta\mid\forall j\per\Int R(i,j)\Rightarrow\Int C(j)}\\

368:       & & \some{R}{C} \mid & \Int{(\some{R}{C})} &=&

369:           \set{i\in\Int\Delta\mid\exists j\per\Int R(i,j)\wedge\Int C(j)} \\

370:       & & \atleast{n}{R} \mid & \Int{(\atleast{n}{R})} &=&

371:           \set{i\in\Int\Delta\mid\sharp

372:           \set{j\in\Int\Delta\mid \Int R(i,j)} \geq n} \\

373:       & & \atmost{n}{R} \mid & \Int{(\atmost{n}{R})} &=&

374:           \set{i\in\Int\Delta\mid\sharp

375:           \set{j\in\Int\Delta\mid \Int R(i,j)} \leq n} \\

376:       & * & \atleastq{n}{R}{C} \mid & \Int{(\atleastq{n}{R}{C})} &=&

377:           \set{i\in\Int\Delta\mid\sharp

378:           \set{j\in\Int\Delta\mid \Int R(i,j)\wedge \Int C(j)} \geq n} \\

379:       & * & \atmostq{n}{R}{C} \mid & \Int{(\atmostq{n}{R}{C})} &=&

380:           \set{i\in\Int\Delta\mid\sharp

381:           \set{j\in\Int\Delta\mid \Int R(i,j)\wedge \Int C(j)} \leq n} \\

382:       R, S & \rightarrow\

383:         & P \mid & \Int P\subseteq\Int\Delta \times\Int\Delta && \text{atomic role} \\

384: %%      & & R^+ \mid & \Int{(R^+)} &=& \cup_{i\geq 1} (\Int R)^i \\ %%% &&\text{(extensions:)} &&&\\

385:       & * & \inv{R} \mid & \Int{(\inv{R})}  &=&  \set{ (i,j)\in\Int\Delta\times\Int\Delta\mid

386:            \Int R(j,i) } \\

387:       & * & R \comp S \mid & \Int{(R\comp S)} &=&  \set{(i,j)\in\Int\Delta\times\Int\Delta\mid

388:           \exists k\per \Int R(i,k) \wedge \Int S(k,j) } \\

389: %%      & * & R \Or S \mid & \Int{(R\Or S)} &=& \Int R \cup \Int S \\

390: %%      & * & R \And S & \Int{(R\And S)} &=& \Int R \cap \Int S

391:     \end{array}$

392: \end{center}\vspace{-1em}

393: } \caption{\label{ALCN} Syntax and model-theoretic semantics of \ALCN

394: and its extensions (marked with $\ast$) considered in this paper.

395: %% equipped with role constructors in $\set{\comp,\inv{},\Or,\And}$ or qualified number restrictions.

396: }

397: \end{figure}

398: 

399: 

400: %As a matter of fact, expressive Description Logics \cite{dl-expr-reas:book-99}

401: %possibly providing for (qualified) number restrictions

402: %have been used for solving interesting

403: %reasoning tasks in the fields of knowledge representation and conceptual modeling

404: %(e.g. for reasoning on database schemata \cite{DBIS98,coopis98,franconi-dood00}).

405: %In this respect, the characterization of the computational behaviour of such description languages

406: %is the foundation to ground their effective usability in applications.

407: 

408: Our investigation is aimed at improving the (un)decidability results presented

409: by Baader and Sattler in \cite{BS99} for \ALCN\ extensions including composition of roles ($\comp$).

410: In particular, they proved that concept satisfiability in \ALCNX{\comp,\And} and \ALCNX{\comp,^-,\Or}

411: %(and, thus, in  \ALCNNX{\comp,\And} and \ALCNNX{\comp,^-,\Or})

412: is undecidable via reduction of a domino problem,

413: %and undecidability of \ALCNNX{^+,\comp} is a straightforward consequence

414: %of their results for \ALCpNX{\comp}.

415: and provided a sound and complete

416: Tableau algorithm for deciding satisfiability of \ALCNX{\comp}-concepts.

417: Furthermore, we recently proved that concept satisfiability is decidable in \ALCNX{\comp,\Or},

418: by providing a Tableau algorithm for the purpose \cite{myDL03}.

419: Moreover, it can easily be proved (using the Role Normal Form introduced in \cite{myDL03}) that

420: \ALCNNX{\comp,\Or} is simply a syntactic variant of \ALCNX{\comp,\Or}.

421: Baader and Sattler also observed in \cite{BS99} that \ALCNX{^-,\Or,\And} %%\cite{BS99}, \ALCNNX{^-,\Or,\And} and all their sublanguages

422: is decidable since \ALCNX{^-,\Or,\And}-concepts

423: can easily be translated into a formula in \Cdue\ \cite{C2}, that is

424: the two-variable FOL fragment with counting quantifiers, which has proved to be

425: decidable \cite{decC2}. In fact, satisfiability of \Cdue formulae can be decided

426: in \NEXPTIME \cite{complC2} if unary coding of numbers is used (which is a common assumption in the field

427: of DLs; if binary coding is adopted we have a \DNEXPTIME upper bound).

428: We can further observe that a similar translation is still possible

429: when \emph{qualified} number restrictions   %\cite{}

430: are considered and, thus, also  \ALCQX{^-,\Or,\And} and \ALCNNX{^-,\Or,\And}

431: are decidable.

432: 

433: 

434: %Baader and Sattler also presented in \cite{BS99} a sound and complete

435: %Tableau algorithm for deciding satisfiability of \ALCNX{\comp}-concepts;

436: %anyway, the decidability of other \ALCNX{\comp} extensions beyond the undecidable \ALCNNX{^+,\comp}

437: %is still unknown.

438: %For example, to the best of our knowledge, decidability of \ALCNX{\comp,\inv{}} (and  \ALCNNX{\comp,\inv{}})

439: %is still an open problem \cite{BS99,dl-expr-reas:book-99}.

440: %Moreover, whereas \ALCpNX{\inv{}} is known to be decidable (due to the results of De Giacomo and Lenzerini

441: %in \cite{KR-96}), it is not known what happens to its extension with a \emph{unrestricted} use

442: %of transitive closure \ALCpNX{^+,^-}, and further to  \ALCNNX{^+,^-}.

443: %Other extensions with potential interest for applications

444: %are also \ALCNNX{^+,\Or} and \ALCNNX{^+,\And}.

445: 

446: In this paper, we consider extensions of \ALCNX{\comp}

447: with role inversion ($\cal I$) or qualified number restrictions ($\cal Q$),

448: whose decidability status, to the best of our knowledge, is still unknown.

449: In particular, we will show in Sec.~\ref{undec1} (via reduction of a domino problem)

450: undecidability of \ALCNX{\comp} extended with inverse roles

451: both in value and in number restrictions (which we can call \ALCNoI, but

452: we also show in Sec.~\ref{undec1} that it is a syntactic variant of \ALCNNX{\comp,^-})

453: is undecidable.

454: This result implies undecidability of \ALCQX{\comp,^-},

455: whereas decidability of ``pure'' \ALCNX{\comp,^-} remains an open question.

456: On the other hand, we will show how the decidability results of \cite{BS99}

457: lift up to \ALCQX{\comp}. In particular, we will show in Sec.~\ref{dec2}

458: that \ALCQX{\comp}-concept satisfiability is decidable and provide

459: an effective decision procedure in the form of a tableau-based algorithm,

460: which extends the \ALCNX{\comp} Tableau proposed by Baader and Sattler \cite{BS99}.

461: In a similar way as done in \cite{BS99}, we will also show that the

462: decision algorithm can be extended to cope with qualified number restrictions

463: on union and/or intersections of role chains of the same length.

464: Conclusions will eventually be found in Section~4.

465: 

466: \subsection*{Preliminaries on Description Logics}

467: 

468: Description Logics expressiveness is based on the definition

469: of complex concepts and roles, which can be built with the help

470: of available constructors, starting from a set of (atomic) concept names \NC\

471: and a set of (atomic) role names \NR. A DL system, enabling concept descriptions

472: to be interrelated, allows the derivation of implicit knowledge from

473: explicitly represented knowledge by means of inference services.

474: For a full account of Description Logics, the reader is referred, for example,

475: to \cite{DLbook}.

476: 

477: In the DL \ALC \cite{ALC}, concept descriptions are formed using the constructors

478: negation, conjunction and disjunction, value (and existential) restrictions.

479: The DL \ALCN \cite{ALCN1,ALCN2} additionally allows for unqualified (at-least and at-most)

480: number restrictions on atomic roles.

481: The syntax rules at the left hand side of Fig.~\ref{ALCN} inductively define

482: valid concept and role expressions for \ALCN and its extensions

483: considered in this paper.

484: As far as semantics is concerned, concepts are interpreted as sets of individuals

485: and roles as sets of pairs of individuals. Formally, an \emph{interpretation} is

486: a pair $\I=(\Int\Delta, \Int\cdot )$, where $\Int\Delta$ is a non-empty set of individuals

487: (the \emph{domain} of $\I$) and $\I$ is a function (the \emph{interpretation function})

488: which maps each concept to a subset of $\Int\Delta$ and each role to a subset of $\Int\Delta\times\Int\Delta$,

489: such that the equations at the right hand side of Fig.~\ref{ALCN} are satisfied.

490: One of the most important inference services of DL systems used in knowledge-representation

491: and conceptual modeling applications is computing the subsumption hierarchy

492: of a given finite set of concept descriptions.

493: \begin{definition}

494: The concept description $C$ is \emph{satisfiable} iff there exist an interpretation $\I$ such that

495: $\Int C \neq\emptyset$; in this case, we say that $\I$ is a model for $C$.

496: The concept description $D$ \emph{subsumes} the concept description $C$

497: (written $C\Implies D$) iff $\Int I\subseteq\Int D$ for all interpretations $\I$; concept

498: descriptions $C$ and $D$ are \emph{equivalent} iff $C\Implies D$ and $D\Implies C$.

499: \end{definition}

500: Since \ALC\ is propositionally complete, subsumption can be reduced to concept satisfiability

501: and \emph{vice versa}: $C\Implies D$ iff $C\And\Not D$ is unsatisfiable and $C$ is satisfiable

502: iff not $C\Implies A\And\Not A$, where $A$ is an arbitrary concept name.

503: 

504: In \ALCN, number restrictions can be used to restrict the cardinality of the set of fillers of roles

505: (role successors). For instance, the concept description:

506: \begin{center}\tt

507: $\atmost{3}{ \text{child} } \And \all{ \text{child} }{ \text{Female} }$

508: \end{center}

509: defines individuals who have at most three daughters and no sons.

510: %\ALCNX{\comp} \cite{BS99} allows counting successors of role chains,

511: %which can be used to express interesting cardinality constraints on the interrelationships

512: %some individuals hold with other objects of the domain.

513: Moreover, \ALCNX{\comp} \cite{BS99} allows counting successors of role chains in concept descriptions,

514: which can be used to express interesting cardinality constraints on the indirect interrelationships

515: some individuals hold with other objects of the domain.

516: For example, the \ALCNX{\comp}-concept:

517: \begin{center}\tt

518: Man $\!\And \;\atleast{50}{ \text{(friend$\,\comp\,$tel\_number)}  }$

519: \end{center}

520: allows us to define men for which the count of different telephone numbers

521: of their friends amounts at least to fifty.

522: % having friends who have a total of at least fifty telephone numbers.

523: Notice that such description does not impose further constraints (disregarding obvious ones)

524: either on the number of friends one may have, or on the number of telephone numbers each friend may

525: have  (e.g. some friends might have no telephone at all), or even on the fact that some numbers

526: may be shared by more than one friends (e.g. if husband and wife).

527: It only gives, for example, a constraint on the minimum size of a phonebook such men need.

528: %: for instance, the description could be either satisfied by an individual

529: %with a unique friend who has fifty different numbers (though unlikely) or by an individual

530: %with one hundred friends, twenty of which have no telephone at all and the remaining

531: %friends do not share more than thirty numbers altogether (

532: 

533: The additional role constructs we consider in this paper

534: further improve the expressiveness of the resulting DLs

535: and, thus, make them very appealing from an application viewpoint.

536: For instance, we may use

537: %the \ALCNX{\comp,\Or}-concept:

538: %\begin{center}\tt

539: %Person $\!\And \;\atleast{2}{ \text{(live\_in$\,\Or\,$child$\,\comp\,$born\_in)} } $

540: %\end{center}

541: %to define persons having at least one child born in a city different from

542: %the one they live in, or

543: the \ALCNNX{\comp,\inv{}}-concept:

544: %\begin{center}\tt

545: %Person $\!\And \;\atmost{1}{ \text{($\inv{\text{child}}\,\comp\,$child)}  }$

546: %\end{center}

547: \begin{center}\tt

548: %Person $\!\And \;\exists \inv{\text{child}} \And\!

549: Person $\!\And \;\some{ \inv{\text{child}} }{\,\text{Person}}\And\!

550: \;\atmost{1}{ \text{($\inv{\text{child}}\,\comp\,$child)}  }$

551: \end{center}

552: to define persons who are a only child, or the \ALCQX{\comp} concept:

553: \begin{center}\tt

554: Woman $\!\And \;\atleastq{3}{ \text{(husband$\,\comp\,$brother)} }{\,\text{Lawyer} }$

555: \end{center}

556: to describe women having at least three lawyers as brother-in-law.

557: 

558: 

559: \begin{figure}[tH]

560: \begin{center}

561: \begin{scriptsize}

562: \setlength{\unitlength}{0.23mm}

563: \begin{picture}(400,500)(0,-75)

564: 

565: %\xput{0,0}{\aleph}

566: 

567: \newsavebox{\cell}

568: \sbox{\cell}{

569: %\begin{picture}(100,100)

570: \xput{50,50}{\bullet}

571: %\xput{0,0}{\bullet}\xput{100,0}{\bullet}%\xput{0,100}{\bullet}\xput{100,100}{\bullet}

572: \put(45,45){\vector(-1,-1){40}}\put(55,55){\vector(1,1){40}}

573: \put(45,55){\vector(-1,1){40}}\put(55,45){\vector(1,-1){40}}

574: \dottedline[$\cdot$]{8}(0,70)(0,0)(100,0)(100,70)

575: \dottedline[$\cdot$]{8}(0,100)(100,100)

576: \matrixput(0,0)(40,0){2}(0,70){2}{\xput{30,15}{R}}

577: %\matrixput(0,0)(60,0){2}(0,30){2}{\xput{20,35}{R}}

578: %\end{picture}

579: \put(25,40){\vector(2,1){20}}

580: \dashline{4}(5,30)(21,38)

581: \xput{20,50}{U}

582: }

583: 

584: \matrixput(100,0)(100,0){5}(0,100){5}{\xput{0,0}{\bullet}}

585: \matrixput(100,0)(100,0){4}(0,100){4}{\usebox{\cell}}

586: 

587: \matrixput(100,0)(300,0){2}(0,300){2}{\xput{0,-15}{A_{00}}\xput{100,-15}{A_{10}}}

588: \matrixput(100,0)(300,0){1}(0,300){2}{\xput{200,-15}{A_{20}}}

589: \matrixput(100,100)(300,0){2}(0,300){2}{\xput{0,-15}{A_{01}}\xput{100,-15}{A_{11}}}

590: \matrixput(100,100)(300,0){1}(0,300){2}{\xput{200,-15}{A_{21}}}

591: \multiput(100,200)(300,0){2}{\xput{0,-15}{A_{02}}\xput{100,-15}{A_{12}}}

592: \put(100,200){\xput{200,-15}{A_{22}}}

593: 

594: %\matrixput(150,50)(300,0){2}(0,300){2}{\xput{0,20}{C_{00}}}

595: %\multiput(250,50)(0,300){2}{\xput{0,20}{C_{10}}\xput{100,20}{C_{20}}}

596: %\multiput(150,150)(300,0){2}{\xput{0,20}{C_{01}}\xput{0,120}{C_{02}}}

597: %\xput{250,170}{C_{11}}

598: %\xput{350,170}{C_{21}}

599: %\xput{250,270}{C_{12}}

600: %\xput{350,270}{C_{22}}

601: \matrixput(150,50)(300,0){2}(0,300){2}{\xput{20,0}{C_{00}}}

602: \multiput(250,50)(0,300){2}{\xput{20,0}{C_{10}}\xput{120,0}{C_{20}}}

603: \multiput(150,150)(300,0){2}{\xput{20,0}{C_{01}}\xput{20,100}{C_{02}}}

604: \xput{270,150}{C_{11}}

605: \xput{370,150}{C_{21}}

606: \xput{270,250}{C_{12}}

607: \xput{370,250}{C_{22}}

608: 

609: \xput{-80,30}{U}

610: \xput{-120,-80}{s}

611: \xput{-105,-76}{\bullet}

612: \put(-101,-73){\line(2,1){226}}

613: %%%%\drawline(-100,-75)(125,40)

614: %\put(-101,-73){\line(1,6){20}}

615: %\put(-101,-73){\line(1,5){30}}

616: %\put(-101,-73){\line(1,4){40}}

617: \put(-101,-73){\line(1,3){20}}

618: \put(-101,-73){\line(1,2){60}}

619: \put(-101,-73){\line(2,3){80}}

620: \put(-101,-73){\line(3,4){80}}

621: \put(-101,-73){\line(3,5){90}}

622: \put(-101,-73){\line(4,5){80}}

623: \put(-101,-73){\line(5,6){95}}

624: \put(-101,-73){\line(1,1){70}}

625: \put(-101,-73){\line(3,2){80}}

626: \put(-101,-73){\line(4,3){85}}

627: \put(-101,-73){\line(5,3){80}}

628: \put(-101,-73){\line(5,4){95}}

629: \put(-101,-73){\line(6,5){85}}

630: \put(-101,-73){\line(3,1){80}}

631: \put(-101,-73){\line(4,1){90}}

632: \put(-101,-73){\line(5,1){100}}

633: \put(-101,-73){\line(6,1){110}}

634: \put(-101,-73){\line(1,0){30}}

635: 

636: %\drawline(-101,-73)(-70,-20)

637: 

638: \end{picture}

639: \end{scriptsize}

640: \end{center}

641: \caption{\label{grid2} The grid structure used in the \ALCNNX{\comp,^-} undecidability proof.}

642: \end{figure}

643: 

644: 

645: \section{Undecidability of \ALCNNX{\comp,^-}} \label{undec1}

646: We consider in this Section the extension of $\ALCNX{\comp}$ by inverse roles ($\I$).

647: Notice that allowing the use of role inversion both in number and in value restrictions,

648: we obtain a Logic which is a syntactic variant of $\ALCNNX{\comp,^-}$.

649: Obviously, \ALCNoI concept descriptions are also \ALCNNX{\comp,^-}  concept descriptions.

650: Conversely, by recursively applying rules $(R\comp S)^- = S^-\comp R^-$

651: (pushing inverses inwards and eliminating parentheses) and $(R^-)^- = R$,

652: we can put any $\ALCNNX{\comp,^-}$ complex role expression in the form

653: $\bar R_1\comp\bar R_2\comp\cdots\comp\bar R_n$,

654: where each $\bar R_i$ is either an atomic role or the inverse of an atomic role

655: ($\bar R_i\in\set{R_i,R_i^-}$).

656: Then we can get rid of role composition in value restrictions thanks to the

657: following equivalences:

658: \begin{eqnarray*}

659:   \some{(\bar R_1\comp\bar R_2\comp\cdots\comp\bar R_n)}{C} &\equiv& \some{\bar R_1}{ \some{\bar R_2}{\cdots \some{\bar R_n}{C} } }\\

660:   \all{(\bar R_1\comp\bar R_2\comp\cdots\comp\bar R_n)}{C} &\equiv& \all{\bar R_1}{ \all{\bar R_2}{\cdots \all{\bar R_n}{C} } }

661: \end{eqnarray*}

662: This procedure gives an effective translation of concept descriptions from \ALCNNX{\comp,^-} to {\ALCNoI}.

663: 

664: 

665: To show undecidability of \ALCNNX{\comp,^-}, borrowing the proof procedure from \cite{BS99},

666: we use a reduction of the well-known undecidable domino problem \cite{domino}:

667: %

668: \begin{Definition}

669: A tiling system ${\cal D} = (D,H,V)$ is given by a non-empty set $D=\set{D_1,\ldots,D_m}$

670: of domino types, and by horizontal and vertical matching pairs $H\subseteq D\times D$,

671: $V\subseteq D\times D$. The (unrestricted) domino problem asks for a compatible tiling

672: of the plane, i.e. a mapping $t: \Z\times\Z \rightarrow D$ such that,

673: for all $m,n\in \Z$,

674: \begin{eqnarray*}

675:   \langle\, t(m,n),t(m+1,n) \,\rangle \in  H %$ and

676: & \text{and} &

677:   \langle\, t(m,n),t(m,n+1) \,\rangle \in  V %.

678: \end{eqnarray*}

679: \end{Definition}

680: %Since a compatible tiling of the first quadrant yields a compatible tiling of the whole plane

681: %\cite{dominoK}, the undecidability result extends also to an alternative definition of

682: %tiling system where the first quadrant $\N\times\N$ substitutes the whole plane  $\Z\times\Z$.

683: 

684: We will show reducibility of the domino problem to \emph{concept satisfiability} in

685: \ALCNNX{\comp,^-}. In particular, we show how a given tiling system $\cal D$

686: can be translated into a concept $E_{\cal D}$ which is satisfiable

687: iff $\cal D$ allows for a compatible tiling.

688: Following the same lines of undecidability proofs in \cite{BS99}, such translation

689: can be split into three subtasks which can be described as follows:

690: \begin{description}

691:   \item[Grid specification] It must be possible to represent a ``square'' of $\Z\times\Z$,

692: which consists of points $(m,n),(m+1,n),(m,n+1)$ and $(m+1,n+1)$, in order to yield a

693: complete covering of the plane via a repeating regular grid structure.

694: The idea is to introduce concepts to represent the grid points and role expressions to represent

695: the $x$- and $y$-successor relations. % between points.

696: %to describe that an individual (a point $(m,n)$), and that the $x$-successor of the $y$-successor

697: %coincides with the $y$-successor of the $x$-successor (i.e. the point $(n+1,m+1)$).

698:   \item[Local compatibility] It must be possible to express that a tiling is locally compatible, that is

699: that the $x$-successor and the $y$-successor of a point have an admissible domino type.

700: The idea is to associate each domino type $D_i$ with an atomic concept $D_i$, and to express

701: the horizontal and vertical matching conditions via value restrictions.

702:   \item[Total reachability] It must be possible to impose the above local conditions on all points

703: in $\Z\times\Z$. This can be achieved by constructing a ``universal'' role and a ``start''

704: individual such that every grid point can be reached from the start individual. The local

705: compatibility conditions can then be globally imposed via value restrictions.

706: \end{description}

707: 

708: 

709: %\subsubsection{Grid Specification}

710: The grid structure that we will use to tile the plane is shown in Fig.\ref{grid2}.

711: In particular, in addition to grid points, we also consider ``centers'' of grid squares,

712: which are connected to grid square vertices by means of a role named $R$.

713: All grid cell centers are instances

714: of the $C$ concept, whereas grid points are instances of the $A$ concept.

715: We introduce nine different (disjoint) types of grid centers via the concepts $C_{ij}$ ($0\leq i,j\leq 2)$

716: and nine different types of (disjoint) grid points via the concepts $A_{ij}$ ($0\leq i,j\leq 2)$, as follows:

717: \begin{eqnarray*}

718: C & := &  \biggOr{0\leq i,j\leq 2}

719: \bigg(

720:        C_{ij}\And ( \biggAnd{\substack{0\leq k,\ell\leq 2\\ (i,j)\neq (k,\ell)}} \Not C_{k\ell} )

721: \bigg)\\ %\And \Not A \\

722: A & := &  \biggOr{0\leq i,j\leq 2}

723: \bigg(

724:        A_{ij}\And ( \biggAnd{\substack{0\leq k,\ell\leq 2\\ (i,j)\neq (k,\ell)}} \Not A_{k\ell} )

725: \bigg) \And \Not C

726: \end{eqnarray*}

727: 

728: \begin{table}

729: \begin{equation*}

730:   \begin{array}{|llc|}\hline

731:     R\text{-successors} & (R\comp R^-)\text{-successors} & C_{ij}\text{-types}\\ \hline\hline

732:     A_{ij} & C_{ij} & \ding{202} \\

733:            & C_{i\oplus 2,j}& \ding{203} \\

734:            & C_{i, j\oplus 2}& \ding{204} \\

735:            & C_{i\oplus 2,j\oplus 2} & \ding{205} \\ \cline{2-2}

736:     A_{i\oplus 1,j}

737:            & C_{i\oplus 1,j} & \ding{206}  \\

738:            & C_{i\oplus 1\oplus 2,j} = C_{ij} & \ding{192} \\

739:            & C_{i\oplus 1, j\oplus 2} & \ding{207} \\

740:            & C_{i\oplus 1\oplus 2,j\oplus 2} = C_{i,j\oplus 2} & \ding{194} \\ \cline{2-2}

741:     A_{i,j\oplus 1}

742:            & C_{i,j\oplus 1} & \ding{208} \\

743:            & C_{i\oplus 2,j\oplus 1} & \ding{209} \\

744:            & C_{i, j\oplus 1\oplus 2} = C_{ij} & \ding{192} \\

745:            & C_{i\oplus 2,j\oplus 1\oplus 2} = C_{i\oplus 2,j} & \ding{193} \\  \cline{2-2}

746:     A_{i\oplus 1,j\oplus 1}

747:            & C_{i\oplus 1,j\oplus 1} & \ding{210} \\

748:            & C_{i\oplus 1\oplus 2,j\oplus 1} = C_{i,j\oplus 1} & \ding{198} \\

749:            & C_{i\oplus 1, j\oplus 1\oplus 2} = C_{i\oplus 1,j} & \ding{196} \\

750:            & C_{i\oplus 1\oplus 2,j\oplus 1\oplus 2} = C_{ij} & \ding{192} \\ \hline

751:   \end{array}

752: \end{equation*}

753: \caption{\label{tab1}

754: Types of the $R$- and $(R\comp R^-)$-successors of a $C_{ij}$-type grid center.

755: In the last column, numbers on black ground mark different $C_{ij}$-types the first time

756: they are met from the top of the table, whereas numbers on white ground refer to

757: $C_{ij}$-types that have been met before.}

758: \end{table}

759: 

760: %In order to understand how the grid construction can be enforced, we start from

761: %having a look at the concept $E_{\cal D}$ that will be used to solve the {\bf Total reachability} task.

762: %Its definition introduces another role, $U$,

763: %which connects a start individual $s$ with all the grid centers, such that

764: %%\noindent{\bf Total reachability} is ensured by the fact that

765: %%every grid center is a $U$-successor of the start individual $s$

766: %%and

767: %every grid point is a $(U\comp R)$-successor of $s$:

768: %%by means of the following concept:

769: 

770: %Let the start individual $s$ be an instance of $E_{\cal D}$.

771: %It has at least one $U$-successor (that cannot be $s$ itself,

772: %as $\atmost{0}{U^-}$ forbids $U$-loops around it), and

773: %all its $U$-successors must have $s$ as their unique $U$-predecessor,

774: %since $\exactly{1}{U\comp U^-}$ ensures that, from $s$, at most one

775: %point can be reached through the path $U\comp U^-$ (and, obviously,

776: %$s$ is on the path). All its $U$-successors are grid centers

777: %(i.e. instances of $C_{\boxplus}$, see below) and, thus, have $R$-successors.

778: %%Hence $s$ has also at least one $(U\comp R)$-successor

779: %%(that cannot be $s$ itself)

780: %Moreover, they have $s$ as their unique $(u\comp R)$-predecessor,

781: %since $\atmost{1}{U\comp R\comp R^-\comp U^-}=

782: %\atmost{1}{(U\comp R)\comp (U \comp R)^-}$  ensures that, from $s$, at most one

783: %point can be reached through the path $U\comp R\comp R^-\comp U^-$ (and, obviously,

784: %$s$ is on the path).

785: %Notice that, as a consequence, all the points that are reached from $s$

786: %through $U\comp R\comp R^-$ are instances of $C_{\boxplus}$,

787: %since they are also $U$-successors of $s$.

788: 

789: \noindent{\bf Grid specification} can then be accomplished by means of the $C_\boxplus$

790: and $A_\boxplus$ concepts which follow:

791: %replacing expression $\exactly{3}{(X_0\Or Y_0)^+}$

792: %with $\exactly{3}{(R\And T_{00})^+}$ (or even simply with $\exactly{3}{T_{00}^+}$), and so on.

793: \begin{eqnarray*}

794: C_{\boxplus} & := & C\And \atmost{4}{R}

795:                      \And \all{R}{A_{\boxplus}} %%\And \exactly{4}{\inv R} )}

796:                      \And \atmost{9}{R\comp R^-} \And \\ %%\exactly{16}{R\comp R^-\comp R} \And \\

797: && \biggAnd{0\leq i,j\leq 2}

798: \big(

799:        C_{ij}\Rightarrow (

800:  \some{R}{A_{ij}}\And\some{R}{A_{i\oplus 1,j}} \And %\\

801: %&& \qquad\qquad

802:    \some{R}{A_{i,j\oplus 1}}\And \some{R}{A_{i\oplus 1,j\oplus 1}} ) \big) \\

803: A_{\boxplus} & := & A\And

804: %\exactly{4}{R^-}  \And

805: %                    \all{R^-}{C} \And \\ %%  (A\And \exactly{4}{\inv R})}

806: %&&

807: \biggAnd{0\leq i,j\leq 2}

808: \big(

809:        A_{ij}\Rightarrow (

810:  \some{R^-}{C_{ij}}\And\some{R^-}{C_{i\oplus 2,j}} \And %\\

811: %&& \qquad\qquad

812:    \some{R^-}{C_{i,j\oplus 2}}\And \some{R^-}{C_{i\oplus 2,j\oplus 2}} ) \big) \\

813: \end{eqnarray*}

814: where $A\Rightarrow B$ is a shorthand for $\Not A\Or B$

815: and $a\oplus b=(a+b)\bmod 3$.

816: 

817: Some relevant constraints that are imposed by these concept descriptions

818: on their models are studied in the Lemmata and Corollaries which follow.

819: %

820: \begin{lemma}\label{lemma10}

821: Let $c$ be an instance of $C_{\boxplus}$. Then it has at most one $R$-successor

822: in each of the nine $A_{k\ell}$ concept extensions.

823: %Let $a$ be an instance of $A_{\boxplus}$. Then it has at most one $(R^-)$-successor

824: %in each of the nine $C_{ij}$ concept extensions.

825: \end{lemma}

826: \textbf{Proof}

827: More precisely, $c$ has exactly one $R$-successor

828: in the extension of each of the four $A_{k\ell}$ concepts it is connected to by $R$

829: (e.g. if w.l.o.g. $c\in\Int{(C_{ij})}$ then $c$ has exactly one $R$-successor

830: in the extension of $A_{ij}$, $A_{i\oplus 1,j}$, $A_{i,j\oplus 1}$, $A_{i\oplus 1,j\oplus 1}$

831: and no $R$-successor in any of the remaining five partitions of the extension of $A$).

832: This follows from the fact that the nine $A_{k\ell}$ concepts are disjoint

833: and $c$ has a total number of at most four $R$-successors.

834: \QED

835: 

836: \begin{lemma}\label{lemma11}

837: Let $c$ be an instance of $C_{\boxplus}$. Then it has exactly one $(R\comp R^-)$-successor

838: in each of the nine $C_{k\ell}$ concept extensions.

839: \end{lemma}

840: \textbf{Proof}

841: Since $c$ is an instance of $C$, it belongs to the extension of exactly one of the nine $C_{k\ell}$ concepts.

842: %Moreover, $c$ has exactly four $R$-successors, which are instances of $A_{\boxplus}$.

843: %In particular, such successors are

844: %nine different types of grid cells can be defined according to the type of their center:

845: %(and the type $A_{ij}$ of their bottom left vertex).

846: %an $(i,j)$-type grid cell has a $C_{ij}$-type center, while its lower left, lower right,

847: %upper left and upper right vertices are

848: %instances of the $A_{ij}$, $A_{i\oplus 1,j}$, $A_{i,j\oplus 1}$

849: %and $A_{i\oplus 1,j\oplus 1}$ concepts, where $a\oplus b=(a+b)\bmod 3$.

850: W.l.o.g. let us assume $c\in\Int{(C_{ij})}$. Hence,

851: owing to the $C_{\boxplus}$ and $A_{\boxplus}$ definitions and Lemma~\ref{lemma10},

852: $c$ has surely $R$-

853: and $(R\comp R^-)$-successors as shown in Tab. \ref{tab1}. In particular, $c$

854: %$c_{ij}$ has four distinct $R$-successors (which are instances of $A_{\boxplus}$), and it

855: has $(R\comp R^-)$-successors in each of the nine $C_{k\ell}$ concept extensions.

856: Since all the $C_{k\ell}$ extensions are disjoint and $c$ has a total of at most nine

857: $(R\comp R^-)$-successors, this means that $c$ has exactly one $(R\comp R^-)$-successor in each

858: of the nine $C_{k\ell}$ concept extensions (being $c$ itself its unique $(R\comp R^-)$-successor

859: in $C_{ij}$). \QED

860: 

861: \begin{corollary}\label{coro10}

862: Let $a$ be an instance of $A_{\boxplus}$. Then (1) all its $(R^-)$-successors are

863: instances of $C_{\boxplus}$ and (2) it has at most one $(R^-)$-successor

864: in each of the nine $C_{k\ell}$ concept extensions.

865: \end{corollary}

866: \textbf{Proof} It is an immediate consequence of Lemma~\ref{lemma11}.

867: W.l.o.g. assume $a\in\Int{(A_{ij})}$.

868: (1) If $a$ had an  $(R^-)$-successor $o\not\in\Int{(C_{\boxplus})}$,

869: then any of the four $(R^-)$-successors of $a$ in $C_{\boxplus}$ would have

870: at least ten $(R\comp R^-)$-successors (it has nine $(R\comp R^-)$-successors in

871: $C_{\boxplus}$ by Lemma~\ref{lemma11} plus $o$) and, thus, would violate

872: the $C_{\boxplus}$ definition.

873: (2) If $a$ had, for instance, two

874: distinct $(R^-)$-successors in $C_{k\ell}$ (i.e. $\exists c,c'\in\Int{(C_{k\ell})}$,

875: $c\neq c'$, with $(c,a)\in\Int R$, $(c',a)\in\Int R$), then

876: $c$ would have two distinct $(R\comp R^-)$-successors

877: in $C_{k\ell}$, $c'$ and itself, contradicting Lemma~\ref{lemma11}.

878: 

879: More precisely, $a$ has exactly one $(R^-)$-successor

880: in the extension of each of the four $C_{k\ell}$ concepts it is connected to by $R^-$.

881: \QED

882: 

883: \begin{corollary}\label{coro11}

884: Let $a$ be an instance of $A_{\boxplus}$. Then it has exactly one $(R^-\comp R)$-successor

885: in each of the nine $A_{k\ell}$ concept extensions.

886: \end{corollary}

887: \textbf{Proof}

888: W.l.o.g. assume $a\in\Int{(A_{ij})}$. We show that if the thesis is false

889: we come up with a contradiction. To this end, we must distinguish three cases.

890: First of all, we can exclude $a$ has another $(R^-\comp R)$-successor, say $a'$,

891: in $A_{ij}$: if this happened, each of the four $(R^-)$-successors of $a$

892: (e.g. $c\in\Int{(C_{ij})}$) would have two distinct $R$-successors ($a$ and $a'$)

893: in $A_{ij}$, thus violating Lemma~\ref{lemma10}.

894: Second, we can also exclude $a$ has two distinct $(R^-\comp R)$-successors in  $A_{k\ell}$,

895: say $a'$ and $a''$, which can be reached through a common $(R^-)$-successor $c$

896: (e.g. $c\in\Int{(C_{ij})}$): if this happened, $c$ would have two distinct $R$-successors

897: ($a$ and $a'$) in $A_{k\ell}$, against Lemma~\ref{lemma10} again.

898: In the third and last case, we must consider $a$ having two distinct $(R^-\comp R)$-successors

899: in  $A_{k\ell}$, say $a'$ and $a''$, which can be reached through distinct $(R^-)$-successors of $a$.

900: W.l.o.g. we may assume such $(R^-)$-successors of $a$ in $C_{ij}$ and $C_{i,j\oplus 2}$,

901: and $a',a''\in\Int{(A_{i\oplus 1,j})}$.

902: %

903: %W.l.o.g. we may assume

904: %$a$ has two distinct $(R^-\comp R)$-successors in $A_{i\oplus 1,j}$

905: %(i.e. $\exists a',a''\in\Int{(A_{i\oplus 1,j})}$,

906: %$a'\neq a''$, such that $a'$ and $a''$ are both $(R^-\comp R)$-successors of $a$).

907: %Notice that $a'$ and $a''$ must be reached through different paths

908: %(i.e. through $C_{ij}$ and through $C_{i,j\oplus 2}$), otherwise

909: %Lemma~\ref{lemma10} or Corollary~\ref{coro10} would be violated.

910: %

911: Hence we must have that $\exists c_0\in\Int{(C_{ij})}$ with $\set{(c_0,a),(c_0,a')}\subseteq\Int R$

912: and  $\exists c\in\Int{(C_{i,j\oplus 2})}$ with $\set{(c,a),(c,a'')}\subseteq\Int R$.

913: We then consider the application of Lemma~\ref{lemma11} from $c_0\in\Int{(C_{ij})}$.

914: By construction, $c_0$ has $c$ as $(R\comp R^-)$-successor through the path

915: passing from $a\in\Int{(A_{ij})}$. Owing to Lemma~\ref{lemma11}, also the

916: $(R\comp R^-)$ path passing from $a'\in\Int{(A_{i\oplus 1,j})}$

917: (the path exists, as $a'$ has an $(R^-)$-successor in $\Int{(C_{i,j\oplus 2})}$)

918: must lead to $c$ and, thus, $(c,a')\in\Int R$.

919: But this contradicts Lemma~\ref{lemma10}, as $c$ would have two distinct $R$-successors

920: ($a'$ and $a''$) in $\Int{(A_{i\oplus 1,j})}$. \QED

921: 

922: 

923: Hence, we will interpret instances of $C_{\boxplus}$ as grid centers

924: and instances of $A_{\boxplus}$ as grid points.

925: In particular, nine different types of grid cells can be defined according to the type of their center:

926: %(and the type $A_{ij}$ of their bottom left vertex).

927: an $(i,j)$-type grid cell has a $C_{ij}$-type center, while its lower left, lower right,

928: upper left and upper right vertices can be defined, respectively, as the instances of the

929: $A_{ij}$, $A_{i\oplus 1,j}$, $A_{i,j\oplus 1}$ and $A_{i\oplus 1,j\oplus 1}$ concepts which are connected

930: to the center via $R$ (according to the $C_{\boxplus}$ definition).

931: Therefore, the $x$- and $y$-successor relations on the grid can be defined

932: by means of the $(R^-\comp R)$-paths connecting an $A_{ij}$-type grid point

933: with an $A_{i\oplus 1,j}$-type and an $A_{i,j\oplus 1}$-type grid points, respectively.

934: Such successors always exist and are uniquely defined, owing to Corollary~\ref{coro11}.

935: 

936: In a similar way, Corollary~\ref{coro11} also allows us to uniquely define the

937: $x$- and $y$-predecessors relations on the grid, by means of the

938: $(R^-\comp R)$-paths connecting an $A_{ij}$-type grid point

939: with an $A_{i\oplus 2,j}$-type and an $A_{i,j\oplus 2}$-type grid points, respectively

940: (cf. $(a-1)\mod 3=(a+2)\mod 3$).

941: 

942: \begin{lemma}[Grid Closure]\label{lemma12}

943: For each grid point, the $(x\comp y)$-

944: and $(y\comp x)$-successors are uniquely defined and coincide.

945: \end{lemma}

946: \textbf{Proof}

947: We can assume the grid point  to represent the point $(m,n)\in\Z\times\Z$ and call it $p_{(m,n)}$.

948: W.l.o.g. we can further assume  $p_{(m,n)}$ to be the bottom left vertex of an $(i,j)$-type grid cell.

949: Therefore, $p_{(m,n)}$ is an instance of $A_{ij}$ and is an $R$-successor of the grid cell center,

950: say $c_{(m,n)}$, which is an instance of $C_{ij}$.

951: The $x$-successor of  $p_{(m,n)}$, say  $p_{(m+1,n)}$, is the $R$-successor of  $c_{(m,n)}$

952: in $A_{i\oplus 1,j}$ (by construction, it is an $(R^-\comp R)$-successor of  $p_{(m,n)}$ and is

953: unique by Corollary~\ref{coro11}).

954: Analogously, the $y$-successor of  $p_{(m,n)}$, say  $p_{(m,n+1)}$, is the $R$-successor of  $c_{(m,n)}$

955: in $A_{i,j\oplus 1}$.

956: According to the $C_{\boxplus}$ definition,  $c_{(m,n)}$ has also a fourth $R$-successor,

957: say $\bar p$, in $A_{i\oplus 1,j\oplus 1}$.

958: We consider now the  $(x\comp y)$-successor of $p_{(m,n)}$, that is the $y$-successor of $p_{(m+1,n)}$,

959: and call it $p'_{(m+1,n+1)}$. Owing to the $y$-successor definition,  $p'_{(m+1,n+1)}$

960: must be an instance of $A_{i\oplus 1,j\oplus 1}$ connected to  $p_{(m+1,n)}$ via $(R^-\comp R)$.

961: However, both $\bar p$ and $p'_{(m+1,n+1)}$ are, by construction, $(R^-\comp R)$-successors

962: of $p_{(m+1,n)}$ in $A_{i\oplus 1,j\oplus 1}$ and, thus, they must coincide thanks to Corollary~\ref{coro11}.

963: Analogously,  the  $(y\comp x)$-successor of $p_{(m,n)}$, that is the $x$-successor of $p_{(m,n+1)}$,

964: say $p''_{(m+1,n+1)}$, must be an instance of $A_{i\oplus 1,j\oplus 1}$ connected

965: to  $p_{(m,n+1)}$ via $(R^-\comp R)$. Thence, Corollary~\ref{coro11} ensures that $\bar p$

966: and  $p''_{(m+1,n+1)}$ coincide, as they are both  $(R^-\comp R)$-successors

967: of $p_{(m,n+1)}$ in $A_{i\oplus 1,j\oplus 1}$.

968: Hence, $\bar p$ is the common $(x\comp y)$-

969: and $(y\comp x)$-successor of $p_{(m,n)}$ on the grid, that can be called $p_{(m+1,n+1)}$

970: to represent the point $(m+1,n+1)$ of the plane. \QED

971: 

972: 

973: %\subsubsection{Local Compatibility}

974: \vskip 5mm

975: \noindent{\bf Local compatibility} is easily achieved by enforcing grid centers

976: to be instances of a $C_{\cal D}$ concept defined as follows:

977: \begin{align*}

978: C_{\cal D} \; := \; &

979: %\biggOr{0\leq i,j\leq 1} \bigg(

980: %                       A_{ij}\And ( \biggAnd{\scriptsize\begin{array}{c}0\leq k,\ell\leq 1\\ (i,j)\neq (k,\ell)\end{array}} \Not A_{k\ell} )

981: %  \And \some{R^-}{C_{ij}} \bigg) \And

982: %C_{\cal D} \; := \; & \biggOr{E\in\set{A,B,C,D}} \big( E\And ( \bigAnd{F\in\set{A,B,C,D}\setminus\set{E}} \Not F ) \big) \And

983: \all{R}{ \bigg( \biggOr{1\leq k\leq m} \big(

984:                        D_k\And ( \biggAnd{\substack{1\leq \ell\leq m\\ k\neq \ell}} \Not D_\ell ) \big)\,\bigg) }\And

985:   \biggAnd{0\leq i,j\leq 2}

986: \bigg(\, C_{ij}\Rightarrow \biggAnd{1\leq k\leq m} \some{R}{ (A_{ij}\And D_k)} \\

987:    & \quad\quad  \Rightarrow   \big( \, \some{R}{(A_{i\oplus 1,j}\And (\bigOr{(D_k,D_\ell)\in H} D_\ell))} \And

988:               \some{R}{(A_{i,j\oplus 1}\And (\bigOr{(D_k,D_\ell)\in V} D_\ell))} %%\And  \\

989: %%             & \some{R^-\comp R}{(A_{i\ominus 1,j}\And (\bigOr{(D_\ell,D_k)\in H} D_\ell))} \And \\

990: %%             & \some{R^-\comp R}{(A_{i,j\ominus 1}\And (\bigOr{(D_\ell,D_k)\in V} D_\ell))}

991: \, \big) \,\bigg)

992: \end{align*}

993: Each domino type $D_k$ is associated to an atomic concept with the same name. The value restriction

994: in the first conjunct of $C_{\cal D}$ forces grid points to have a domino type.

995: The second conjunct uses the definition of the $x$- and $y$-successors for the bottom left vertex

996: of an $(i,j)$-type cell to enforce horizontal and vertical matching conditions via value restrictions.

997: 

998: %\subsubsection*{Total Reachability}

999: \vskip 5mm

1000: \noindent\textbf{Total Reachability}

1001: will be achieved by constructing a ``start'' individual ($s$)

1002: and two ``universal'' roles: the former ($U$) which connects $s$ to every grid center

1003: and the latter ($U\comp R$) which connects $s$ to every grid point  (see Fig.~\ref{grid2}).

1004: The Lemmata and Corollaries which follow will justify the correctness of our construction.

1005: 

1006: \begin{lemma}\label{lemma1}

1007: Let $s$ be an instance of

1008: \begin{equation*}

1009:   D\;:=\;\exists U\comp R\And \atmost{1}{(U\comp R)\comp (U\comp R)^-}

1010: \And\Not\exists R^-\And\Not\exists U^-\And\all{U}{\Not\exists R^-}

1011: \end{equation*}

1012: in a given interpretation $\I$.

1013: Then any $(U\comp R)$-successor $x$ of $s$ in $\I$

1014: ($D$ ensures that there is at least one) has $s$ as its

1015: \emph{unique} $(U\comp R)$-predecessor.

1016: \end{lemma}

1017: \textbf{Proof} Assume $s\in\Int D$ and $x$ is a $(U\comp R)$-successor of $s$,

1018: that is $\exists o\in\Int\Delta$ such that $(s,o)\in\Int U$, $(o,x)\in\Int R$,

1019: with $o\neq s$ (as $s\not\in\Int{(\exists U^-)}$),

1020: $x\neq o$ (as $s\in\Int{(\all{U}{\Not\exists R^-})}$ and, thus, $o\not\in\Int{(\exists R^-)}$)

1021: and $s\neq x$ (as $s\not\in\Int{(\exists R^-)}$).

1022: If there were $s'\in\Int\Delta$, $s'\neq s$, such that $s'$ is a $(U\comp R)$-predecessor

1023: of $x$ (i.e. $\exists o'\in\Int\Delta$ such that $(s',o')\in\Int U$, $(o',x)\in\Int R$),

1024: then $s$ and $s'$ would be both $(R^-\comp U^-)=(U\comp R)^-$-successors of $x$ in $\I$

1025: and, thus, both $(U\comp R)\comp (U\comp R)^-$-successors of $s$ in $\I$.

1026: Hence we should have $s\not\in\Int D$, against the hypothesis. \QED

1027: 

1028: \begin{corollary}\label{corol1}

1029: Under the hypothesis of Lemma \ref{lemma1},

1030: any $U$-successor of $s$ in $\I$ has $s$ as its \emph{unique} $U$-predecessor.

1031: \end{corollary}

1032: \begin{corollary}\label{corol2}

1033: Under the hypothesis of Lemma \ref{lemma1},

1034: let $s$ be an instance of

1035: \begin{equation*}

1036:   D'\;:=\;D\And \all{U}{\all{R}{\all{R^-}{\exists U^-}}} \And\Not\exists R

1037: \end{equation*}

1038: in a given interpretation $\I$.

1039: Then any $(U\comp R\comp R^-)$-successor $y$ of $s$ in $\I$

1040: ($D$ ensures that there is at least one) is a $U$-successor of $s$ in $\I$

1041: and has $s$ as its \emph{unique} $U$-predecessor.

1042: \end{corollary}

1043: \textbf{Proof} Let $y\in\Int \Delta$ be a generic $(U\comp R\comp R^-)$-successor of $s$

1044: in $\I$, that is $\exists o,x\in\Int\Delta$ such that $(s,o)\in\Int U$, $(o,x)\in\Int R$, $(y,x)\in\Int R$

1045: (we may assume $y\neq o$, as the Corollary is trivially true for $o$),

1046: with $s\neq y$ (as $s\not\in\Int{(\exists R)}$).

1047: Since $s\in\Int{(\all{U}{\all{R}{\all{R^-}{\exists U^-}}})}$, $y\in\Int{(\exists U^-)}$,

1048: that is $\exists s'\in\Int\Delta$ such that $(s',y)\in\Int U$.

1049: Notice that both $s$ and $s'$ have, by construction, $x$ as $(U\comp R)$-successor.

1050: Since $s\in\Int D$, thanks to Lemma \ref{lemma1}, $s$ and $s'$ must coincide.

1051: Hence $y$ is a $U$-successor of $s$, which is also its unique $U$-predecessor

1052: by Corollary \ref{corol1}. \QED

1053: 

1054: \begin{lemma}[Plane Covering and Compatible Tiling] \label{lemma2}

1055: Let $s$ be an instance of

1056: \begin{eqnarray*}

1057: E_{\cal D} &:=&

1058: %\atleast{1}{U\comp R}

1059: \exists U\comp R \And \atmost{1}{(U\comp R)\comp (U \comp R)^-}

1060: \And \Not\exists R \And \Not\exists R^- \And\Not\exists U^- \And \\

1061: %% \atleast{1}{U} \And \atmost{1}{U\comp U^-} \And \atmost{0}{U^-} \And \\

1062:  & & \all{U}{\all{R}{\all{R^-}{\exists U^-}}} \And

1063:  \all{U}{( C_{\boxplus}\And %%\exists R\And  %%\atleast{4}{R\comp R^-} \And

1064: C_{\cal D} \And \Not\exists R^- )} %\\

1065: % & &  %\atleast{1}{U\comp R} \And

1066: \end{eqnarray*}

1067: in a given interpretation $\I$. Then, for the grid that tiles the plane $\Z\times\Z$,

1068: any grid center can be reached from $s$ via $U$,

1069: any grid point can be reached from $s$ via $U\comp R$ and local tiling conditions

1070: are imposed on all grid points (yielding a compatible tiling of the plane).

1071: %$E_{\cal D}$ enforces

1072: %a compatible tiling of the whole plane $\Z\times\Z$.

1073: %In particular,

1074: \end{lemma}

1075: \textbf{Proof}

1076: Let us consider a grid center connected to $s\in\Int{(E_{\cal D})}$

1077: via $U$ ($E_{\cal D}\Implies\exists U\comp R\And\all{U}{C_{\boxplus}}$ ensures that

1078: there is at least one).

1079: W.l.o.g. we can assume  it to be the center of an $(i,j)$-type cell and call it $c_{(0,0)}$

1080: ($c_{(0,0)}\in\Int{(C_{ij})}$). We can also call $p_{(0,0)}$ the bottom left vertex

1081: of this grid cell ($p_{(0,0)}\in\Int{(A_{ij})}$) and let it represent the origin $(0,0)$ of $\Z\times\Z$.

1082: We can now consider the $x$- and $y$-successors of $p_{(0,0)}$, say $p_{(1,0)}$ and $p_{(0,1)}$, respectively.

1083: By construction, we have $p_{(1,0)}\in\Int{(A_{i\oplus 1,j})}$, $p_{(0,1)}\in\Int{(A_{i,j\oplus 1})}$;

1084: moreover, either $p_{(0,0)}$, $p_{(1,0)}$ and $p_{(0,1)}$ are $R$-successors of $c_{(0,0)}$

1085: and, thus, $(U\comp R)$-successors of $s$.

1086: In the $(i,j)$-type grid cell centered on $c_{(0,0)}$, $p_{(1,0)}$ and $p_{(0,1)}$ are the

1087: bottom right and top left vertices,  but they are also the  bottom left vertices

1088: of the two grid cells adjacent to the right and to the top, respectively.

1089: In particular, $p_{(1,0)}$ and $p_{(0,1)}$ are the bottom left vertices of an $(i\oplus 1,j)$-

1090: and an $(i,j\oplus 1)$-type grid cells, whose centers we can call $c_{(1,0)}$ and $c_{(0,1)}$,

1091: respectively (the existence and uniqueness of these cells and their centers is ensured

1092: by Lemma~\ref{lemma11}). Obviously, $c_{(1,0)}$ and $c_{(0,1)}$ are

1093: ($(R\comp R^-)$-successors of $c_{(0,0)}$ and) $(R^-)$-successors

1094: of  $p_{(1,0)}$ and $p_{(0,1)}$, respectively. Therefore, they are

1095: $(U\comp R\comp R^-)$-successors of the start individual $s$ and, thanks to Corollary~\ref{corol2}

1096: (as $E_{\cal D}\Implies D'$), they are also $U$-successors of $s$.

1097: 

1098: Using the $x$- and $y$-predecessor definitions, we can easily see that the same holds for

1099: $c_{(-1,0)}$ and $c_{(0,-1)}$ grid centers. In any case, we can repeat the argument at will,

1100: starting with $c_{(1,0)}$, $c_{(0,1)}$, $c_{(-1,0)}$ and $c_{(0,-1)}$ in place of $c_{(0,0)}$,

1101: and show that the center of any grid cell on the plane can be reached from $s$ via $U$.

1102: Hence, all grid points can be reached from $s$ via $U\comp R$ and local tiling conditions

1103: are imposed on all of them by value restrictions (as $E_{\cal D}\Implies \all{U}{C_{\cal D}}$).

1104: \QED

1105: 

1106: \vskip 5mm

1107: Thanks to Lemma~\ref{lemma2}, it is easy to see that

1108: a tiling system $\cal D$ has a compatible tiling

1109: iff concept $E_{\cal D}$ is satisfiable (i.e. there is an interpretation $\I$

1110: such that $\Int{(E_{\cal D})} \neq \emptyset$).

1111: \begin{theorem}\label{th1}

1112: Satisfiability (and, thus, subsumption) of concepts

1113: is undecidable for \ALCNNX{\comp,^-} (and \ALCQX{\comp,^-}).

1114: \end{theorem}

1115: 

1116: 

1117: %\newpage

1118: 

1119: \section{Decidability of \ALCQX{\comp}} \label{dec2}

1120: 

1121: We will show in this Section how an effective decision procedure for \ALCQX{\comp}-concept

1122: satisfiability can be provided as a tableau-based algorithm.

1123: To this end, we consider \ALCQX{\comp}-concept descriptions in Negation Normal Form (NNF \cite{ALC}),

1124: where the negation sign is allowed to appear before atomic concepts only.

1125: In fact, \ALCQX{\comp}-concept descriptions can be transformed into NNF in linear time

1126: via application of the same rules which can be used for \ALCQ (pushing negations inwards):

1127: \begin{equation*}

1128: \begin{array}{cccc}

1129:  \Not \atmostq{n}{R}{C} \;=\; \atleastq{n+1}{R}{C} &&&

1130:  \Not \atleastq{n}{R}{C} \;=\; \atmostq{n-1}{R}{C} \quad (\Bot \text{ if }n=0)\\

1131: % \Not \atmost{n}{R} \;=\; \atleast{n+1}{R} &&&

1132: % \Not \atleast{n}{R} \;=\; \atmost{n-1}{R} \quad (\Bot \text{ if }n=0) \\

1133:  \Not \some{R}{C} \;=\; \all{R}{\Not C} &&&

1134:  \Not \all{R}{C} \;=\; \some{R}{\Not C} \\

1135: % \text{in addition to:} &&& \Not\Not C \;=\; C \\

1136: % \Not(C_1\And C_2) \;=\; \Not C_1 \Or \Not C_2 &&&

1137: % \Not(C_1\Or C_2) \;=\; \Not C_1 \And \Not C_2 \\

1138: \end{array}

1139: \end{equation*}

1140: in addition to the absorption rule for double negations and De Morgan's laws for $\And$ and $\Or$.

1141: Obviously, unqualified number restrictions are treated as particular cases of qualified restrictions (with $C=\Top$).

1142: We can further make use of the rules:

1143: \begin{eqnarray*}

1144: \begin{array}{cccc}

1145: \some{R}{C} \;=\; \atleastq{1}{R}{C} &&&

1146: \all{R}{C} \;=\; \atmostq{0}{R}{\Not C} % \Not \atleastq{1}{R}{\Not C} \\

1147: \end{array}

1148: \end{eqnarray*}

1149: to get rid of (existential and) value restrictions. We define the concept descriptions

1150: obtained in this way as in NNF$^{\Join}$ and denote the NNF$^{\Join}$ of the

1151: \ALCQX{\comp}-concept description $\Not C$ as $\sim C$.

1152: We will use the symbol $\Join$ in number restrictions $\atbothq{n}{R}{C}$ as a placeholder

1153: for either $\geq$ or $\leq$.

1154: 

1155: The Tableau algorithm we are going to introduce

1156: manipulates, as basic data structures, ABox assertions

1157: involving domain individuals.

1158: In fact, our algorithm is a simple extension

1159: of the tableau-based algorithm to decide \ALCNX{\comp}-concept satisfiability presented by

1160: Baader and Sattler in \cite{BS99}. The extension is based on the modification

1161: of the transformation rules for number restrictions ($\geq$- and $\leq$-rules)

1162: to take into account the ``qualifying'' conditions

1163: and on the introduction of a so-called \emph{choose} rule (called \choos-rule here),

1164: which makes sure that all ``relevant'' concepts that are implicitly satisfied by an individual

1165: are made explicit in the ABox.

1166: Basically, the proposed extension is similar to the one which extends

1167: the tableau-based \ALCN satisfiability algorithm \cite{ALCN1,ALCN2} to

1168: an \ALCQ satisfiability algorithm \cite{HB91,BS01}.

1169: 

1170: \begin{definition}

1171: Let $\NI$ be a set of individual names. An \emph{ABox} \A\ is a finite set of assertions of the form $C(a)$

1172: --\emph{concept assertion}-- or $R(a,b)$ --\emph{role assertion}-- where $C$ is a concept description, $R$ a role

1173: name, and $a,b$ are individual names.

1174: An interpretation $\I$, which additionally assigns elements $a^\I\in\dom$ to individual names $a$,

1175: is a \emph{model} of an ABox \A\ iff $a^\I\in C^\I$ (resp. $(a^\I,b^\I)\in R^\I$) for all

1176: assertions $C(a)$ (resp. $R(a,b)$) in \A.

1177: The ABox \A\ is consistent iff it has a model. The individual $a$ is an instance of the description $C$ w.r.t.

1178: \A\ iff $a^\I\in C^\I$ holds for all models $\I$ of \A.

1179: We also consider in a ABox \emph{inequality assertions} of the form

1180: $a\neq b$, with the obvious semantics that an interpretation $\I$ satisfies $a\neq b$, iff

1181: $a^\I \neq b^\I$. Inequality assertions are assumed to be symmetric, that is saying that

1182: $\set{a\neq b}\subseteq \A$ is the same as saying $\set{b\neq a}\subseteq\A$.

1183: \end{definition}

1184: Sometimes in the DL field, a \emph{unique name assumption} is made in works concerning reasoning with individuals,

1185: that is the mapping $\pi:\NI\rightarrow\dom$ from individual names to domain elements is required

1186: to be injective. We dispense from this requirement as it has no effect for the \ALC extensions studied here

1187: and the explicitly introduced inequality assertions can be used to enforce the uniqueness of names anyway.

1188: 

1189: 

1190: \begin{definition}

1191: The individual $y$ is a $(R_1\comp R_2\comp\cdots\comp R_m)$-\emph{successor} of $x$ in \A\

1192: iff $\exists y_2 y_3 \ldots y_m$ variables in \A\ such that

1193: $\set{ R_k(y_k,y_{k+1}) \mid 2\leq k\leq m-1 }\cup\set{ R_1(x,y_2),R_m(y_m,y) } \subseteq\A$. %% with $y_1=x$ and $y_{m+1}=y$.

1194: \end{definition}

1195: %Notice that, owing to this definition,

1196: %role successors in \A\ are also successors in every model $\I$

1197: %of \A: if $\I$ satisfies \A, and $y$ is an $(R_1\comp R_2\comp\cdots\comp R_m)$-successor of $x$ in \A,

1198: %then $y^\I$ is an  $(R_1\comp R_2\comp\cdots\comp R_m)$-successor of $x^\I$ in $\I$.

1199: 

1200: \begin{definition}

1201: An ABox \A\ contains a \emph{clash} iff, for an individual name $x\in\NI$, one of the two situations below occurs:

1202: \begin{itemize}

1203: \item $\set{A(x),\Not A(x)}\subseteq \A$, for a concept name $A\in\NC$;

1204: \item $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$ and

1205: $x$ has $p$ $(R_1\comp\cdots\comp R_m)$-successors $y_1,\ldots,y_p$ with $p>n$

1206: such that $\set{C(y_i)\mid 1\leq i\leq p}\cup\set{y_i\neq y_j\mid 1\leq i<j\leq p}\subseteq \A$,

1207: for role names $\set{R_1,\ldots,R_m}\subseteq\NR$, a concept description $C$ and an integer $n\geq 0$.

1208: \end{itemize}

1209: \end{definition}

1210: 

1211: To test the satisfiability of an \ALCQX{\comp} concept $C$ in NNF$^{\Join}$, the proposed \ALCQX{\comp}-algorithm

1212: works as follows. Starting from the initial ABox  $\set{C_0(x_0)}$, it applies the \emph{completion rules}

1213: in Fig.~\ref{fig:tabl1}, which modify the ABox. It stops when no rule is applicable (when a clash is generated,

1214: the algorithm does not immediately stops but it always generate a complete ABox).

1215: An ABox \A\ is called \emph{complete} iff none of the completion rules is any longer applicable.

1216: The algorithm answers ``$C$ is satisfiable'' iff a complete

1217: and clash-free ABox has been generated.

1218: The \ALCQX{\comp}-algorithm is non-deterministic, due to the $\Or$-, $\leq$- and \choos-rules

1219: (for instance, the $\Or$-rule non-deterministically chooses which disjunct to add for a disjunctive concept).

1220: 

1221: 

1222: \begin{figure}

1223: \hrule

1224: \begin{eqnarray*}

1225: \And\text{-rule: } & \text{\bf if}\quad 1. & (C_1\And C_2)(x)\in\A \text{ and} \\

1226:                    &        \;\;\;\quad 2. & \set{ C_1(x), C_2(x) }\not\subseteq \A \\

1227:                    & \text{\bf then} & \A':=\A\cup\set{ C_1(x), C_2(x) } \\

1228:  \Or\text{-rule: } & \text{\bf if}\quad 1. & (C_1\Or C_2)(x)\in\A \text{ and} \\

1229:                    &        \;\;\;\quad 2. & \set{ C_1(x), C_2(x) }\cap \A=\emptyset \\

1230:                    & \text{\bf then} & \A':=\A\cup\set{ D(x) } \text{ for some } D\in\set{ C_1,C_2 }\\

1231: %\exists\text{-rule: } & \text{\bf if}\quad 1. & (\some{R}{C})(x)\in\A \text{ and} \\

1232: %                   &        \;\;\;\quad 2. & \text{ there is no } y \text{ with } \set{ R(x,y), C(y) }\subseteq \A\\

1233: %                   & \text{\bf then} & \A':=\A\cup\set{ R(x,y), C(y) } \text{ for a fresh individual } y\\

1234: %\forall\text{-rule: } & \text{\bf if}\quad 1. & (\all{R}{C})(x)\in\A \text{ and} \\

1235: %                   &        \;\;\;\quad 2. & \text{ there is a } y \text{ with } R(x,y)\in\A \text{ and } C(y)\not\in\A\\

1236: %                   & \text{\bf then} & \A':=\A\cup\set{ C(y) } \\

1237: \geq\text{-rule: } & \text{\bf if}\quad 1. & (\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A \text{ and} \\

1238: %                   &        \;\;\;\quad 2. & \sharp (R_1\comp\cdots\comp R_m)^\A(x)<n \\

1239:                    &        \;\;\;\quad 2. & x \text{ has exactly $p$ $(R_1\comp\cdots\comp R_m)$-successors $y_1,\ldots,y_p$ with }p<n\\

1240:                                     && \text{such that } \set{C(y_i)\mid 1\leq i\leq p}\cup\set{y_i\neq y_j\mid 1\leq i<j\leq p}\subseteq \A\\

1241: %                   &        \;\;\;\quad 2. & \sharp\set{ y\mid y \text{ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ in } \A }<n \\

1242:                    & \text{\bf then} & \A':=\A\cup\set{ R_1(x,z_{i2}),R_2(z_{i2},z_{i3}),\ldots,R_m(z_{im},z_i),C(z_i)\mid 1\leq i\leq n-p }\\

1243:                                  &&\qquad\quad\;\;    \cup\set{ z_i\neq z_j\mid 1\leq i<j\leq n-p}

1244:                                                       \cup\set{ y_i\neq z_j\mid 1\leq i\leq p, 1\leq j\leq n-p}\\

1245: %  &&\qquad \set{ z\neq w\mid w \text{ is an $R_1\comp\cdots\comp R_m$-successor of }x, C(w)\in\A   } \\

1246:                                     && \text{where $z_{ik},z_i$ (for $1\leq i\leq n-p,2\leq k\leq m$) are $m(n-p)$ fresh variables } \\

1247: \leq\text{-rule: } & \text{\bf if}\quad 1. & (\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A \text{ and} \\

1248:                    &        \;\;\;\quad 2. & x \text{ has more than $n$ $(R_1\comp\cdots\comp R_m)$-successors $y_1,\ldots,y_p$ such that}\\

1249:  && \set{ C(y_i)\mid 1\leq i\leq p }\subseteq \A \text{ and } \set{y_i\neq y_j}\cap\A=\emptyset \text{ for some $i,j$ ($1\leq i<j\leq p$), } \\

1250: %                   &        \;\;\;\quad 3. & \text{$x$ has two $(R_1\comp\cdots\comp R_m)$-successors, $y$ and $z$, such that }

1251: %\set{ y\neq z, C(y), C(z) } \subseteq \A  \\

1252: %%%%%\set{ R(x,y),R(x,z) }\subseteq \A \text{ for some }y\neq z\text{ and} \\

1253: %                   &        \;\;\;\quad 4. & \text{for every $(R_1\comp\cdots\comp R_m)$-successor $u$ of $x$, }

1254: %                                             \set{ C(u), \sim C(u) }\cap \A\neq\emptyset \\

1255: %%                   &        \;\;\;\quad 5. & \text{the replacement of $y$ by $z$ is safe in \A} \\

1256:                    & \text{\bf then} & \text{for some pair }y_i,y_j \,(1\leq i<j\leq p) \text{ such that } \set{y_i\neq y_j}\cap\A=\emptyset \\

1257: && \A':=[y_i/y_j]\A \text{ (i.e. $\A'$ is obtained %from \A\

1258: by replacing each occurrence of $y_i$ by $y_j$)}\\

1259: \text{\choos-rule: } & \text{\bf if}\quad 1. & (\atbothq{n}{R_1\comp\cdots\comp R_m}{C})(x) \in\A \text{ and }\\

1260:                    &        \;\;\;\quad 2. &  y \text{ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ such that }%% and }\\

1261:                   \set{ C(y), \sim C(y) }\cap \A=\emptyset \\

1262:                    & \text{\bf then} & \A':=\A\cup\set{ D(y) } \text{ for some } D\in\set{ C,\sim C }\\

1263: \end{eqnarray*}

1264: \hrule

1265: \caption{\label{fig:tabl1}

1266: The Completion Rules for \ALCQX{\comp}}

1267: \vspace*{3mm}\hrule

1268: \end{figure}

1269: 

1270: \begin{lemma}\label{lemmaX}

1271: Let $C_0$ be an  \ALCQX{\comp}-concept in NNF$^{\Join}$, and let \A\ be an ABox obtained by applying

1272: the completion rules to  $\set{C_0(x_0)}$. Then

1273: \begin{enumerate}

1274:   \item For each completion rule $\cal R$ that can be applied to \A\ and for each interpretation $\I$,

1275: the following equivalence holds: $\I$ is a model of \A\ iff $\I$ is a model of the ABox

1276: $\A'$ obtained by applying  $\cal R$.

1277:   \item If \A\ is a complete and clash-free ABox, then \A\ has a model.

1278:   \item If \A\ is complete but contains a clash, then \A\ does not have a model.

1279:   \item The completion algorithm terminates when applied to  $\set{C_0(x_0)}$.

1280: \end{enumerate}

1281: \end{lemma}

1282: As a matter of fact, termination (4) yields that after finitely many steps

1283: we obtain a complete ABox. If $C_0$ is satisfiable,

1284: then  $\set{C_0(x_0)}$ is also satisfiable and, thus, at least one of the

1285: complete ABoxes that the algorithm can generate is satisfiable by (1).

1286: Hence, such an ABox must be clash-free by (3). Conversely, if the application

1287: of the algorithm produces a complete and clash-free ABox \A, then it is

1288: satisfiable by (2) and, owing to (1), this implies that $\set{C_0(x_0)}$ is satisfiable.

1289: Consequently, the algorithm is a decision procedure for satisfiability

1290: of  \ALCQX{\comp}-concepts.

1291: 

1292: \begin{corollary}

1293: Concept satisfiability (and subsumption) for \ALCQX{\comp} is decidable,

1294: and the Tableau algorithm based on the completion rules in Fig.~\ref{fig:tabl1}

1295: is an effective decision procedure. %% for satifiability (and subsumption) of \ALCQX{\comp}-concepts.

1296: \end{corollary}

1297: 

1298: 

1299: \noindent\textbf{Proof of Part 1 of Lemma \ref{lemmaX}}

1300: We consider only the rules concerned with number restrictions

1301: and the \choos-rule, as the proof for the first two rules

1302: is the same as for \ALC.

1303: \begin{description}

1304: \item[3. $\geq$-rule.] Assume that the rule is applied to the constraint

1305: $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$ and that its application yields:

1306: \begin{eqnarray*}

1307:  \A'& = & \A\cup\set{ R_1(x,z_{i2}),R_2(z_{i2},z_{i3}),\ldots,R_m(z_{im},z_i),C(z_i)\mid 1\leq i\leq n-p }\\

1308:                                  &&\qquad \cup\set{ z_i\neq z_j\mid 1\leq i<j\leq n-p}

1309:                                           \cup\set{ y_i\neq z_j\mid 1\leq i\leq p, 1\leq j\leq n-p}

1310: \end{eqnarray*}

1311: Since \A\ is a subset of $\A'$, any model of  $\A'$ is also a model of \A.

1312: Conversely, assume that $\I$ is a model of \A. On the one hand, since $\I$ satisfies

1313: $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$, $x^\I$ has at least $n$

1314: $(R_1\comp\cdots\comp R_m)$-successors in $\I$ which are instances of $C$.

1315: On the other hand, since the  $\geq$-rule

1316: is applicable to $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$, $x$ has exactly

1317: $p$ $(R_1\comp\cdots\comp R_m)$-successors $y_1,\ldots,y_p$, with $p<n$, which are instances of $C$ in $\A$.

1318: Thus, there exists $n-p$ $(R_1\comp\cdots\comp R_m)$-successors

1319: $b_1,\ldots,b_{n-p}$ of $x^\I$ in $\I$

1320: such that $b_i\in C^\I$ and $b_i\neq y_j$ for all $i,j$ ($1\leq i\leq n-p,1\leq j\leq p$).

1321: For all $i$ ($1\leq i\leq n-p$), let $\set{b_{i2},\ldots, b_{im}}\subseteq\dom$

1322: be such $(x^\I,b_{i2})\in R_1^\I$, $(b_{i2},b_{i3})\in R_2^\I,\ldots,$

1323: $(b_{im},b_i)\in R_m^\I$. We define the interpretation of the new variables

1324: added by the $\geq$-rule as

1325: $z_{i2}^\I=b_{i2},\ldots,z_{im}^\I=b_{im}$, and $z_i^\I=b_i$ ($1\leq i\leq n-p$).

1326: Obviously, $\I$ satisfies $\A'$.

1327: \item [4. $\leq$-rule.] Assume that the rule is applied to the constraint

1328: $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in \A$ and let $\I$ be a model of \A.

1329: On the one hand, since the rule is applicable, $x$ has more than

1330: $n$ $(R_1\comp\cdots\comp R_m)$-successors which are instances of $C$ in $\A$.

1331: On the other hand, $\I$ satisfies $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)$

1332: and, thus, there are two different $(R_1\comp\cdots\comp R_m)$-successors

1333: $y_i, y_j$ of $x$ and instances of $C$ in \A\ such that $y_i^\I=y_j^\I$.

1334: Obviously, this implies that $\set{y_i\neq y_j}\cap \A=\emptyset$ and, thus,

1335: $\A'=\A[y_i/y_j]$ is the ABox obtained by applying the $\leq$-rule

1336: to $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)$. In addition, since

1337: $y_i^\I=y_j^\I$, $\I$ satisfies $\A'$.

1338: Conversely, assume that $\A'=\A[y_i/y_j]$ is obtained from $\A$ by applying the

1339: $\leq$-rule, and let $\I$ be a model of $\A'$. If we consider an interpretation $\I$

1340: so that

1341: %$y^\I$ is the same for all the variables $y$ with same name in \A\ and $\A'$ and we have

1342: $y_j^\I=y_i^\I$ for the additional variable $y_j$ that is present in \A\,

1343: then obviously $\I$ satisfies $\A$.

1344: \item [5. \choos-rule.] Assume that the rule is applied to the constraint

1345: $(\atbothq{n}{R_1\comp\cdots\comp R_m}{C})(x)$ and that

1346: %Further assume that, w.l.o.g.,

1347: its application yields:

1348: \begin{eqnarray*}

1349:  \A'& = & \A\cup\set{ D(y) }

1350: \end{eqnarray*}

1351: where $D(y)\not\in\A$.

1352: Since \A\ is a subset of $\A'$, any model of  $\A'$ is also a model of \A.

1353: Conversely, assume that $\I$ is a model of \A. As far as

1354: %the $(R_1\comp\cdots R_m)$-successor of $x$ in \A\

1355: $y$ is concerned,

1356: either $y^\I\in C^\I$ or  $y^\I\in \dom\setminus C^\I=(\sim C)^\I$.

1357: If $y^\I\in C^\I$, for the ABox $\A'$ built with the choice $D=C$

1358: we have that $\I$ satisfies $\A'$. Else, if  $y^\I\in(\sim C)^\I$,

1359: $\I$ satisfies $\A'$ for the choice $D=\sim C$. In any case, $\I$

1360: is a model of the ABox $\A'$ obtained by applying the \choos-rule to \A.

1361: \end{description}

1362: \QED

1363: 

1364: \noindent\textbf{Proof of Part 2  of Lemma \ref{lemmaX}}

1365: Let \A\ be a complete and clash-free ABox that is obtained by applying the completion rules to  $\set{C_0(x_0)}$.

1366: We define the \emph{canonical interpretation} $\I_\A$ of \A\ as follows:

1367: \begin{enumerate}

1368:   \item The domain $\Delta^{\I_\A}$ of $\I_\A$ consists of all the individual names $x\in\NI$ occurring in \A.

1369:   \item For all concept names $C\in\NC$ we define $C^{\I_\A} := \set{ x\mid C(x)\in\A }$.

1370:   \item For all role names $R\in\NR$ we define $R^{\I_\A} := \set{ (x,y)\mid R(x,y)\in\A }$.

1371:   \item For all individual names $x^{\I_\A}:=x$ (i.e. the variable assignment $\pi$ is the identity on \NI).

1372: \end{enumerate}

1373: We show that $\I_\A$ satisfies every constraint in \A.

1374: 

1375: By definition, $\I_\A$ satisfies all the role assertions of the form $R(x,y)$,

1376: %%%of the form $(x^{\I_\A}, y^{\I_\A})\in R^{\I_\A}$ in $\I_\A$,

1377: iff $R(x,y)\in\A$.

1378: More generally, $y$ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ in \A\ iff

1379: $y$ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ in $\I_\A$.

1380: Furthermore, $y\neq z$ implies $y^{\I_\A}\neq z^{\I_\A}$ by construction of $\I_\A$.

1381: By induction on the structure

1382: of concept descriptions, it can be easily shown that $\I_\A$ satisfies the concept assertions as well,

1383: provided that \A\ is complete and clash-free. Again, we restrict our attention to number restrictions

1384: and the \choos-rule,

1385: since the induction base and the treatment of other constructors is the same as for \ALC.

1386: \begin{itemize}

1387:   \item First, consider any assertion $(\atbothq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$

1388: and all $y$'s which are

1389: $(R_1\comp\cdots\comp R_m)$-successors of $x$ in \A.

1390: Then, for each of them, either $C(y)\in\A$ or $\sim C(y)\in\A$,

1391: otherwise the  \choos-rule could be applied.

1392: Moreover, it can be easily proved (by induction on the structure of $C$) that

1393: $\set{C(y),\sim C(y)}\subseteq\A$ would lead to a clash.

1394: %since \A\ is clash-free.

1395: %In any case, the number of $y$s for which $C(y)$ holds and the number

1396: %of $y$s for which $\sim C(y)$ holds are such that we have $x\in(\atbothq{n}{R_1\comp\cdots\comp R_m}{C})^{\I_\A}$:

1397: %otherwise, if $\Join=\geq$ the $\geq$-rule could be applied, else if $\Join=\leq$ the $\leq$-rule could be applied

1398: %or we would have a clash.

1399:   \item Consider $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$. Since \A\ is complete,

1400: the $\geq$-rule cannot be applied to $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$ and, thus,

1401: $x$ has at least $n$ $(R_1\comp\cdots\comp R_m)$-successors which are instances of $C$ in \A,

1402: which are also $(R_1\comp\cdots\comp R_m)$-successors of $x$ and instances of $C$ in $\I_\A$

1403: (by induction, $y\in C^{\I_\A}$ for each $y$ with $C(y)\in\A$).

1404: Hence, $x\in (\atleastq{n}{R_1\comp\cdots\comp R_m}{C})^{\I_\A}$

1405:   \item Constraints with the form $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$ are

1406: satisfied since \A\ is clash-free and complete. In fact, assume that $x$ has more than $n$

1407: $(R_1\comp\cdots\comp R_m)$-successors which are instances of $C$ in $\I_\A$. Then

1408: $x$ has more than $n$

1409: $(R_1\comp\cdots\comp R_m)$-successors which are instances of $C$ also in \A.

1410: If $\A$ contained

1411: inequality constraints $y_i\neq y_j$ for all these successors, then we would have a clash.

1412: Otherwise, the $\leq$-rule could be applied.

1413: \end{itemize}

1414: \QED

1415: 

1416: \noindent\textbf{Proof of Part 3 of Lemma \ref{lemmaX}}

1417: Assume that $\A$ contains a clash. If $\set{A(x),(\Not A)(x)}\subseteq \A$, then clearly no

1418: interpretation can satisfy both constraints. Thus assume that $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$ and

1419: $x$ has $p>n$ $(R_1\comp\cdots\comp R_m)$-successors $y_1,\ldots,y_p$ with

1420: $\set{C(y_i)\mid 1\leq i\leq p}\cup\set{y_i\neq y_j\mid 1\leq i<j\leq p}\subseteq \A$. Obviously,

1421: this implies that, in any model $\I$ of \A, $\Int{x}$ has $p>n$ $(R_1\comp\cdots\comp R_m)$-successors

1422: which are instances of $C$ in $\I$, which shows that $\I$ cannot satisfy

1423: $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)$. \QED

1424: 

1425: \vskip 5mm

1426: \noindent\textbf{Proof of Part 4 of Lemma \ref{lemmaX}}

1427: We must show that the Tableau algorithm that tests satisfiability of \ALCNX{\comp}-concepts

1428: always terminates. In the following, we consider only ABoxes \A\ that are obtained by applying

1429: the completion rules to $\set{C_0(x_0)}$. For a concept $C$, we define its and/or-size $|C|_{\And,\Or}$

1430: as the number of $\And$ and $\Or$ constructors in $C$. The maximal role depth $\depth(C)$ of $C$ is

1431: defined as follows:

1432: \begin{eqnarray*}

1433:   \depth(A) = \depth(\Not A) & := & 0\quad \text{ for }A\in \NC \\

1434:   \depth(C_1\And C_2) = %& := & \max\set{ \depth(C_1), \depth(C_2) } \\

1435:   \depth(C_1\Or C_2) & := & \max\set{ \depth(C_1), \depth(C_2) } \\

1436:   \depth(\atbothq{n}{R_1\comp\cdots\comp R_m}{C}) & = & m + \depth(C)

1437: \end{eqnarray*}

1438: Let $C_0$ be an \ALCNX{\comp}-concept in NNF$^{\Join}$, and let \A\ an ABox obtained

1439: by applying the completion rules to  $\set{C_0(x_0)}$. As an easy consequence

1440: of the definition of the completion rules, we can observe the following facts:

1441: \begin{enumerate}

1442: \item Every variable $x\neq x_0$ that occurs in \A\ is an $(R_1\comp\cdots\comp R_m)$-successor

1443: of $x_0$ for some role chain of length $m\geq 1$. In addition, every other role chain that

1444: connects $x_0$ with $x$ has the same length.

1445: \item If $x$ can be reached in \A\ by a role chain of length $m$ from $x_0$, then for each

1446: constraint $C(x)\in\A$, the maximal role depth of $C$ is bounded by the maximal role depth

1447: of $C_0$ minus $m$ (i.e. $\depth(C)\leq\depth(C_0)-m$). Consequently, $m\leq\depth(C_0)$.

1448: \end{enumerate}

1449: Let $m_0$ be the maximal role depth of $C_0$. Because of the first fact, every individual $x$ in a

1450: ABox \A\ (reached from $\set{C_0(x_0)}$ by applying completion rules) has a unique role level

1451: $\level(x)$, which is its distance from the root node $x_0$, i.e. the unique length of the

1452: role chains that connect  $x_0$ with  $x$. Owing to the second fact, the level of each individual

1453: is an integer between 0 and  $m_0$.

1454: 

1455: In the following, we define a mapping $K$ of ABoxes \A\ to a $3(m_0+1)$-tuple of non-negative

1456: integers such that $\A\rightarrow\A'$ implies $K(\A)\succ K(\A')$, where $\succ$ denotes

1457: the lexicographic ordering on tuples. Since the lexicographic ordering is well-founded,

1458: this implies termination of the algorithm. In fact, if the algorithm did not terminate, then there would

1459: exist an infinite sequence $\A_0\rightarrow\A_1\rightarrow\cdots$, and this would yield an infinite

1460: descending $\succ$-chain of tuples.

1461: 

1462: Hence, let \A\ be an ABox that can be reached from $\set{C_0(x_0)}$ by applying completion rules.

1463: We define:

1464: \begin{displaymath}

1465:   K(\A) := (\overline\kappa_0,\overline\kappa_1,\ldots,\overline\kappa_{m_0-1},\overline\kappa_{m_0}),

1466: \end{displaymath}

1467: where (sub)tuple $\overline\kappa_\ell=(\kappa_\ell^1,\kappa_\ell^2,\kappa_\ell^3)$ and the components

1468: $\kappa_\ell^i$ are obtained as follows:

1469: \begin{itemize}

1470:   \item $\kappa_\ell^1$ is the number of individual variables $x$ in \A\ with $\level(x)=\ell$.

1471:   \item $\kappa_\ell^2$ is the sum of the and/or sizes $|C|_{\And,\Or}$ of all constraints

1472: $C(x)\in\A$ such that $\level(x)=\ell$ and the $\And$- or $\Or$-rule is applicable to $C(x)$ .

1473:   \item For a constraint $\alpha(x)=(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)\in\A$, let $s$ be

1474: the cardinality of \emph{maximal sets} $\set{y_1,\ldots,y_s }$, such that

1475: $y_i$ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ ($1\leq i\leq s$),

1476: %$C(y_i)\in\A\, (1\leq i\leq s)$ and $y_i\neq y_j\in\A\, (1\leq i<j\leq s)$.

1477: $\set{C(y_i)|1\leq i\leq s}\subseteq\A$ and $\set{y_i\neq y_j|1\leq i<j\leq s}\subseteq\A$.

1478: %\begin{align*}

1479: %&  y_i  \text{ is an $(R_1\comp\cdots\comp R_m)$-successor of }x,

1480: %  C(y_i)\in\A\, (1\leq i\leq s) \\

1481: %  & \text{and } y_i\neq y_j\in\A\, (1\leq i<j\leq s)

1482: %\end{align*}

1483: Then we associate with the constraint the number $r(\alpha(x))=\max\set{n-s,0}$, representing the number of individuals

1484: that (possibly) still have to be added to \A\ to make the constraint $\alpha(x)$ satisfied, and define $\kappa_\ell^3$

1485: as follows:

1486: \begin{eqnarray*}

1487: \kappa_\ell^3 &=& \sum_{\alpha(x)\in\A, \level(x)=\ell} r(\alpha(x))

1488: \end{eqnarray*}

1489: \end{itemize}

1490: In the following, we show that $\A\rightarrow\A'$ implies $K(\A)\succ K(\A')$ for each

1491: of the completion rules in Fig.~\ref{fig:tabl1}.

1492: \begin{description}

1493:   \item[1. $\And$-rule.] Assume the rule is applied to the constraint $(C_1\And C_2)(x)$,

1494: let $\A'$ be the ABox obtained by its application and let $\ell=\level(x)$.

1495: First we compare $\overline\kappa_\ell$ and $\overline\kappa_\ell'$, i.e. the tuples associated

1496: with level $\ell$ in \A\ and $\A'$, respectively. The first components $\kappa_\ell^1$

1497: and $\kappa_\ell^{1\prime}$ agree since the number of individuals and their levels have not been changed.

1498: For the second component, we have a decrease (i.e. $\kappa_\ell^{2\prime} < \kappa_\ell^2$), since

1499: $|C_1\And C_2|_{\And,\Or}$ is removed from the sum, and replaced by a number that is no larger than

1500: $|C_1|_{\And,\Or}+|C_2|_{\And,\Or}$ (depending on whether the top constructor of $C_1$ and $C_2$

1501: is $\Or$ or $\And$, or another constructor). Since tuples are compared with lexicographic ordering,

1502: a decrease in the second component makes sure that what happens in the third component is irrelevant.

1503: For the same reason, we need not consider tuples $\kappa_q$ for $q>\ell$.

1504: Tuples at levels $q<\ell$ are either unchanged or have their third component decreased

1505: by the application of the rule, since the addition of the new constraints may add

1506: $x$ to one of the maximal sets involved in the $\kappa_q^3$ definition

1507: (e.g. if $(\atleastq{1}{R}{C_1})(x')$ with $R(x',x)\in\A$ but $C_1(x)\not\in\A$,

1508: we might have a decrement in $\kappa_{\ell-1}^3$ when $C_1(x)$ is added to $\A'$).

1509: %%% there is no change due to the application of the rule. (???)

1510:   \item[2. $\Or$-rule.] This rule can be treated like the $\And$-rule.

1511:   \item[3. $\geq$-rule.] Assume the rule is applied to the constraint

1512: $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$,

1513: let $\A'$ be the ABox obtained by its application and let $\ell=\level(x)$.

1514: The first two components of $\overline\kappa_\ell$ remains unchanged.

1515: The third component decreases (i.e. $\kappa_\ell^{3\prime} < \kappa_\ell^3$),

1516: since the new individuals $z_1,\ldots,z_{n-q}$ can now be added to the maximal sets

1517: of explicitly distinct individuals which are instances of $C$ and $(R_1\comp\cdots\comp R_m)$-successors of $x$

1518: used in the computation of $s$.

1519: For this reason, the increase in the first component of tuples of levels larger than $\ell$ is irrelevant

1520: ($z_{i2}$'s are added at level $\ell+1$, %% $z_{i3}$'s at level $\ell+2$,

1521: \ldots, $z_{im}$'s at level $\ell+m-1$, and $z_i$'s are added at level $\ell+m$).

1522: Tuples at levels smaller than $\ell$ are either unchanged or have their third component

1523: decreased by the application of the rule.

1524:   \item[4. $\leq$-rule.] Assume the rule is applied to the constraint

1525: $(\atmostq{n}{R_1\comp\cdots\comp R_m}{C})(x)$,

1526: let $\A'$ be the ABox obtained by its application and let $\ell=\level(x)$.

1527: On level $\ell+m$, the first component $\kappa^1_\ell$ decreases, since variable $y_i$ is removed.

1528: Thus, possible increases in other components of $\overline\kappa_\ell$ are irrelevant.

1529: Tuples associated with smaller levels $q<\ell$ remain unchanged or decrease. In fact, the

1530: third component of tuples of smaller level cannot increase since for the individuals $y_i$ and $y_j$

1531: that have been identified there was no inequality $y_i\neq y_j\in\A$. Moreover,

1532: since no constraints are removed and, in particular, $y_j$ in $\A'$

1533: has all its old constraints plus the constraints of $y_i$ in \A,

1534: $y_i$ may contribute to one of the maximal sets involved in the $\kappa_q^3$ definition

1535: %some other constraints may become satisfied

1536: (e.g. if %a previously unsatisfied constraint

1537: $\set{(\atleastq{1}{R}{C})(x'),R(x',y_i),C(y_j)}\subseteq\A$

1538: we might have a decrement in $\kappa_{\ell-1}^3$).

1539: %; hence, as a consequence, $\kappa_\ell^3$ decreases).

1540:   \item[5. \choos-rule.] Assume the rule is applied to the constraint

1541: $(\atbothq{n}{R_1\comp\cdots\comp R_m}{C})(x)$,

1542: let $\A'$ be the ABox obtained by its application and let $\ell=\level(x)$.

1543: Obviously, the first two components remain unchanged at every level.

1544: Tuples at levels $q$ smaller than $\ell+m$ have their third component unchanged

1545: or decreased, since the addition of the constraint $D(y)$ (with $\level(y)=\ell+m$)

1546: may add some new individual %(whose $y$ is a successor)

1547: to some of the maximal sets involved in the $\kappa_q^3$ definition.

1548: \end{description}

1549: \QED

1550: 

1551: \subsection*{Complexity issues}

1552: The tableau-based satisfiability algorithm proposed above for \ALCQX{\comp}

1553: may require exponential time and space.

1554: The optimization strategies profitably employed for \ALCN and \ALCQ \cite{Tobi01,BS01}

1555: do not seem to be applicable to \ALCNX{\comp} and \ALCQX{\comp}.

1556: As a matter of fact, such strategies rely on the fact that the

1557: underlying Logics have the \emph{tree model} property, and,

1558: for the sake of satisfiability testing, the individuality

1559: of different role-successors of a given domain object is not relevant.

1560: Only the number of such successors counts (for $\geq$- and $\leq$-rule

1561: applicability and clash testing) and, thus, a single successor

1562: at a time can be used as ``representative'' also for its siblings,

1563: when continuing the algorithm for its further role-successors.

1564: In such a way, only one branch of the tree model at a time can be generated

1565: and investigated by the algorithm, giving rise to a non-deterministic

1566: procedure consuming only polynomial space and, thus, to \PSPACE complexity

1567: (since \NPSPACE=\PSPACE, owing to Savitch's Theorem \cite{Savi70}).

1568: In our case, such an optimization does not seem to be possible, since \ALCNX{\comp}

1569: and \ALCQX{\comp} do not have the tree model property, as number restrictions

1570: $\atleast{p}{R_1\comp\cdots\comp R_{m-1}}\And\atmost{q}{R_1\comp\cdots\comp R_{m-1}\comp R_m}$

1571: (with $p>q$) make some separate $(R_1\comp\cdots\comp R_{m-1})$ role chains merge

1572: into confluent $(R_1\comp\cdots\comp R_{m-1}\comp R_m)$ chains to respect both kinds of number restrictions.

1573: In fact, the identifications of successors effected by the

1574: $\leq$-rule (say at level $\ell$) may involve individuals generated by previous

1575: executions of the $\geq$-rule for different  $\atleastq{n}{R_1\comp\cdots\comp R_m}{C}(x)$

1576: constraints, with possibly different values of $\level(x)$

1577: and role chain lengths (with the proviso that $\level(x)+1\leq\ell\leq\level(x)+m$).

1578: The enforcement of mutual constraints between possibly ``intersecting''

1579: role chains strictly relies on the \emph{individuation} of single successors,

1580: and cannot be surrogated, in general, via representatives.

1581: As a result, the algorithm in Fig.~\ref{fig:tabl1} is a non-deterministic procedure

1582: possibly producing complete ABoxes of \emph{exponential size} in the length of the

1583: input concept description (even if binary coding of numbers is assumed).

1584: %Moreover, if binary coding is assumed, the application of a single

1585: %$\geq$-rule already produces a number $n$ of successors which comes out exponential

1586: %in the length of the encoding of $n$ (whereas the use of single representatives

1587: %for \ALCN and \ALCQ also avoids this exponential explosion).

1588: \begin{lemma}\label{lemmaK}

1589: Given a complete ABox $\A$ generated by the algorithm in Fig.~\ref{fig:tabl1},

1590: the size of $\A$ is exponential in the input size $s$, thanks to the

1591: following facts:

1592: \begin{enumerate}

1593: \item The number $a$ of individuals in $\A$ is $O(2^{p(s)})$, where $p$ is a polynomial

1594: function.

1595: \item The number of constraints in $\A$ is a polynomial function of $a$.

1596: \end{enumerate}

1597: %Therefore, the size of $\A$ is exponential in $s$.

1598: \end{lemma}

1599: Let us define the \emph{size} $c_0$ of the concept description $C_0$ as the total

1600: number of symbols (operators, concept and role names) it contains, and let

1601: $N:=\max\set{n| (\atleastq{n}{R_1\comp\cdots\comp R_m}{C}) \text{ is a subconcept of }C_0}$.

1602: Moreover, the number of subconcepts of $C_0$ is obviously bounded by $c_0$.

1603: 

1604: \vskip 5mm

1605: \noindent\textbf{Proof of Fact 1}

1606: According to Fig.~\ref{fig:tabl1}, new individuals (apart from $x_0$) are added to $\A$

1607: by the application of the $\geq$-rule only.

1608: The algorithm execution generates a connected structure with the shape of a tree, rooted on $x_0$,

1609: where some node coincide (owing to $\leq$-rule applications).

1610: Each path in this tree-structure has a maximal length which is bounded

1611: by the maximal role depth $m_0$ of $C_0$. The out-degree is bounded by the maximal

1612: number of new successors that can be generated from an individual $x$.

1613: This number cannot exceed $c_0 N m_0$, since the number of

1614: of times the $\geq$-rule can be applied to a constraint on $x$ is limited by

1615: the total number of $\exists^{\geq n}$ constructors in $C_0$ and, thus, by $c_0$

1616: and, for each application of the $\geq$-rule, no more than $N m_0$

1617: new individuals can be added. Hence, the total size of the tree-structure

1618: is bounded by $(c_0  N  m_0)^{m_0}$ $= 2^{m_0(\log c_0+\log N+\log m_0)}$

1619: $\leq 2^{2 c_0^2+c_0\log N}$, since $m_0\leq c_0$. Obviously,

1620: the exponent is a polynomial function of the input size, even if binary

1621: coding of numbers is adopted.

1622: \QED

1623: 

1624: \vskip 5mm

1625: \noindent\textbf{Proof of Fact 2}

1626: For each individual $x$, $\A$ may at most contain a pair of constraints

1627: $\set{C(x),\sim C(x)}$ for each subconcept $C$ of $C_0$. Hence, the total

1628: number of constraints with the form $D(x)$ in $\A$ is bounded by $2 c_0$.

1629: Moreover, for each pair of individuals $x$ and $y$,

1630: the number of constraints with the form $R(x,y)$ (or $x\neq y$) in $\A$

1631: is limited by the number of role names in $C_0$, which is strictly less than $c_0$,

1632: plus one (for inequality constraints).

1633: Hence, the size of $\A$ is surely bounded by $2 c_0 a + c_0 a^2$

1634: (we could derive a tighter bound if we took into account the role levels of individuals).

1635: \QED

1636: 

1637: %This fact can be shown by explicitly deriving an exponential upper bound for the

1638: %number $a$ of individuals in $\A$ (i.e. the size of $\Delta^{\I_\A}$).

1639: %In fact, $\A$ contains a number of constraints $C(x)$ which is limited

1640: %by $a$ times the number of concept names in $C_0$, plus a number of constraints

1641: %$R(x,y)$ (or $x\neq y$) which is limited by  $a^2$ times

1642: %the number of role names in $C_0$ plus one (for inequality constraints),

1643: %which is obviously a number polynomial in $a$.

1644: 

1645: %Let us define the \emph{size} $c_0$ of the concept description $C_0$ as the total

1646: %number of symbols (operators, concept and role names) it contains, and let

1647: %$N:=\max\set{n| \atleastq{n}{R_1\comp\cdots\comp R_m}{C} \text{ appears in }C_0}$.

1648: 

1649: %During the execution of the algorithm in Fig.~\ref{tab1}, starting from $\{C_0(x_0)\}$,

1650: %each completion rule can be applied with a recursion depth which is limited by the

1651: %maximal role depth $m_0$  of $C_0$. Moreover, new individuals are generated by the

1652: %application of the $\geq$-rule only. At each step, the number of rules which are

1653: %applicable to a single object in $\A$, including generating ones, is bounded

1654: %by the size $c_0$ of $C_0$ and, thus, a total number $c_0^{m_0}$ of applications

1655: %is at most concerned by the whole algorithm execution. Each of these applications

1656: %may involve the $\geq$-rule for a constraint $(\atleastq{n}{R_1\comp\cdots\comp R_m}{C})(x)$

1657: %and generate a tree-structure, rooted on $x$, where some node coincide (owing to

1658: %$\leq$-rule applications). The maximal size of such tree-structures

1659: %is bounded by $N^{m_0}$, as the out-degree of tree nodes is limited by $N$

1660: %and the tree depth is limited by $m_0$. Summing up, the total number $a$ of individuals

1661: %generated by the algorithm is bounded by $c_0^{m_0}\cdot N^{m_0}$ $= 2^{m_0(\log c_0+\log N)}$

1662: %$\leq 2^{c_0^2+c_0\log N}$. If $n$ is the satisfiability problem input size,

1663: %we have $c_0\leq n$ and $\log N\leq n$ (also if binary encoding of numbers is assumed).

1664: %Hence $a\leq 2^{2n^2}$ and, thus, the size of $a$ is exponential in $n$.

1665: \vskip 5mm

1666: As it can be easily seen, the two facts together give a space consumption

1667: bounded by $2^{6s^2+s}$.

1668: 

1669: \begin{corollary}

1670: By the given algorithm, deciding satisfiability (subsumption) of \ALCQX{\comp} concepts

1671: is in the \NEXPTIME (\emph{co-}\NEXPTIME) complexity class.

1672: \end{corollary}

1673: 

1674: \subsection{An extension of the decidability result}

1675: We provide in this Section an extension of the algorithm given in Fig.~\ref{fig:tabl1}

1676: for \ALCQX{\comp}-concept satisfiability,

1677: such that it can also deal with union and/or intersection of role chains \emph{of the same length}.

1678: The extension follows the same directions of the similar extension proposed

1679: for \ALCNX{\comp} in \cite{BS99}. Analogously, also the soundness, completeness and

1680: termination proofs of our extended algorithm are very similar to the ones proposed

1681: for the basic algorithm in the previous Section and, thus, they will only be sketched.

1682: 

1683: The general form of a role expression $\cal R$ we consider here is the following:

1684: \begin{eqnarray*}

1685:   {\cal R} &=&

1686: %\overset{M}{\bigOr{i=1}} {\cal R}_i

1687: %       \quad=\quad \overset{M}{\bigOr{i=1}} \overset{N_i}{\bigAnd{j=1}} {\cal R}_{ij} \\

1688: %           &=&

1689: \overset{M}{\bigOr{i=1}} \overset{N_i}{\bigAnd{j=1}} (R^{ij}_1\comp R^{ij}_2\comp\cdots R^{ij}_m)

1690: \end{eqnarray*}

1691: %% with an obvious definition of ${\cal R}_i$ and  ${\cal R}_{ij}$ symbols,

1692: that is we assume, for the sake of simplicity, Boolean role chain combinations

1693: to be in Disjunctive Normal Form\footnote{

1694: General $\And/\Or$ combinations of role chains can be put in DNF (which may require an exponential time)

1695: by rewriting concept $C_0$ before the execution of the satisfiability algorithm.} (DNF).

1696: In the presence of role expressions of this kind, we modify the definition

1697: of role successor for a complex role chain $\cal R$ as follows.

1698: 

1699: \begin{figure}

1700: \hrule

1701: \begin{eqnarray*}

1702: \geq'\text{-rule: } & \text{\bf if}\quad 1. & (\atleastq{n}{{\cal R}}{C})(x)\in\A \text{ and} \\

1703: %                   &        \;\;\;\quad 2. & \sharp (R_1\comp\cdots\comp R_m)^\A(x)<n \\

1704:                    &        \;\;\;\quad 2. & x \text{ has exactly $p$ $\cal R$-successors $y_1,\ldots,y_p$ with }p<n\\

1705:                                     && \text{such that } \set{C(y_i)\mid 1\leq i\leq p}\cup\set{y_i\neq y_j\mid 1\leq i<j\leq p}\subseteq \A\\

1706: %                   &        \;\;\;\quad 2. & \sharp\set{ y\mid y \text{ is an $(R_1\comp\cdots\comp R_m)$-successor of $x$ in } \A }<n \\

1707:                    & \text{\bf then} & \A':=\A\cup\set{ R^{\hat\imath_i j}_1(x,z^j_{i2}),R^{\hat\imath_i j}_2(z^j_{i2},z^j_{i3}),\ldots,R^{\hat\imath_i j}_m(z^j_{im},z^j_i),C(z_i) \\

1708: &&\qquad\qquad\qquad\; \mid 1\leq i\leq n-p, 1\leq j\leq N_{\hat\imath_i} }\\

1709:                                  &&\qquad\quad\;\;    \cup\set{ z^\ell_i\neq z^\ell_j\mid 1\leq i<j\leq n-p, 1\leq\ell\leq N_{\hat\imath_i}} \\

1710:                                  &&\qquad\quad\;\;    \cup\set{ y_i\neq z^\ell_j\mid 1\leq i\leq p, 1\leq j\leq n-p, 1\leq\ell\leq N_{\hat\imath_i}}\\

1711: %  &&\qquad \set{ z\neq w\mid w \text{ is an $R_1\comp\cdots\comp R_m$-successor of }x, C(w)\in\A   } \\

1712:                                  && \text{for some $\set{\hat\imath_1,\hat\imath_2,\ldots,\hat\imath_{n-p}} \subseteq\set{1,\ldots, M}$,}\\

1713:                                  &&\text{where $z^j_{ik},z^j_i$ (for $1\leq i\leq n-p,2\leq k\leq m,1\leq j\leq N_{\hat\imath_i}$)}\\

1714:                                  &&\text{are $\textstyle m\sum_{i=1}^{n-p}N_{\hat\imath_i}$ fresh variables } \\

1715: \leq'\text{-rule: } & \text{\bf if}\quad 1. & (\atmostq{n}{{\cal R}}{C})(x)\in\A \text{ and} \\

1716:                    &        \;\;\;\quad 2. & x \text{ has more than $n$ $\cal R$-successors $y_1,\ldots,y_p$ such that}\\

1717:  && \set{ C(y_i)\mid 1\leq i\leq p }\subseteq \A \text{ and } \set{y_i\neq y_j}\cap\A=\emptyset \text{ for some $i,j$ ($1\leq i<j\leq p$), } \\

1718: %                   &        \;\;\;\quad 3. & \text{$x$ has two $(R_1\comp\cdots\comp R_m)$-successors, $y$ and $z$, such that }

1719: %\set{ y\neq z, C(y), C(z) } \subseteq \A  \\

1720: %%%%%\set{ R(x,y),R(x,z) }\subseteq \A \text{ for some }y\neq z\text{ and} \\

1721: %                   &        \;\;\;\quad 4. & \text{for every $(R_1\comp\cdots\comp R_m)$-successor $u$ of $x$, }

1722: %                                             \set{ C(u), \sim C(u) }\cap \A\neq\emptyset \\

1723: %%                   &        \;\;\;\quad 5. & \text{the replacement of $y$ by $z$ is safe in \A} \\

1724:                    & \text{\bf then} & \text{for some pair }y_i,y_j \,(1\leq i<j\leq p) \text{ such that } \set{y_i\neq y_j}\cap\A=\emptyset \\

1725: && \A':=[y_i/y_j]\A \\

1726: \text{\choos$'$-rule: } & \text{\bf if}\quad 1. & (\atbothq{n}{{\cal R}}{C})(x) \in\A \text{ and }\\

1727:                    &        \;\;\;\quad 2. &  y \text{ is an $\cal R$-successor of $x$ such that }%% and }\\

1728:                   \set{ C(y), \sim C(y) }\cap \A=\emptyset \\

1729:                    & \text{\bf then} & \A':=\A\cup\set{ D(y) } \text{ for some } D\in\set{ C,\sim C }\\

1730: \end{eqnarray*}

1731: \hrule

1732: \caption{\label{fig:tabl2}

1733: The Completion Rules for \ALCQX{\comp} extended with complex role chains}

1734: \vspace*{3mm}\hrule

1735: \end{figure}

1736: \begin{definition}

1737: The individual $y$ is a $\cal R$-\emph{successor} of $x$ in \A\ (where $\cal R$ is defined as above)

1738: iff for some $\hat\imath$ ($1\leq \hat\imath \leq M$), $\exists y^1_2 y^1_3 \ldots y^1_m y^2_2 y^2_3 \ldots y^2_m$

1739: $y^{N_{\hat\imath}}_2 y^{N_{\hat\imath}}_3 \ldots y^{N_{\hat\imath}}_m$ variables in \A\ such that

1740: $\set{ R^{\hat\imath j}_k(y^j_k,y^j_{k+1}) \mid 2\leq k\leq m-1, 1\leq j\leq N_{\hat\imath} }\cup

1741: \set{ R^{\hat\imath j}_1(x,y^j_2),R^{\hat\imath j}_m(y^j_m,y) \mid 1\leq j\leq N_{\hat\imath} } \subseteq\A$. %% with $y_1=x$ and $y_{m+1}=y$.

1742: \end{definition}

1743: Notice that, owing to this definition, role successors in \A\ are also successors in every model $\I$

1744: of \A: if $\I$ satisfies \A, and $y$ is an $\cal R$-successor of $x$ in \A, then $y^\I$

1745: is an  $\cal R$-successor of $x^\I$ in $\I$.

1746: 

1747: The Tableau algorithm is extended by replacing the completion rules dealing with number restrictions

1748: %% $\atbothq{n}{\cal R}{C}$

1749: and the \choos-rule  with the rules shown in Fig.~\ref{fig:tabl2}, so that the new complex role chains

1750: can be managed.

1751: 

1752: In order to prove that the new algorithm decides concept satisfiability for this \ALCQX{\comp}

1753: extension, we must prove that all four parts of Lemma~\ref{lemmaX} still hold.

1754: \begin{enumerate}

1755: \item \emph{Local correctness} of the $\geq'$-, $\leq'$- and \choos$'$-rules can be shown

1756: as in the proof of Part 1 of the Lemma~\ref{lemmaX}.

1757: \item The \emph{canonical model} induced by a complete and clash-free ABox is defined

1758: as in the proof of Part 2 of the Lemma~\ref{lemmaX}. The proof that this canonical model

1759: satisfies the ABox is also similar to the one provided for Lemma~\ref{lemmaX}.

1760: Note that the definition we used for $\cal R$-successors coincides with the notion

1761: of  $\cal R$-successors in the canonical model $\I_\A$ induced by \A.

1762: \item The proof that an ABox containing a clash is unsatisfiable is the same as the one

1763: given above. This follows from the fact that role successors in an ABox \A\ are also

1764: successors in every model $\I$ of \A.

1765: \item The proof of \emph{termination} is also very similar to the one considered before.

1766: The definition of the depth of a concept is extended in the obvious way to expressions

1767: involving complex roles:

1768: \begin{eqnarray*}

1769:   \depth(\atbothq{n}{{\cal R}}{C}) =

1770:   \depth\bigg(\atbothq{n}{ \big( \overset{M}{\underset{i=1}\Or} \overset{N_i}{\underset{j=1}\And}

1771:   (R^{ij}_1\comp R^{ij}_2\comp\cdots R^{ij}_m)\big) }{C}\bigg) & = & m + \depth(C)

1772: \end{eqnarray*}

1773: Since role chains in complex roles are all of the same length, the two facts stated in the proof

1774: of Part 4 of Lemma~\ref{lemmaX} are still valid and, thus, we can define the same metric $K(\A)$

1775: as before also on all the ABoxes that are produced by the new completion rules. It can be seen

1776: that the proof that $\A\rightarrow\A'$ implies $K(\A)\succ K(\A')$ carries over to the new rules.

1777: Actually, the proof given in Part 4 of Lemma~\ref{lemmaX} only relies on the fact that all role

1778: chains connecting any two individuals have the same length, which is still satisfied in the

1779: extended logics.

1780: \end{enumerate}

1781: An immediate consequence of these observations is the Theorem that follows:

1782: \begin{theorem}

1783: Concept satisfiability (and subsumption) for the logic that extends \ALCQX{\comp}

1784: with union/intersections of role chains of the same length is decidable,

1785: and the Tableau algorithm based on the completion rules in Fig.~\ref{fig:tabl2}

1786: is an effective decision procedure.

1787: \end{theorem}

1788: 

1789: As far as complexity of the algorithm is concerned, Lemma~\ref{lemmaK} holds

1790: also for the algorithm in Fig.~\ref{fig:tabl2}. The only modification required

1791: is to the proof of Fact 2, in the tree-structure out-degree evaluation, since

1792: the application of each $\geq'$-rule may generate at most $N m_0 \hat{N}$

1793: successors, where $\hat N$ is the maximal number of conjuncts occurring

1794: in a role chain combination. Since $\hat N\leq c_0$, the number of individuals

1795: in $\A$ is now bounded by $2^{3 c_0^2+c_0\log N}$.

1796: \begin{corollary}

1797: By the given algorithm, deciding concept satisfiability (subsumption)

1798: for the logic that extends \ALCQX{\comp} with union/intersections of role chains of the same length

1799: is in the \NEXPTIME (\emph{co-}\NEXPTIME) complexity class.

1800: \end{corollary}

1801: 

1802: 

1803: \newcommand{\blu}[1]{\textcolor{blue}{#1}}

1804: \newcommand{\rosso}[1]{\textcolor{red}{#1}}

1805: \newcommand{\giallo}[1]{\textcolor{yellow}{#1}}

1806: \newcommand{\verde}[1]{\textcolor{green}{#1}}

1807: \newcommand{\viola}[1]{\textcolor{magenta}{#1}}

1808: 

1809: \begin{figure}

1810: \setlength{\unitlength}{.3mm}

1811: \centering

1812: \begin{picture}(500,710)(0,-50)

1813: 

1814: \xput{250,660}{\rosso{\ALCQX{\comp,^-,\Or,\And}}}

1815: \xput{250,640}{\rosso{\ALCNNX{\comp,^-,\Or,\And}}}

1816: \xput{250,620}{\rosso{\ALCNX{\comp,^-,\Or,\And}}}

1817: 

1818: %%%%%%%%%%%%%%%%%%%%%%%%%%

1819: 

1820: \drawline(250,610)(100,530)

1821: \drawline(250,610)(200,530)

1822: \drawline(250,610)(300,530)

1823: \drawline(250,610)(400,530)

1824: 

1825: %%%%%%%%%%%%%%%%%%%%%%%%%%

1826: 

1827: 

1828: \xput{100,520}{\blu{\ALCQX{^-,\Or,\And}}}

1829: \xput{100,500}{\blu{\ALCNNX{^-,\Or,\And}}}

1830: \xput{100,480}{\blu{\ALCNX{^-,\Or,\And}}}

1831: 

1832: \xput{200,520}{\rosso{\ALCQX{\comp,^-,\Or}}}

1833: \xput{200,500}{\rosso{\ALCNNX{\comp,^-,\Or}}}

1834: \xput{200,480}{\rosso{\ALCNX{\comp,^-,\Or}}}

1835: 

1836: \xput{300,520}{\rosso{\ALCQX{\comp,\Or,\And}}}

1837: \xput{300,500}{\rosso{\ALCNNX{\comp,\Or,\And}}}

1838: \xput{300,480}{\rosso{\ALCNX{\comp,\Or,\And}}}

1839: 

1840: \xput{400,520}{\rosso{\ALCQX{\comp,^-,\And}}}

1841: \xput{400,500}{\rosso{\ALCNNX{\comp,^-,\And}}}

1842: \xput{400,480}{\rosso{\ALCNX{\comp,^-,\And}}}

1843: 

1844: %%%%%%%%%%%%%%%%%%%%%%%%%%

1845: 

1846: \drawline(100,470)(0,330)

1847: \drawline(100,470)(100,330)

1848: \drawline(100,470)(200,330)

1849: 

1850: \drawline(200,470)(100,330)

1851: \drawline(200,470)(300,330)

1852: \drawline(200,470)(500,330)

1853: 

1854: \drawline(300,470)(200,330)

1855: \drawline(300,470)(300,330)

1856: \drawline(300,470)(400,330)

1857: 

1858: \drawline(400,470)(100,330)

1859: \drawline(400,470)(400,330)

1860: \drawline(400,470)(500,330)

1861: 

1862: %%%%%%%%%%%%%%%%%%%%%%%%%%

1863: 

1864: \xput{0,320}{\blu{\ALCQX{^-,\And}}}

1865: \xput{0,300}{\blu{\ALCNNX{^-,\And}}}

1866: \xput{0,280}{\blu{\ALCNX{^-,\And}}}

1867: 

1868: \xput{100,320}{\blu{\ALCQX{^-,\Or}}}

1869: \xput{100,300}{\blu{\ALCNNX{^-,\Or}}}

1870: \xput{100,280}{\blu{\ALCNX{^-,\Or}}}

1871: 

1872: \xput{200,320}{\blu{\ALCQX{\Or,\And}}}

1873: \xput{200,300}{\blu{\ALCNNX{\Or,\And}}}

1874: \xput{200,280}{\blu{\ALCNX{\Or,\And}}}

1875: 

1876: \xput{300,320}{\ALCQX{\comp,\Or}}

1877: \xput{300,300}{\blu{\ALCNNX{\comp,\Or}}}

1878: \xput{300,280}{\blu{\ALCNX{\comp,\Or}}}

1879: 

1880: \xput{400,320}{\rosso{\ALCQX{\comp,\And}}}

1881: \xput{400,300}{\rosso{\ALCNNX{\comp,\And}}}

1882: \xput{400,280}{\rosso{\ALCNX{\comp,\And}}}

1883: 

1884: \xput{500,320}{\rosso{\ALCQX{^-,\comp}}}

1885: \xput{500,300}{\rosso{\ALCNNX{^-,\comp}}}

1886: \xput{500,280}{\ALCNX{^-,\comp}}

1887: 

1888: %%%%%%%%%%%%%%%%%%%%%%%%%%

1889: 

1890: \drawline(100,130)(0,270)

1891: \drawline(100,130)(100,270)

1892: \drawline(100,130)(500,270)

1893: 

1894: \drawline(200,130)(100,270)

1895: \drawline(200,130)(200,270)

1896: \drawline(200,130)(300,270)

1897: 

1898: \drawline(300,130)(0,270)

1899: \drawline(300,130)(200,270)

1900: \drawline(300,130)(400,270)

1901: 

1902: \drawline(400,130)(300,270)

1903: \drawline(400,130)(400,270)

1904: \drawline(400,130)(500,270)

1905: 

1906: %%%%%%%%%%%%%%%%%%%%%%%%%%

1907: 

1908: \xput{100,120}{\blu{\ALCQX{^-}}}

1909: \xput{100,100}{\blu{\ALCNNX{^-}}}

1910: \xput{100,80}{\blu{\ALCNX{^-}}}

1911: 

1912: \xput{200,120}{\blu{\ALCQX{\Or}}}

1913: \xput{200,100}{\blu{\ALCNNX{\Or}}}

1914: \xput{200,80}{\blu{\ALCNX{\Or}}}

1915: 

1916: \xput{300,120}{\blu{\ALCQX{\And}}}

1917: \xput{300,100}{\blu{\ALCNNX{\And}}}

1918: \xput{300,80}{\blu{\ALCNX{\And}}}

1919: 

1920: \xput{400,120}{\blu{\ALCQX{\comp}}}

1921: \xput{400,100}{\blu{\ALCNNX{\comp}}}

1922: \xput{400,80}{\blu{\ALCNX{\comp}}}

1923: 

1924: %%%%%%%%%%%%%%%%%%%%%%%%%%

1925: 

1926: \drawline(250,-10)(100,70)

1927: \drawline(250,-10)(200,70)

1928: \drawline(250,-10)(300,70)

1929: \drawline(250,-10)(400,70)

1930: 

1931: %%%%%%%%%%%%%%%%%%%%%%%%%%

1932: 

1933: \xput{250,-20}{\blu{\ALCQ}}

1934: \xput{250,-40}{\blu{\ALCN}}

1935: 

1936: %%%%%%%%%%%%%%%%%%%%%%%%%%

1937: 

1938: %\xput{20,610}{\rosso{\textsl{UNDECIDABLE}}}

1939: %\xput{20,590}{\blu{\textsl{DECIDABLE}}}

1940: %\dashline{4}(-50,600)(150,600)(150,340)(350,340)(350,140)(450,140)(450,290)

1941: %\dashline{3}(250,340)(250,310)(350,310)

1942: %\dashline{3}(450,260)(550,260)

1943: %\thicklines

1944: %\verde{\drawline(450,290)(550,290)(550,340)(450,340)(450,290)}

1945: %\verde{\drawline(350,90)(450,90)(450,140)(350,140)(350,90)}

1946: 

1947: \xput{20,610}{\rosso{\textsl{UNDECIDABLE}}}

1948: \xput{20,590}{\blu{\textsl{DECIDABLE}}}

1949: \dashline{3}(-50,600)(150,600)(150,460)

1950: (255,310)(350,310)

1951: %%(230,340)%(150,340)

1952: \dashline{3}(235,340)(350,340)(350,260)(550,260)

1953: %\dashline{3}(250,340)(250,310)(350,310)

1954: \dashline{3}(450,260)(450,290)

1955: \Thicklines

1956: \verde{\path(450,290)(550,290)(550,340)(450,340)(450,290)}

1957: \verde{\path(350,90)(450,90)(450,140)(350,140)(350,90)}

1958: 

1959: \end{picture}

1960: \caption{\label{fig:status}

1961: Decidability status of concept satisfiability in \ALCN extensions.

1962: The inclusion edges are meant between corresponding DLs

1963: in the $\cal N/\bar N/Q$ stack.

1964: The green boxes highlight the DLs studied in this paper.}

1965: \end{figure}

1966: 

1967: \section{Conclusions}

1968: 

1969: In this paper we studied expressive Description Logics %extending \ALCNX{\comp},

1970: allowing for number restrictions on complex roles built with

1971: the composition operator ($\comp$), %%and other constructors in $\set{\inv{},\Or,\And}$.

1972: extended with other role constructors in $\set{\inv{},\Or,\And}$ and qualified number restrictions.

1973: 

1974: In this framework, we improved the (un)decidability results

1975: by Baader and Sattler on logics of the \ALCN family \cite{BS99}

1976: by showing that \ALCNNX{\comp,^-} is undecidable via reduction of a domino problem,

1977: whereas the introduction of qualified number restrictions in \ALCQX{\comp}

1978: (and in its extension with $\And/\Or$ combinations of role chains with the same length)

1979: does not hinder decidability of reasoning.

1980: For \ALCQX{\comp}, a tableau-based satisfiability algorithm

1981: with a \NEXPTIME upper bound has been proposed.

1982: 

1983: As we observed in the Introduction that known decidability results

1984: also lift up to \ALCQX{^-,\Or,\And}, we shed some new light on the

1985: whole decidability scenario ranging from \ALCN to

1986: \ALCQX{\comp,^-,\Or,\And}, which is depicted in

1987: Fig.~\ref{fig:status}. In this scenario, since we recently proved

1988: that \ALCNX{\comp,\Or} (for which \ALCNNX{\comp,\Or} is a syntactic variant) is decidable \cite{myDL03},

1989: small gaps left open concern decidability of \ALCQX{\comp,\Or}

1990: and of ``pure'' \ALCNX{\comp,^-}. In particular, around the narrow borders of the second gap,

1991: we proved in this work that the language with inverses in value restrictions and

1992: inverses and composition of roles under unqualified number

1993: restrictions is undecidable, whereas the language with inverses

1994: and role composition under value restrictions and inverses under

1995: qualified number restrictions is decidable, as it is a sublanguage

1996: of the DL $\cal CIQ$ \cite{KR-96}. Another open question is the

1997: exact characterization of \ALCQX{\comp} (and \ALCNX{\comp})

1998: complexity, as the \NEXPTIME bound we derived may be far from

1999: being tight. Future work will also consider such issues.

2000: 

2001: 

2002: 

2003: %\bibliography{dbdl}

2004: %\bibliographystyle{plain}

2005: \begin{thebibliography}{10}

2006: 

2007: \bibitem{AF99}

2008: {A. Artale and E. Franconi}.

2009: \newblock {Temporal ER Modeling with Description Logics}.

2010: \newblock In {\em Proc. Intl' Conf. on Conceptual Modeling (ER'99)}, pages

2011:   81--95, {Paris, France}, November 1999.

2012: 

2013: \bibitem{BJ92}

2014: {A. Borgida and M. Jarke}.

2015: \newblock {Knowledge Representation and Reasoning in Software Engineering}.

2016: \newblock {\em IEEE Transactions on Software Engineering}, 18(6):449--450,

2017:   1992.

2018: 

2019: \bibitem{DLbook}

2020: F.~Baader, D.~McGuinness, D.~Nardi, and P.F. Patel-Schneider, editors.

2021: \newblock {\em The Decsription Logic Handbook: Theory, implementation and

2022:   applications}.

2023: \newblock Cambridge University Press, Cambridge, UK, 2003.

2024: 

2025: \bibitem{BS99}

2026: F.~Baader and U.~Sattler.

2027: \newblock {Expressive Number Restrictions in Description Logics}.

2028: \newblock {\em J. of Logic and Computation}, 9(3):319--350, 1999.

2029: 

2030: \bibitem{BS01}

2031: F.~Baader and U.~Sattler.

2032: \newblock {An Overview of Tableau Algorithms for Description Logics}.

2033: \newblock {\em Studia Logica}, 69:5--40, 2001.

2034: 

2035: \bibitem{domino}

2036: R.~Berger.

2037: \newblock {The Undecidability of the Dominoe Problems}.

2038: \newblock {\em Mem. Amer. Mathematical Society}, 66:1--72, 1966.

2039: 

2040: \bibitem{C2}

2041: A.~Borgida.

2042: \newblock {On the Relative Expressiveness of Description Logics and First Order

2043:   Logics}.

2044: \newblock {\em Artificial Intelligence}, 82:353--367, 1996.

2045: 

2046: \bibitem{GHB96}

2047: {C.A. Goble and C. Haul and S. Bechhofer}.

2048: \newblock {Describing and Classifying Multimedia Using the Description Logic

2049:   GRAIL}.

2050: \newblock In {\em Proc. of Storage and Retrieval for Image and Video Databases

2051:   (SPIE IV)}, pages 132--143, {San Diego/La Jolla, CA}, {January/February}

2052:   1996.

2053: 

2054: \bibitem{dl-expr-reas:book-99}

2055: D.~Calvanese, G.~{De Giacomo}, M.~Lenzerini, and D.~Nardi.

2056: \newblock {Reasoning in Expressive Description Logics}.

2057: \newblock In {\em Handbook of Automated Reasoning}, pages 1581--1634. Elsevier

2058:   Science, {Amsterdam, The Netherlands}, 2001.

2059: 

2060: \bibitem{JLC-DL-99}

2061: D.~Calvanese, G.~De Giacomo, and M.~Lenzerini.

2062: \newblock {Representing and Reasoning on XML Documents: A Description Logic

2063:   Approach}.

2064: \newblock {\em J. of Logic and Computation}, 9(3):295--318, 1999.

2065: 

2066: \bibitem{KR-98}

2067: D.~Calvanese, G.~De Giacomo, M.~Lenzerini, D.~Nardi, and R.~Rosati.

2068: \newblock {Description Logic Framework for Information Integration}.

2069: \newblock In {\em Proc. of Intl' Conf. on the Principles of Knowledge

2070:   Representation and Reasoning (KR'98)}, pages 2--13, {Trento, Italy}, June

2071:   1998.

2072: 

2073: \bibitem{DBIS98}

2074: D.~Calvanese, M.~Lenzerini, and D.~Nardi.

2075: \newblock {Description Logics for Conceptual Data Modeling}.

2076: \newblock In {\em Logics for Databases and Information Systems}, pages

2077:   229--263. Kluwer Academic Publishers, {Boston, MA}, 1998.

2078: 

2079: \bibitem{ALCN1}

2080: F.M. Donini, M.~Lenzerini, D.~Nardi, and W.~Nutt.

2081: \newblock {The Complexity of Concept Languages}.

2082: \newblock {\em Information and Computation}, 134:1--58, 1997.

2083: 

2084: \bibitem{myDL01}

2085: {F. Grandi}.

2086: \newblock {On Expressive Number Restrictions in Description Logics}.

2087: \newblock In {\em Proc. of Intl' Workshop on Description Logics (DL'01)}, pages

2088:   56--65, {Stanford, CA}, August 2001.

2089: 

2090: \bibitem{myDL03}

2091: {F. Grandi}.

2092: \newblock {A Tableau Algorithm for \ALCNX{\comp,\Or}}.

2093: \newblock In {\em Proc. of Intl' Workshop on Description Logics (DL'03)},

2094:   {Rome, Italy}, September 2003.

2095: \newblock \emph{To appear}.

2096: 

2097: \bibitem{franconi-dood00}

2098: E.~Franconi, F.~Grandi, and F.~Mandreoli.

2099: \newblock {A Semantic Approach for Schema Evolution and Versioning in

2100:   Object-Oriented Databases}.

2101: \newblock In {\em Proc. Intl' Conf. on Deductive and Object-Oriented Databases

2102:   (DOOD 2000)}, pages 1048--1062, {London, UK}, 2000.

2103: 

2104: \bibitem{KR-96}

2105: G.~De Giacomo and M.~Lenzerini.

2106: \newblock {TBox and ABox Reasoning in Expressive Description Logics}.

2107: \newblock In {\em Proc. of Intl' Conf. on the Principles of Knowledge

2108:   Representation and Reasoning (KR'96)}, pages 348--353, {Cambridge, MA},

2109:   November 1996.

2110: 

2111: \bibitem{decC2}

2112: E.~{Gr\"{a}del}, M.~Otto, and E.~Rosen.

2113: \newblock {Two-variable Logic with Counting is Decidable}.

2114: \newblock In {\em Proc. Annual IEEE Symp. on Logic in Computer Science

2115:   (LICS'97)}, pages 306--317, {Warsaw, Poland}, 1997.

2116: 

2117: \bibitem{HB91}

2118: B.~Hollunder and F.~Baader.

2119: \newblock {Qualifying Number Restrictions in Concept Languages}.

2120: \newblock In {\em Proc. of 2nd International Conference on Principles of

2121:   Knowledge Representation and Reasoning ({KR}'91)}, pages 335--346, Cambridge,

2122:   MA, April 1991.

2123: 

2124: \bibitem{ALCN2}

2125: B.~Hollunder, W.~Nutt, and M.~Schmidt-Schau{\ss}.

2126: \newblock {Subsumption Algorithms for Concept Description Languages}.

2127: \newblock In {\em Proc. of Europ. Conf. on Artificial Intelligence (ECAI'90)},

2128:   pages 335--346, {Stockolm, Sweden}, 1990.

2129: 

2130: \bibitem{HS01}

2131: {I. Horrocks and U. Sattler}.

2132: \newblock {Ontology Reasoning in the ${\cal SHOQ}(D)$ Description Logic}.

2133: \newblock In {\em Proc. of Intl' Joint Conf. on Artificial Intelligence

2134:   (IJCAI'01)}, pages 199--204, {Seattle, WA}, 2001.

2135: 

2136: \bibitem{ALC}

2137: {M. Schmidt-Schau{\ss} and G. Smolka}.

2138: \newblock {Attributive Concept Descriptions with Complements}.

2139: \newblock {\em Artificial Intelligence}, 48(1):1--26, 1991.

2140: 

2141: \bibitem{complC2}

2142: L.~Pacholski, W.~Szwast, and L.~Tendera.

2143: \newblock {Complexity of Two-variable Logic with Counting}.

2144: \newblock In {\em Proc. Annual IEEE Symp. on Logic in Computer Science

2145:   (LICS'97)}, pages 318--327, {Warsaw, Poland}, 1997.

2146: 

2147: \bibitem{Savi70}

2148: W.~J. Savitch.

2149: \newblock {Relationship between Nondeterministic and Deterministic Tape

2150:   Complexities}.

2151: \newblock {\em Journal of Computer and System Sciences}, 4:177--192, 1970.

2152: 

2153: \bibitem{Tobi01}

2154: S.~Tobies.

2155: \newblock {\em {Complexity Results and Practical Algorithms for Logics in

2156:   Knowledge Representation}}.

2157: \newblock PhD thesis, RWTH Aachen, Germany, 2001.

2158: 

2159: \end{thebibliography}

2160: 

2161: \end{document}

2162: 

2163: 

2164: %%%% TEXT ABSTRACT FOR ARXIV:

2165: 

2166: Description Logics are knowledge representation formalisms

2167: which have been used in a wide range of application domains.

2168: Owing to their appealing expressiveness, we consider in this paper

2169: extensions of the well-known concept language ALC allowing for

2170: number restrictions on complex role expressions.

2171: These have been first introduced by Baader and Sattler as

2172: ALCN(M) languages, with the adoption

2173: of role constructors M subset-of {o,-,And,Or}.

2174: In particular, they showed in 1999 that, although ALCN(o)

2175: is decidable, the addition of other operators may easily lead

2176: to undecidability: in fact, ALCN(o,And) and ALCN(o,-,Or)

2177: were proved undecidable.

2178: 

2179: In this work, we further investigate the computational properties

2180: of the ALCN family, aiming at narrowing the decidability gap left open

2181: by Baader and Sattler's results.

2182: In particular, we will show that

2183: ALCN(o) extended with inverse roles both in number and in value restrictions

2184: becomes undecidable, whereas it can be safely extended

2185: with qualified number restrictions without losing decidability.

2186: