1: %%% $Id: si.tex,v 1.23 2001/06/12 13:14:33 tobies Exp $
2:
3: \newcommand{\satalci}{\textsc{SAT}(\si)\xspace}
4: \newcommand{\satalcni}{\textsc{SAT}(\sin)\xspace}
5:
6: \section{Transitive and Inverse Roles: \si}
7:
8: In this section we study the complexity of reasoning with the DL \si, an
9: extension of the DL \alc with \iemph{transitive roles} and \iemph{inverse roles}:
10:
11: \index{roles!transitive}
12: \index{roles!inverse}
13:
14: \begin{definition}[Syntax and Semantics of \si]\label{def:si-syntax}
15: Let \Names be a set of atomic \emph{concept names}, \Roles a set of atomic
16: \emph{role names}, and $\RolesTrans \subseteq \Roles$ a set of
17: \emph{transitive role names}. With $\overline \Roles := \Roles \cup \{ R^{-1}
18: \mid R \in \Roles \}$ we denote the set of \emph{\si-roles}. The set of
19: \emph{\si-concepts} is built inductively from $\Names$ and $\overline{\Roles}$
20: using the following grammar, where $A \in \Names$ and $R \in \overline
21: \Roles$:
22: \[
23: C ::= A \bnfor \lnot C \bnfor C_1 \sqcap C_2 \bnfor C_1 \sqcup C_2 \bnfor
24: \all R C \bnfor \some R C .
25: \]
26: The semantics of \si-concepts is defined similarly to the semantics of
27: \alc-concepts \wrt an interpretation $\I$, where, for an inverse role $R^{-1}
28: \in \overline \Roles$, we set $(R^{-1})^\I = \{ (y,x) \mid (x,y) \in R^\I \}$.
29: Moreover, we only consider those interpretations that interpret transitive
30: roles $R \in \RolesTrans$ by transitive relations. An \si-concept $C$ is
31: \emph{satisfiable} iff there exists an interpretation $\I$ such that, for
32: every $R \in \RolesTrans$, $R^\I$ is transitive, and $C^\I \neq \emptyset$.
33: Subsumption is defined as usual, again with the restriction to interpretations
34: that interpret transitive roles with transitive relations.
35:
36: \index{si@\si}
37: \index{s@\s}
38: \index{00nr@$\overline{\Roles}$}
39: \index{00nrplus@$\RolesTrans$}
40:
41: With $\s$ we denote the fragment of $\si$ that does not contain any inverse
42: roles. \eod
43: \end{definition}
44:
45: In order to make the following considerations easier, we introduce two functions
46: on roles:
47:
48: \begin{enumerate}
49: \item The inverse relation on roles is symmetric, and to avoid considering roles
50: such as $R^{-1 -1}$, we define a function $\Inv$ which returns the inverse of a
51: role. More precisely, $\Inv(R) = R^{-1}$ if $R$ is a role name, and $\Inv(R) = S$
52: if $R=S^{-1}$. \index{00invr@$\Inv(R)$}
53:
54: \item Obviously, the interpretation $R^\I$ of a role $R$ is transitive if and
55: only if the interpretation of $\Inv(R)$ is transitive. However, this may be
56: required by either $R$ or $\Inv(R)$ being in $\Rplus$. We therefore define a
57: function $\Tr$, \index{00transr@$\Tr(R)$} which is $\mathrm{true}$ iff $R$ must
58: be interpreted with a transitive relation---regardless of whether it is a role
59: name or the inverse of a role name. More precisely, $\Tr(R) = \texttt{true}$
60: iff $R\in \Rplus$ or $\Inv(R)\in\Rplus$.
61: \end{enumerate}
62:
63: \subsection{The \si-algorithm}
64:
65: We will now describe a tableau algorithm that decides satisfiability of
66: \si-concepts in \pspace, thus proving \pspace-completeness of \si-satisfiability.
67: Like other tableau algorithms, the \si-al\-go\-rithm tries to prove the
68: satisfiability of a concept $C$ by constructing a model for $C$. The model is
69: represented by a so-called \iemph{completion tree}, a tree some of whose nodes
70: correspond to individuals in the model, each node being labelled with two sets
71: of \si-concepts. When testing the satisfiability of an \si-concept $C$, these
72: sets are restricted to subsets of $\sub(C)$, where $\sub(C)$ is
73: the set of subconcepts of $C$, which is defined in the obvious
74: way. \index{00subc@$\sub(C)$}
75: Before we formally present the algorithm, we first discuss some problems that
76: need to be overcome when trying to develop an \si-algorithm that can be
77: implemented to run in \pspace.
78:
79: Dealing with transitive roles in tableau algorithms requires extra
80: considerations because transitivity of a role is, generally speaking, a
81: \emph{global} constraint whereas the expansion rules and clash conditions of the
82: tableau algorithms that we have studied so far are of a more \emph{local}
83: nature. They only take into account a single node of the constraint system or at
84: most a node and its direct neighbours. Also, many of our previous considerations
85: relied on the fact that satisfiable concepts have tree models, which, in the
86: presence of transitive roles is no longer the case. To circumvent these
87: problems, we use the solution that has already been used, e.g., by Halpern and
88: Moses \citeyear{HalpernMoses92} to deal with the modal logic $\mathsf{S4}$,
89: which possesses a reflexive and transitive accessibility relation. Instead of
90: directly dealing with models and transitive relations, we use abstractions of
91: models---so called \emph{tableaux}---that disregard transitivity of roles and
92: have the form of a tree. This is done in a way that allows to recover a model of
93: the input concept by transitively closing those role relations that are
94: explicitly asserted in the tableau. To prove satisfiability of the input
95: concept, the \si-algorithm now tries to build a tableau instead of trying to
96: construct a model. Apart from this difference, the \si-algorithm is very similar
97: to the tableau algorithms we have encountered so far: starting from an initial
98: constraint system it employs completion rules until the constraint system is
99: complete, in which case the existence of a tableau is evident, or until an
100: obvious contradiction indicates an unsuccessful run of the (non-deterministic)
101: algorithm.
102:
103: While it would be possible to maintain the use of ABoxes to capture the
104: constraint system that we will encounter during our discussion of DLs with
105: transitive roles, it is much more convenient to emphasise the view of constraint
106: systems as node- and edge-labelled trees, so this view will prevail in the
107: remainder of this chapter.
108:
109: %From those concepts that appear in the label of nodes
110: %in the tableau thus need to be satisfied in the generated model, transitively
111: %closing role relations only effects universal restrictions. Consequently, only
112: %concepts of the form $\all R C$ with $\Tr(R)$ are treated specially by the
113: %algorithm.
114:
115: \subsection{Blocking}
116:
117: Sattler \citeyear{Sattler-KI-1996} shows that concept satisfiability for \s can
118: be determined in polynomial space using an adaptation of the techniques employed
119: by Halpern and Moses \citeyear{HalpernMoses92} to decide satisfiability for the
120: modal logic $\mathsf{S4}$. To understand why these techniques cannot be
121: extended easily to deal with inverse roles, as we have done in
122: Chapter~\ref{chap:alcq} when generalizing from \alcq to \alcqir, we have to
123: discuss the role of \iemph{blocking}.
124:
125: The key difference between the algorithms from the previous chapters and the
126: \si-algorithm lies in the way universal restrictions are propagated through the
127: constraint system: whenever $\all R C$ with $\Tr(R)$ appears in the label of a
128: node $x$ and $x$ has an $R$-neighbour $y$, then not only $C$ is asserted for
129: $y$, but also $\all R C$. This makes sure that $C$ is successively asserted for
130: every node reachable from $x$ via a \emph{chain} of $R$-edges. These are exactly
131: the nodes that are reachable from $x$ with a single $R$-step once $R$ has been
132: transitively closed; exactly these nodes must satisfy $C$ in order for
133: $\all R C$ to hold at $x$.
134:
135: Previously the termination of the tableau algorithms relied on the fact that the
136: nesting of universal and existential restrictions strictly decreases along a
137: path in the tableau. When dealing with transitive roles in the described manner,
138: this is no longer guaranteed. For example, consider a node $x$ labelled $\{C,
139: \some{R}{C}, \all{R}{(\some{R}{C})}\}$, where $R$ is a transitive role. The
140: described approach would cause the new node $y$ that is created due for the
141: \some{R}{C} constraint to receive a label identical to the label of $x$. Thus,
142: the expansion process could be repeated indefinitely.
143:
144: The way we deal with this problem is by \emph{blocking}: halting the expansion
145: process when a cycle is
146: detected~\cite{Baader91c,Buchheit93,HalpernMoses92,Sattler-KI-1996,BaaderBuchheit+-AIJ-1996,HorrSat-JLC-99}.
147: For logics without inverse roles, the general procedure is to check the
148: constraints asserted for each new node $y$, and if they are a \emph{subset} of
149: the constraints for an existing node $x$, then no further expansion of $y$ is
150: performed: $x$ is said to block $y$. The resulting constraint system
151: corresponds to a cyclic model in which $y$ is identified with
152: $x$.\footnote{For logics with a transitive closure operator it is necessary to
153: check the validity of the cyclic model created by blocking~\cite{Baader91c},
154: but for logics that only support transitive roles the cyclic model is always
155: valid~\cite{Sattler-KI-1996}.} The validity of the cyclic model is an easy
156: consequence of the fact that each $\some{R}{D}$ constraint for $y$ must also be
157: satisfied by $x$ because the constraints for $x$ are a superset of the
158: constraints for $y$. Termination is now guaranteed by the fact that all
159: constraints for individuals in the constraint system are ultimately derived from
160: the decomposition of the input concept $C$, so every set of constraints for an
161: individual must be a subset of the subconcepts of $C$, and a blocking situation must
162: therefore occur within a finite number of expansion steps.
163:
164:
165: \subsubsection{Dynamic Blocking}
166: \label{sec:dynblk}
167:
168: Blocking is more problematic when inverse roles are added to the logic, and a
169: key feature of the algorithms presented in~\cite{HorrSat-JLC-99} was the
170: introduction of a \iemph{dynamic blocking} strategy. It uses label equality
171: instead of the subset condition, and it allows blocks to be established,
172: broken, and re-established. \index{blocking!dynamic blocking}
173:
174: Label inclusion as a blocking criterion is no longer correct in the presence of
175: inverse roles because roles are now bi-directional, and hence universal
176: restrictions at the blocking node can conflict with the constraints for the
177: predecessor of the blocked node.
178:
179: %Consider the concept
180: %\[
181: %\neg A \sqcap \some R {(A \sqcap \all {R^{-1}} {\neg A})} \sqcap \all R D
182: %\]
183: %where $D$ stands for the concept $(\some R A \sqcap \all {R^{-1}} {\all {R^{-1}} {\neg A}})$ .
184:
185:
186: Taking the above example of a node labelled $\{C, \some{R}{C},
187: \all{R}{(\some{R}{C})}\}$, if the successor of this node were blocked by a node
188: whose label additionally included $\all{R^{-1}}{\neg C}$, then the cyclic model
189: would clearly be invalid. This is shown in Figure~\ref{fig:block-cyclic}, where
190: $x$ blocks its $R$-successor $y$ (if subset-blocking is assumed) and hence in
191: the induced model (shown on the right), there exists an $R$-cycle from $x$ to $x$. Hence, $C$ and
192: $\all {R^{-1}} {\neg C}$, which have both been asserted for $x$, now stand in a
193: conflict.
194:
195: \begin{figure}[tbh]
196: \begin{center}
197: \vspace{2ex}
198: \parbox{5.75in}{\input{block-bsp5.pstex_t}}
199: \caption{An invalid cyclic model}
200: \label{fig:block-cyclic}
201: \end{center}
202: \end{figure}
203:
204:
205:
206: %There are concepts for which this
207: %problem indeed leads to wrong answers of the algorithm if label inclusion is
208: %used as the blocking criterion.
209: %where this kind
210: %of problem leads to an unsound algorithm if label inclusion is used
211: In~\cite{HorrSat-JLC-99}, this problem was overcome by allowing a node $x$ to be
212: blocked by one of its ancestors if and only if they were labelled with the
213: same set of concepts.
214:
215: Another difficulty introduced by inverse roles is the fact that it is no longer
216: possible to establish a block on a once-and-for-all basis when a new node is
217: added to the tree. This is because further expansion in other parts of the tree
218: could lead to the labels of the blocking and/or blocked node being extended and
219: the block being invalidated. Consider the example sketched in
220: Figure~\ref{fig:block-exa}, which shows parts of a tableau that was generated
221: for the concept
222: %
223: $$A\sqcap \exists S. ( \exists R.\top \sqcap \exists P. \top \sqcap \forall R.C
224: \sqcap \forall P.(\exists R.\top) \sqcap \forall P.(\forall R.C) \sqcap \forall
225: P.(\exists P.\top)),
226: $$
227: %
228: where $C$ represents the concept
229: %
230: $$\forall R^{-1} . (\forall P^{-1} . (\forall S^{-1} . \neg A)).$$
231: %
232: This concept is clearly not satisfiable: $w$ has to be an instance of $C$, which
233: implies that $x$ is an instance of $\neg A$. This is inconsistent with $x$
234: being an instance of $A$.
235:
236: \begin{figure}[tbh]
237: \begin{center}
238: \vspace{2ex}
239: \parbox{3.75in}{\input{block-bsp2.pstex_t}}
240: \caption{A tableau where dynamic blocking is crucial}
241: \label{fig:block-exa}
242: \end{center}
243: \end{figure}
244:
245: Since $P$ is a transitive role, all universal value restrictions over $P$ are
246: propagated from $y$ to $z$, hence $y$ and $z$ are labelled with the same
247: constraints and hence $z$ is blocked by $y$. If the blocking of $z$ was not
248: subsequently broken when $\forall P^{-1}.(\forall S^{-1}.\neg A)$ is added to
249: $\Lab(y)$ from $C\in \Lab(v)$, then $\neg A$ would never be added to $\Lab(x)$
250: and the unsatisfiability would not be detected.
251:
252: As well as allowing blocks to be broken, it is also necessary to continue with
253: some expansion of blocked nodes, because $\all{R}{C}$ concepts in their labels
254: could affect other parts of the tree. Again, let us consider the example in
255: Figure~\ref{fig:block-exa}. After the blocking of $z$ is broken and $\forall
256: P^{-1}.(\forall S^{-1}.\neg A)$ is added to $\Lab(z)$ from $C \in \Lab(w)$, $z$ is
257: again blocked by $y$. However, the universal value restriction $\forall
258: P^{-1}.(\forall S^{-1}.\neg A) \in \Lab (z)$ has to be expanded in order to detect the
259: unsatisfiability.
260:
261: These problems are overcome by using \emph{dynamic} blocking: using label
262: equality as blocking criterion and allowing blocks to be dynamically established
263: and broken as the expansion progresses, and continuing to expand $\all{R}{C}$
264: concepts in the labels of blocked nodes.
265:
266: \subsubsection{Refined blocking}
267:
268: \index{refined blocking}
269: \index{blocking!refined blocking}
270:
271: As mentioned before, in~\cite{HorrSat-JLC-99}, blocking of nodes is based on
272: label equality. This leads to major problems when trying to establish a
273: polynomial bound on the length of paths in the completion tree. If a node can only be
274: blocked by an ancestor when the labels coincide, then there could potentially be
275: exponentially many ancestors in a path before blocking actually occurs. Due to
276: the non-deterministic nature of the expansion rules, these subsets might
277: actually be generated; the algorithm would then need to store the node labels of
278: a path of exponential length, thus consuming exponential space.
279:
280: This problem is already present when one tries to implement a tableau algorithm
281: for the logic \alcRtrans~\cite{Sattler-KI-1996}, where the non-deterministic nature
282: of the expansion rules for disjunction might lead to the generation of a chain
283: of exponential size before blocking occurs. Consider, for example, the concept
284: %
285: \begin{align*}
286: % D & = \some{R}{\textsc{Top}} \sqcap \all{R}{(\some{R}{\textsc{Top}} \sqcap C)}
287: % \\
288: % C & = (A_1 \sqcup B_1) \sqcap (A_2 \sqcup B_2) \sqcap \dots \sqcap (A_n \sqcup
289: % B_n) \\
290: % \textsc{Top} & = A \sqcup \neg A
291: C & = \some{R}{D} \sqcap \all{R}{(\some{R}{D})} \\ D & = (A_1 \sqcup B_1)
292: \sqcap (A_2 \sqcup B_2) \sqcap \dots \sqcap (A_n \sqcup B_n)
293: \end{align*}
294: %
295: where $R$ is a transitive role. The concept $C$ causes the generation of a chain
296: of $R$-successors for all of which $D$ is asserted. There are $2^n$ possible
297: ways of expanding $D$ because for every disjunctive concept $A_i \sqcup B_i$ the
298: \ruleor-rule can choose to add $A_i$ or $B_i$. The completion tree for $D$ is
299: only complete once one node of this path is blocked and all unblocked nodes
300: (including the blocking node) are fully expanded. For \alcRtrans, a polynomial
301: bound on the length of paths is obtained by applying a simple strategy: a new
302: successor is only generated when no other rule can be applied, and propositional
303: expansion of concepts only takes place if universal restrictions have been
304: exhaustively been dealt with. Once a node is blocked, it is not necessary to
305: perform its propositional expansion because it has already been ensured at the
306: blocked node that such an expansion is possible without causing a clash.
307:
308: However, in the presence of inverse roles, this strategy is no longer possible.
309: Indeed, the expansion rules for \si as they have been presented
310: in~\cite{HorrocksSattler-DL-1998} based on set equality might lead to a tableau
311: with paths of exponential length for $C$---even though $C$ does not contain any
312: inverse roles. This is due to the fact that blocking is established on the basis
313: of label equality. Since the label of the blocked and blocking node must be
314: equal, this implies that, since the label of the blocking node must be fully
315: expanded, this also must hold for the label of the blocked. Since there are
316: $2^n$ possibilities for such an expansion, it might indeed take a path of
317: $2^n+1$ nodes before such a situation necessarily occurs and the completion
318: tree is complete.
319:
320: %Since the blocking node must be fully
321: %propositionally expanded, so must be the blocked node. And because disjunction
322: %is resolved in a non-deterministic way, this can lead to the generation of $2^n$
323: %different expansions of the concept $C$.
324:
325: In order to obtain a tableau algorithm that circumvents this problem and
326: guarantees blocking after a polynomial number of steps, we will keep the
327: information that is relevant for blocking separated from the ``irrelevant''
328: information (due to propositional expansion) in a way which allows for a simple
329: and comprehensible tableau algorithm. In the following, we will explain this
330: ``separation'' idea in more detail.
331:
332: \begin{figure}[h]
333: \begin{center}
334: \vspace{2ex}
335: \parbox{3.25in}{\input{block-bsp3.pstex_t}}
336: \caption{Refined blocking}
337: \label{fig:block-sit}
338: \end{center}
339: \end{figure}
340:
341: Figure~\ref{fig:block-sit} shows a blocking situation. Assume node $y$ to be
342: blocked by node $x$. When generating a model from this tree, the blocked node
343: $y$ will be omitted and $y'$ will get $x$ as an $S$-successor, which is
344: indicated by the backward arrow. On the one hand, this construction yields a
345: new $S$-successor $x$ of $y'$, a situation which is taken care of by the subset
346: blocking used in the normal \alcRtrans tableau algorithms. On the other hand,
347: $x$ receives a new $S^{-1}$-successor $y'$. Now blocking has to make sure that, if
348: $x$ must satisfy a concept of the form $\all{S^{-1}}{D}$, then $D$ (and
349: $\all{S^{-1}}{D}$ if $S$ is a transitive role) is satisfied by $y'$.
350:
351:
352: This was dealt with by equality blocking in \cite{HorrSat-JLC-99}. In the
353: following algorithm it will be dealt with using two labels per node and a
354: modified blocking condition that takes these two labels into account. In addition
355: to the label $\Lab$, each node now has a second label $\BLab$, where the latter
356: is always a subset of the former. The label $\Lab$ contains complete
357: information, whereas $\BLab$ contains only information relevant to blocking.
358: Propositional consequences of concepts in $\Lab$ and concepts being propagated
359: ``upwards'' in the tree are stored in $\Lab$ only, as they are not important for
360: blocking as long as they are not universal restrictions that state requirements
361: on the predecessor in the completion tree. The modified blocking condition now
362: looks as follows. For a node $y$ to be blocked by a node $x$ we require that
363:
364: \begin{itemize}
365: \item the label $\BLab(y)$ of the blocked node $y$ is contained in the label
366: $\Lab(x)$ of the blocking node $x$. Expansions of disjunctions are only stored
367: in $\Lab$ and thus cannot prevent a node from being blocked.
368: \item if $y$ is reachable from its predecessor in the completion tree via the
369: role $S$, then the universal restrictions along $\Inv(S)$ asserted
370: for $y$ are the same as those asserted for $x$. This takes care of the fact
371: that the predecessor $y'$ of the blocked node $y$ becomes a new
372: $\Inv(S) $-successor of the blocking node $x$.
373: \end{itemize}
374:
375:
376:
377: %We split the labels of a node $x$ into two sets $\BLab(x)$ and
378: %$\Lab(x)$ to keep track of these two conditions more easily. We also use this
379: %separation to overcome the problem that the unfolding of concepts of the form
380: %\[ (A_1 \sqcup B_1) \sqcap \dots \sqcap (A_n \sqcup B_n) \]
381: %may lead non-deterministically to $2^n$ different unfoldings.
382:
383:
384: %More precisely, the new definition of blocking reads as follows:
385:
386: %A node $y$ is \emph{blocked} if for, some ancestor $x$, $x$ is blocked or
387: %\[ \BLab(y) \subseteq \Lab(x) \quad \text{and} \quad \Lab(y)/\Inv(S) =
388: %\Lab(x)/\Inv(S) \] where $y'$ is the predecessor of $y$ in the completion tree
389: %and $\Lab\tuple{y'}{y}=S$. We define
390: %\[\Lab(y)/\Inv(S) =
391: %\{ \all{\Inv(S)}{C} \in \Lab(y) \}.
392: %\]
393:
394: Summing up, we build a completion tree in a way that, for all nodes $x$,
395:
396: \begin{itemize}
397: \item we have $\BLab(x) \subseteq \Lab(x)$,
398: \item $\BLab(x)$ contains only concepts which move \emph{down} the tree,
399: \item $\Lab(x)$ contains, additionally, all concepts which move \emph{up} the
400: tree, and
401: \item expansion of disjunctions and conjunctions only affects $\Lab(x)$.
402: \end{itemize}
403:
404:
405: \subsection{A Tableau Algorithm for \si}
406:
407: We now present a tableau algorithm derived from the one presented
408: in~\cite{HorrSat-JLC-99}. We shape the rules in a way that allows for the
409: separation of the concepts which are relevant for the two parts of the blocking
410: condition. For ease of construction, we assume all concepts to be in
411: \emph{negation normal form} (NNF), \index{negation normal form} that is, negation occurs only in front of
412: concept names. Any \si-concept can easily be transformed into an equivalent one in
413: NNF in the same way as this can be done for \alc-concepts
414: (Definition~\ref{def:nnf}).
415:
416: The soundness and completeness of the algorithm will be proved by showing that
417: it creates a \emph{tableau} for $C$. In contrast to the approach we have taken
418: in the previous chapters, where a constraint system stood in direct
419: correspondence to a model, here we introduce tableaux as intermediate
420: structures that encapsule the transition from the \emph{syntactic object} of a
421: completion tree to the \emph{semantical} object of a model and takes care of the
422: transitive roles on that way. This makes it possible for the algorithm to
423: operate on trees even though \si does not have a genuine tree model property due
424: to its transitive roles.
425:
426: \begin{definition}[A Tableau for \si] \label{def:si-tableau}
427: If $C$ is an \si-concept in NNF and $\overline{\Roles}_C$
428: \index{00nrc@$\overline{\Roles}_C$} is the set of roles occurring in $C$
429: together with their inverses, a \emph{tableau} \index{tableau!for si@for \si}
430: $\mcT$ for $C$ is a triple $(\mcS,\TabLab,\Edges)$ such that $\mcS$ is a
431: non-empty set, $\TabLab:\mcS \rightarrow 2^{\textit{sub}(C)}$ maps each
432: element of $\mcS$ to a subset of $\textit{sub}(C)$, and
433: $\Edges:\overline{\Roles}_C \rightarrow 2^{\mcS \times \mcS}$ maps each role
434: in $\overline{\Roles}_C$ to a set of pairs of individuals. In addition, the
435: following conditions must be satisfied:
436: \begin{itemize}
437: \item [\tab 1] There is an $s \in \mcS$ with $C \in \TabLab(s)$, and
438: \end{itemize}
439: for all $s,t \in \mcS$, $A,C_1,C_2,D\in \mathit{sub}(C)$, and $R\in \overline{\Roles}_C$,
440: \begin{enumerate}
441: \item [\tab 2] if $A \in \TabLab(s)$, then $\neg A \notin
442: \TabLab(s)$, for $A \in \Names$,
443: \item [\tab 3] if $C_1 \sqcap C_2 \in \TabLab(s)$, then $C_1\in\TabLab(s)$ and
444: ${C_2\in\TabLab(s)}$,
445: \item [\tab 4] if $C_1 \sqcup C_2 \in \TabLab(s)$, then $C_1 \in \TabLab(s)$ or $C_2 \in \TabLab(s)$,
446: \item [\tab 5] if $\some{R}{D} \in \TabLab(s)$, then there is some $t \in \mcS$ such
447: that $\tuple{s}{t} \in \Edges(R)$ and $D \in \TabLab(t)$,
448: \item [\tab 6] if $\all{R}{D} \in \TabLab(s)$ and $\tuple{s}{t} \in \Edges(R)$, then $D
449: \in \TabLab(t)$,
450: \item [\tab 7] if $\all{R}{D} \in \TabLab(s)$, $\tuple{s}{t} \in \Edges(R)$ and $\Tr(R)$,
451: then $\all{R}{D} \in \TabLab(t)$, and
452: \item [\tab 8] $\tuple{s}{t}\in \Edges(R)$ iff $\tuple{t}{s}\in
453: \Edges(\Inv(R))$. \eod
454: \end{enumerate}
455:
456: \end{definition}
457:
458: A tableau $\mcT$ for a concept $C$ is a ``syntactic witness'' for the satisfiability
459: of $C$:
460:
461:
462: \begin{lemma} \label{lem:si-tableau}
463: An \si-concept $C$ is satisfiable iff there exists a tableau for $C$.
464: \end{lemma}
465:
466: \begin{proof}
467: For the \emph{if}-direction, if $\mcT = (\mcS,\TabLab,\Edges)$ is a tableau
468: for $C$ with $C\in \TabLab(s_0)$, a model $\mathcal{I} = (\domain, \cdot\ifunc)$
469: of $C$ can be defined as follows:
470: %
471: \[
472: \begin{array}{rcl} \hspace{2cm}\domain & = & \mcS, \\[0.5ex]
473: %\multicolumn{3}{l}{\mbox{ for all
474: %concept names A in $\textit{sub}(D)$:}} \\
475: A\ifunc & = & \{s \mid A \in \TabLab(s)\} \quad\mbox{for all concept names A in
476: $\textit{sub}(C)$}, \\[0.5ex] R\ifunc & = & \left\{ \begin{array}{ll} \Edges(R)^+
477: & \mbox{if $\Tr(R)$} \\ \Edges(R) & \mbox{otherwise},
478: \end{array}
479: \right.
480: \end{array}
481: \]
482: %
483: where $\Edges(R)^+$ denotes the transitive closure of $\Edges(R)$. Transitive
484: roles are interpreted by transitive relations by definition. By induction on
485: the structure of concepts, we show that, if $D\in \TabLab(s)$, then $s\in
486: D\ifunc$. This implies $C\ifunc\neq \emptyset$ because $s_0\in C\ifunc$. Let
487: $D\in \TabLab(s)$:
488: %
489: \begin{enumerate}
490: \item If $D = A \in \Names$ is a concept name, then $s\in D^\I$ by definition.
491: \item If $D=\neg A$ for $A \in \Names$ then $A \notin \TabLab(s)$ (due to \tab
492: 2 ), so $s \in \domain \setminus A\ifunc= D\ifunc$.
493: \item If $D= (C_1 \sqcap C_2)$, then, due to \tab 3, $C_1 \in \TabLab(s)$ and
494: $C_2 \in \TabLab(s)$, and hence, by induction, $s \in C_1\ifunc$ and $s\in
495: C_2\ifunc$. Thus, $s\in (C_1 \sqcap C_2)\ifunc$.
496: \item The case $D=(C_1 \sqcup C_2)$ is analogous to the previous one.
497: \item If $D= \some{R}{E}$, then, due to \tab 5, there is some $t \in \mcS$
498: such that $\tuple{s}{t} \in \Edges(R)$ and $E \in \TabLab(t)$. By definition
499: of $\I$, $\tuple{s}{t} \in R\ifunc$ holds as follows. It is immediate, if
500: $R \in \Roles$. If $R = S^{-1}$ for $S \in \Roles$, then $\tuple s t \in
501: \Edges(R)$ implies $\tuple t s \in \Edges(S)$ by \tab 8. Hence, $\tuple t s
502: \in S^\I$ and $\tuple s t \in R^\I$ holds. By induction, $t\in E\ifunc$ and
503: hence $s \in (\some{R}{E})\ifunc$.
504: \item If $D= (\all{R}{E})$ and $\tuple{s}{t} \in R \ifunc$, then either
505: \begin{enumerate}
506: \item $\tuple{s}{t} \in\Edges(R)$ and $E\in \TabLab(t)$ (due to \tab 6), or
507: \item $\tuple{s}{t} \not\in\Edges(R)$. Due to $\tab 8$, this can only be the
508: case if $R$ is transitive and there exists a path of length $n\geq 1$ such
509: that $\tuple{s}{s_1},$ $\tuple{s_1}{s_2},\ldots,$ $\tuple{s_n}{t}\in
510: \Edges(R)$. Due to \tab 7, $\all{R}{E}\in \TabLab(s_i)$ for all
511: $1\leqslant i \leqslant n$, and we have $E\in \TabLab(t)$, again due to
512: \tab 6.
513: \end{enumerate}
514: In both cases, by induction $t\in E\ifunc$ holds, and hence $s\in
515: (\all{R}{E})\ifunc$.
516: \end{enumerate}
517:
518: \bigskip
519:
520: For the converse direction, if $\mathcal{I} = (\domain, \cdot\ifunc)$ is a
521: model of $C$, then a tableau $\mcT = (\mcS,\TabLab,\Edges)$ for $C$ can be
522: defined by:
523: %
524: \begin{eqnarray*}
525: \mcS & = & \domain, \\
526: \Edges(R) & = & R\ifunc, \\
527: \TabLab(s) & = & \{D \in \textit{sub}(D) \mid s \in D\ifunc \}.
528: \end{eqnarray*}
529:
530: It remains to demonstrate that $\mcT$ is a tableau for $C$:
531: %
532: \begin{enumerate}
533: \item $\mcT$ satisfies \tab 1 -- \tab 6 and \tab 8 as a direct consequence of the
534: semantics of \si concepts and of inverse roles.
535: \item If $s \in (\all{R}{D})\ifunc$, $\tuple{s}{t} \in R\ifunc$ and $\Tr(R)$,
536: then $t \in (\all{R}{D})\ifunc$ unless there is some $u$ such that
537: $\tuple{t}{u} \in R\ifunc$ and $u \notin D\ifunc$. However, if $\tuple{s}{t}
538: \in R\ifunc$, $\tuple{t}{u} \in R\ifunc$ and $\Tr(R)$, then
539: $\tuple{s}{u} \in R\ifunc$, which would imply $s \notin (\all{R}{D})\ifunc$.
540: $T$ therefore satisfies \tab 7. \qed
541: \end{enumerate}
542: \end{proof}
543:
544: \subsection{Constructing an \si Tableau}\label{section:si-algo}
545:
546: From Lemma~\ref{lem:si-tableau}, it follows that an algorithm that constructs a
547: tableau for an \si-concept $C$ can be used as a decision procedure for the
548: satisfiability of $C$. Such an algorithm will now be described.
549:
550: Like the tableau algorithms that we have studied so far, the algorithm for \si
551: works by manipulating a constraint system. In the presence of blocking, and
552: especially in the case of the refined blocking we are using for \si, it is more
553: convenient to emphasise the graph structure of the constraint system and deal
554: with an edge- and node-labelled graph instead of an ABox. In case of the
555: \si-algorithm, the constraint system has the form of a \emph{completion tree}.
556:
557: \begin{algorithm}[The \si-algorithm]\label{alg:si}
558: Let $C$ be an \si-concept in NNF to be tested for satisfiability and
559: $\overline{\Roles}_C$ the set of roles that occur in $C$ together with their
560: inverse. A \emph{completion tree} \index{completion tree!for si@for \si}
561: $\Tree = (\bfV, \bfE, \bfL, \BLab)$ is a labelled tree in which each node $x
562: \in \bfV$ is labelled with two subsets $\Lab(x)$ and $\BLab(x)$ of
563: $\textit{sub}(C)$. Furthermore, each edge $\tuple{x}{y} \in \bfE$ in the tree
564: is labelled $\Lab\tuple{x}{y}= R$ for some (possibly inverse) role $R \in
565: \overline{\Roles}_C$. Nodes and edges are added when expanding \some{R}{D}
566: and \some{R^{-1}}{D} constraints; they correspond to relationships between
567: pairs of individuals and are always directed from the root node to the leaf
568: nodes. The algorithm expands the tree by extending $\Lab(x)$ (and possibly
569: $\BLab(x)$) for some node $x$, or by adding new leaf nodes.
570:
571: \index{si@\si!tableau algorithm}
572: \index{tableau algorithm!for si@for \si}
573:
574: A completion tree \Tree is said to contain a \emph{clash} if, for a node $x$
575: in \Tree, it holds that there is a concept name $A$ such that $\{A, \neg A\}
576: \subseteq \Lab(x)$.
577:
578: If nodes $x$ and $y$ are connected by an edge $\tuple{x}{y} \in \bfE$, then $y$ is
579: called a \emph{successor} of $x$ and $x$ is called a \emph{predecessor} of
580: $y$. If $\Lab\tuple{x}{y} = R$, then $y$ is called an $R$-\emph{successor} of
581: $x$ and $x$ is called an $\Inv(R)$-\emph{predecessor} of $y$.
582:
583: \emph{Ancestor} is the transitive closure of \emph{predecessor} and
584: \emph{descendant} is the transitive closure of \emph{successor}. A node $y$
585: is called an $R$\emph{-neighbour} of a node $x$ if either $y$ is an
586: $R$-successor of $x$ or $y$ is an $R$-predecessor of $x$.
587:
588: To define the blocking condition we need the following auxiliary definition.
589: For a (possibly inverse) role $S \in \overline{\Roles}_C$, we define the set
590: $\Lab(y)/S$ by \index{00lxbyr@$\Lab(y)/R$}
591: \[
592: \Lab(y)/S = \{ \all{S}{D} \in \Lab(y)\} .
593: \]
594: A node $y$ is \emph{blocked} if for some ancestor $x$ of $y$, $x$ is blocked or
595: \[
596: \BLab(y) \subseteq \Lab(x) \quad \text{and} \quad \Lab(y)/\Inv(S) =
597: \Lab(x)/\Inv(S)
598: \]
599: for the unique predecessor $y'$ of $y$ in the completion tree,
600: $\Lab\tuple{y'}{y}=S$ holds.
601:
602: The algorithm initializes a tree \Tree to contain a single node $x_0$, called
603: the \emph{root} node, with $\Lab(x_0) = \BLab(x_0) = \{C\}$. \Tree is then
604: expanded by repeatedly applying the rules from Figure~\ref{fig:si-rules}.
605:
606: The \ruleex-rule is called \emph{generating}; all other rules are called
607: \emph{non-generating}.
608:
609: \begin{figure}[tb!]
610: \begin{center}
611: \begin{tabular}{@{}l@{$\;$}l@{$\;$}l}%{lll}
612: \ruleand: & \bfif \hfill 1. & $C_1 \sqcap C_2 \in \Lab(x)$ and \\ &
613: \hfill 2. & $\{C_1,C_2\} \not\subseteq \Lab(x)$ \\ & \bfthen & $\Lab(x)
614: \ruleand \Lab(x) \cup \{C_1,C_2\}$ \\[1ex]
615:
616: \ruleor: & \bfif \hfill 1. & $C_1 \sqcup C_2 \in \Lab(x)$ and \\ &
617: \hfill 2. & $\{C_1,C_2\} \cap \Lab(x) = \emptyset$ \\ & \bfthen & $\Lab(x)
618: \ruleor \Lab(x) \cup \{E\}$ for some $E\in \{C_1,C_2 \}$\\[1ex]
619:
620: \rulefa: & \bfif \hfill 1. & $\all{R}{D} \in \Lab(x)$ and \\ & \hfill
621: 2. &there is an $R$-successor $y$ of $x$ with $D \notin \BLab(y)$ \\ & \bfthen &
622: $\Lab(y) \rulefa \Lab(y) \cup \{D\}$ and $\BLab(y) \rulefa \BLab(y) \cup
623: \{D\}$ \bfor\\ & \hfill 2'.&there is an $R$-predecessor $y$ of $x$
624: with $D \notin \Lab(y)$ \\ & \bfthen & $\Lab(y) \rulefa \Lab(y) \cup
625: \{D\}$ and delete \emph{all} descendants of $y$. \\[1ex]
626:
627: \rulefatr: & \bfif \hfill 1. & $\all{R}{D} \in \Lab(x)$ and $\Tr(R)$
628: and \\ & \hfill 2. &there is an $R$-successor $y$ of $x$ with $\all{R}{D}
629: \notin \BLab(y)$ \\ & \bfthen & $\Lab(y) \rulefatr \Lab(y) \cup
630: \{\all{R}{D}\}$ and $\BLab(y) \rulefatr \BLab(y) \cup
631: \{\all{R}{D}\}$ \bfor \\ & \hfill 2'. &there is an $R$-predecessor $y$ of $x$
632: with $\all{R}{D} \notin \Lab(y)$ \\ & \bfthen & $\Lab(y) \rulefatr
633: \Lab(y) \cup \{\all{R}{D}\}$ and delete \emph{all} descendants of $y$. \\[1ex]
634:
635: \ruleex: & \bfif \hfill 1. & $\some{R}{D} \in \Lab(x)$, $x$ is not
636: blocked and no non-generating rule \\ && is applicable to $x$ and any of
637: its ancestors, and
638: \\ & \hfill 2. & $x$ has no $R$-neighbour $y$ with $D\in \BLab(y)$ \\ &
639: \bfthen & create a new node $y$ with $\Lab\tuple{x}{y}=R$ and $\Lab(y)=
640: \BLab(y) = \{D\}$ \\[1ex]
641: \end{tabular}
642: \caption{Tableau expansion rules for \si}
643: \label{fig:si-rules}
644: \end{center}
645: \index{00ruleand@\ruleand}
646: \index{00ruleor@\ruleor}
647: \index{00rulefa@\rulefa}
648: \index{00rulefatr@\rulefatr}
649: \index{00ruleex@\ruleex}
650: \index{completion rules!for si@for \si}
651: \index{si@\si!completion rules}
652: \end{figure}
653:
654: The completion tree is \emph{complete} if, for some node $x$, $\Lab(x)$
655: contains a clash or if none of the expansion rules is applicable. If the
656: expansion rules can be applied in such a way that they yield a complete,
657: clash-free completion tree, then the algorithm returns ``$C$ is satisfiable'';
658: otherwise, the algorithm returns ``$C$ is not satisfiable''. \eod
659: \end{algorithm}
660:
661:
662:
663: Like for all other tableau algorithms studied in this thesis, it turns out (see
664: the proof of Lemma~\ref{lemma:si-completeness}) that the choice of which rule to
665: apply where and when is don't-care non-deterministic---no choice can prohibit the
666: discovery of a complete and clash-free completion tree for a satisfiable
667: concept. On the other hand, as before, the choice of the \ruleor-rule is
668: don't-know non-deterministic---only certain choices will lead to the discovery of
669: a complete and clash-free completion tree for a satisfiable concept. For an
670: implementation this means that an arbitrary strategy that selects which rule to
671: apply where will yield a complete implementation but exhaustive search is
672: required to consider the different choices of the \ruleor-rule. A similar
673: situation exist in case of the \shiq-algorithm in
674: Section~\ref{sec:shiq-practical}, where it follows from the proof of
675: Lemma~\ref{lemma:shiq-completeness} that choice of which rule to apply where is
676: don't-care non-deterministic.
677:
678:
679: Note that in the definition of successor and predecessor, the tree structure is
680: reflected. If $y$ is an $R$-successor of $x$ than this implies that $y$ is
681: successor of $x$ in the completion tree and it is \emph{not} the case that $x$
682: is an $\Inv(R)$-predecessor of $y$. Successor and predecessor always refer to
683: the relative position of nodes in the completion tree. This is necessary
684: because, in the construction of a tableau from a complete and clash-free
685: completion tree, the edges pointing to blocked successors will be redirected to
686: the respective blocking nodes, which makes the relative position of nodes in the
687: completion tree significant.
688:
689: We are aiming for a \pspace-decision procedure, so, like the\alcqir-algorithm
690: (Algorithm~\ref{alg:alcqir}), the \rulefa- and \rulefatr-rules delete parts of
691: the completion tree whenever information is propagated upward in the completion
692: tree to make tracing possible.
693:
694: \subsubsection{Correctness}\label{sec:si-soundness}
695:
696: As before, correctness of the algorithm will be demonstrated by proving that,
697: for an \si-concept $C$, it always terminates and that it returns ``satisfiable''
698: if and only if $C$ is satisfiable. To prove this, we follow a slightly different
699: approach than the one that is indicated by
700: Theorem~\ref{theo:generic-correctness}. The reason for this is that it is
701: unclear how to deal with blocked nodes when trying to define a suitable notion
702: of satisfiability for a completion tree. We will come back to this topic.
703:
704: Before we start proving the properties we need to establish correctness of the
705: \si-algorithm, let us state an obvious property of the \si-algorithm:
706:
707: \begin{lemma}\label{lem:label-subsets}
708: Let \Tree be a completion tree generated by the \si-algorithm. Then, for every
709: node $x$ of \Tree, $\BLab(x) \subseteq \Lab(x)$.
710: \end{lemma}
711:
712: \begin{proof}
713: Obviously, $\BLab(x_0) \subseteq \Lab(x_0)$ holds for the only node $x_0$ of
714: the initial tree. Subsequently, whenever a concept $D$ is added to $\BLab(x)$
715: by an application of one of the rules, then it is always also added to
716: $\Lab(x)$. \qed
717: \end{proof}
718:
719: We first show termination of the algorithm:
720:
721: \begin{lemma}[Termination]\label{lemma:si-termination}
722: For each \si-concept $C$, the tableau algorithm terminates.
723: \end{lemma}
724:
725: \begin{proof}
726: Let $m = \Card{\textit{sub}(C)}$. Obviously, $m$ is linear in the length of
727: $C$. Termination is a consequence of the following properties of the expansion
728: rules:
729: %
730: \begin{enumerate}
731: \item The expansion rules never remove concepts from node labels.
732: \item Successors are only generated for concepts of the form \some{R}{D} and,
733: for any node, each of these concepts triggers the generation of at most one
734: successor. Since $\textit{sub}(C)$ contains at most $m$ concepts of the
735: form \some{R}{D}, the out-degree of the tree is bounded by $m$.
736: \item Nodes are labelled with nonempty subsets of $\textit{sub}(C)$. If a
737: path $p$ is of length $>2^{2m}$, then there are 2 nodes $x,y$ on
738: $p$, with $\Lab(x)=\Lab(y)$ and $\BLab(x) = \BLab(y)$, and blocking occurs.
739: Since a path on which nodes are blocked cannot become longer, paths are of
740: length at most $2^{2m}+1$.
741: \end{enumerate}
742:
743: An infinite run of the completion algorithm can thus only occur due
744: to an infinite number of deletions of nodes of the tree. That this
745: can never happen can be shown in exactly the same way this has been
746: done in the proof of Lemma~\ref{lem:alcqri-alg-terminates}. \qed
747: \end{proof}
748:
749: \begin{lemma}[Soundness]\label{lemma:si-soundness}
750: If the \si-algorithm generates a complete and clash-free completion tree for a
751: concept $C$, then $C$ has a tableau.
752: \end{lemma}
753:
754: \begin{proof}
755: Let $\Tree = (\bfV, \bfE, \Lab, \BLab)$ be the complete and clash-free
756: completion tree constructed by the tableau algorithm for $C$. A tableau $\mcT
757: = (\mcS,\TabLab,\Edges)$ can be defined by
758: \[
759: \begin{array}{@{}r@{\;}c@{\;}l}%{r@{\,}c@{\,}l}
760: \mcS &=& \{x \mid \mbox{$x$ is a node in \Tree, and $x$ is not
761: blocked}\},\\[0.5ex]
762: \TabLab&=& \Lab|_{\mcS},\\[0.5ex]
763: \Edges(R) & = & \{\tuple{x}{y} \in
764: \mcS \times \mcS \mid \begin{array}[t]{l@{\,}l} 1. & y \mbox{ is
765: an $R$-neighbour of }x\quad\emph{or} \\ 2. & \exists z . \Lab\tuple{x}{z} = R \mbox{
766: and $y$ blocks $z$} \quad\emph{or} \\ 3. & \exists z . \Lab\tuple{y}{z} = \Inv(R)
767: \mbox{ and $x$ blocks $z$}\}.
768: \end{array}
769: \end{array}
770: \]
771: We now show that $\mcT$ is a tableau for $C$. By definition of $\mcT$,
772: we have $\Lab = \TabLab$ for all $x \in \mcS$, so it is sufficient to establish
773: the required properties for the function $\Lab$.
774:
775: \begin{itemize}
776: \item $C \in \Lab(x_0)$ for the root $x_0$ of \Tree and, since $x_0$ has no
777: predecessors, it cannot be blocked. Hence $C \in \Lab(s)$ for some $s \in
778: \mcS$ and \textbf{\tab 1} holds.
779: \item \textbf{\tab 2} is satisfied because \Tree is clash-free.
780: \item \textbf{\tab 3} and \textbf{\tab 4} are satisfied because neither the \ruleand-rule nor
781: the \ruleor-rule apply to any $x \in \mcS$. Hence $\Lab(x)$ satisfies the
782: required properties.
783: \item \textbf{\tab 5} is satisfied because, for all $x \in \bfS$, if $\some{R}{D}
784: \in \Lab(x)$, then the \ruleex-rule ensures that there is either:
785: \begin{enumerate}
786: \item an $R$-predecessor $y$ with $D \in \BLab(y) \subseteq \Lab(y)$ (see
787: Lemma~\ref{lem:label-subsets}). Because $y$ is a predecessor of $x$ (which
788: is an unblocked node), it cannot be blocked, so $y \in \mcS$ and $\tuple{x}{y}
789: \in \Edges(R)$.
790: \item an $R$-successor $y$ with $D \in \BLab(y) \subseteq \Lab(y)$ (again,
791: see Lemma~\ref{lem:label-subsets}). If $y$ is not blocked, then $y \in
792: \mcS$ and $\tuple{x}{y} \in \Edges(R)$. Otherwise, $y$ is blocked
793: by some $z$ with $\BLab(y) \subseteq \Lab(z)$. Hence $D \in \Lab(z)$, $z
794: \in \mcS$ and $\tuple{x}{z} \in \Edges(R)$.
795: \end{enumerate}
796: \item To show that \textbf{\tab 6} is satisfied for all $x \in \mcS$, if $\all{R}{D}
797: \in \Lab(x)$ and $\tuple{x}{y} \in \Edges(R)$, we have to consider three
798: possible cases:
799: \begin{enumerate}
800: \item $y$ is an $R$-neighbour of $x$. The \rulefa-rule guarantees $D \in
801: \Lab(y)$.
802: \item $\Lab\tuple{x}{z} = R$, $y$ blocks $z$. Then by the \rulefa-rule
803: we have $D \in \BLab(z)$ and, by the definition of blocking, $\BLab(z)
804: \subseteq \Lab(y)$. Hence $D \in \Lab(y)$.
805: \item $\Lab\tuple{y}{z} = \Inv(R)$, $x$ blocks $z$. From the definition of
806: blocking we have that $\Lab(z)/R = \Lab(x)/R$.
807: Hence $\all{R}{D} \in \Lab(z)$ and the \rulefa-rule guarantees $D \in
808: \Lab(y)$.
809: \end{enumerate}
810: In all three cases, $D \in \Lab(y)$ holds.
811: \item For \textbf{\tab 7}, let $x \in \mcS$ with $\all{R}{D} \in \Lab(x)$,
812: $\tuple{x}{y} \in \Edges(R)$, and $\Tr(R)$. There are three possible cases:
813: \begin{enumerate}
814: \item $y$ is an $R$-neighbour of $x$. The \rulefatr-rule guarantees
815: $\all{R}{D} \in \Lab(y)$.
816: \item $\Lab\tuple{x}{z}= R$, $y$ blocks $z$. Then, by the \rulefatr-rule,
817: we have $\all{R}{D} \in \BLab(z)$ and, by the definition of blocking,
818: $\BLab(z) \subseteq \Lab(y)$. Hence $\all{R}{D} \in \Lab(y)$.
819: \item $\Lab\tuple{y}{z} = \Inv(R)$, $x$ blocks $z$. From the definition of
820: blocking, we have that $\Lab(z)/R = \Lab(x)/R$. Hence $\all{R}{D} \in
821: \Lab(z)$ and the \rulefatr-rule guarantees $\all{R}{D} \in \Lab(y)$.
822: \end{enumerate}
823: \item \textbf{\tab 8} is satisfied because, for each $\tuple{x}{y} \in \Edges(R)$,
824: either:
825: \begin{enumerate}
826: \item $x$ is an $R$-neighbour of $y$, so $y$ is an $\Inv(R)$-neighbour of
827: $x$ and $\tuple{y}{x} \in \Edges(\Inv(R))$.
828: \item $\Lab\tuple{x}{z} = R$ and $y$ blocks $z$, so $\Lab\tuple{x}{z} =
829: \Inv(\Inv(R))$ and $\tuple{y}{x} \in \Edges(\Inv(R))$.
830: \item $\Lab\tuple{y}{z} = \Inv(R)$ and $x$ blocks $z$, so $\tuple{y}{x}
831: \in \Edges(\Inv(R))$. \qed
832: \end{enumerate}
833: \end{itemize}
834: \end{proof}
835:
836: We have already mentioned that it is problematic to define a suitable notion of
837: satisfiability for \si-completion trees (as it would be required by
838: Theorem~\ref{theo:generic-correctness}) due to blocking. As one can see, the
839: blocked nodes of the completion tree do not play a r{\^o}le when defining the
840: tableau, so (hidden) inconsistencies in the labels of indirectly blocked nodes
841: should not prevent a complete and clash-free tree from being satisfiable. On the
842: other hand, due to dynamic blocking, blocked nodes may become unblocked during a
843: run of the algorithm, in which case inconsistencies in these nodes may prevent
844: the discovery of a complete and clash-free tree. Consequently, for the
845: completeness proof, we require all nodes, also the blocked ones, to be free from
846: inconsistencies. Since we have not found a way to uniformly combine these two
847: different approaches into a single notion of satisfiability for completion
848: trees, we give a proof for the correctness of the \si-algorithm that does not
849: rely on Theorem~\ref{theo:generic-correctness}.
850:
851: \begin{lemma}\label{lemma:si-completeness}
852: Let $C$ be an \si-concept in NNF. If $C$ has a tableau, then the
853: expansion rules can be applied in such a way that the tableau
854: algorithm yields a complete and clash-free completion tree for $C$.
855: \end{lemma}
856:
857: \begin{proof}
858: Let $\mcT = (\mcS,\TabLab,\Edges)$ be a tableau for $C$. Using $\mcT$, we
859: guide the application of the non-deterministic \ruleor-rule such that the
860: algorithm yields a completion tree $\Tree$ that is both complete and
861: clash-free. The algorithm starts with the initial tree $\Tree$ consisting of a
862: single node $x_0$, the root, with $\BLab(x_0) = \Lab (x_0)=\{D\}$.
863:
864: $\mcT$ is a tableau, hence there is some $s_0\in \mcS$ with $D\in \TabLab
865: (s_0)$. When applying the expansion rules to $\Tree$, the application of the
866: non-deterministic \ruleor-rule is guided by the labelling in the tableau
867: $\mcT$. We will expand $\Tree$ in such a way that the following invariant
868: holds: there exists a function $\pi$ that maps the nodes of $\Tree$ to
869: elements of $\mcS$ such that
870:
871: \begin{equation}
872: \tag{$*$}
873: \begin{array}{l}
874: \Lab(x) \subseteq \TabLab (\pi(x)) \text{ holds for all nodes $x$ of \Tree,
875: and}\\
876: \text{if } \Lab \tuple x y = R \text{ then } \tuple {\pi(x)} {\pi(y)} \in
877: \Edges(R) \text{ for all nodes $x,y$ in $\Tree$}.
878: \end{array}
879: \end{equation}
880:
881: \begin{claim}
882: If $(*)$ holds for a completion tree $\Tree$ and a rule is applicable to
883: $\Tree$, then it can be applied in a way that maintains $(*)$.
884: \end{claim}
885:
886: We have to distinguish the different rules:
887: \begin{itemize}
888: \item If the \textbf{\ruleand-rule} can be applied to $x$ in $\Tree$ with $D =C_1\sqcap
889: C_2 \in \Lab(x) \subseteq \TabLab(\pi(x))$, then $C_1, C_2$ are added to
890: $\Lab(x)$. Since $\mcT$ is a tableau, $\{C_1, C_2\} \subseteq
891: \TabLab(\pi(x))$, and hence the \ruleand-rule preserves $\Lab(x) \subseteq
892: \TabLab(\pi(x))$.
893: \item If the \textbf{\ruleor-rule} can be applied to $x$ in $\Tree$ with $D =C_1\sqcup
894: C_2 \in \Lab(x) \subseteq \TabLab(\pi(x))$, then there is an $E \in
895: \{C_1,C_2\}$ such that $E \in \TabLab(\pi(x))$, and the \ruleor-rule can
896: add $E$ to $\Lab(x)$. Hence the \ruleor-rule can be applied in a way that
897: preserves $\Lab(x)\subseteq \TabLab(\pi(x))$.
898: \item If the \textbf{\ruleex-rule} can be applied to $x$ in $\Tree$ with $D =
899: \some{R}{E} \in \Lab(x) \subseteq \TabLab(\pi(x))$, then $D\in
900: \TabLab(\pi(x))$ and there is some $t\in \mcS$ with $\tuple{\pi(x)}{t}\in
901: \Edges (R)$ and $E\in \Lab(t)$. The \ruleex-rule creates a new successor $y$
902: of $x$ and we extend $\pi$ by setting $\pi' := \pi[y \mapsto t]$, i.e.,
903: $\pi'$ is the extension of $\pi$ that maps $y$ to $t$. It is easy to see
904: that the extended completion tree together with the function $\pi'$ satisfy
905: $(*)$.
906: \item If the \textbf{\rulefa-rule} can be applied to $x$ in $\Tree$ with $D = \all
907: {R}{E} \in \Lab(x) \subseteq \TabLab(\pi(x))$ and $y$ is an $R$-neighbour of
908: $x$, then $\tuple{\pi(x)}{\pi(y)} \in \Edges (R)$, and thus $E\in
909: \Lab(\pi(y))$. The \rulefa-rule adds $E$ to $\Lab(y)$ and thus preserves
910: $\Lab(x)\subseteq \TabLab(\pi(x))$. The deletion of nodes can never violate
911: $(*)$.
912: \item If the \textbf{\rulefatr-rule} can be applied to $x$ in $\Tree$ with $D = \all
913: {R}{E} \in \Lab(x) \subseteq \TabLab(\pi(x))$, $\Tr(R)$, and $y$ an
914: $R$-neighbour of $x$, then $\tuple{\pi(x)}{\pi(y)} \in \Edges (R)$, and thus
915: $\all{R}{E}\in \TabLab(\pi(y))$. The \rulefatr-rule adds $\all {R}{E}$ to
916: $\Lab(y)$ and thus preserves $\Lab(y)\subseteq \TabLab(\pi(y))$. The
917: deletion of nodes can never violate $(*)$.
918: \end{itemize}
919:
920: From this claim, the lemma can be derived as follows. It is obvious that the
921: initial tree satisfies $(*)$: since $\mcT$ is a tableau for $C$, there exists
922: an element $s_0 \in \mcS$ with $C \in \TabLab(s_0)$ and hence the function
923: $\pi$ that maps $x_0$ to $s_0$ satisfies the required properties. The claim
924: states that, whenever a rule is applicable, it can be applied in a way that
925: preserves $(*)$. Obviously, no completion tree that satisfies $(*)$
926: contains a clash as this would contradict \tab 2. Moreover, from
927: Lemma~\ref{lemma:si-termination}, we have that the expansion process terminates
928: and thus must eventually yield a complete and clash-free completion tree. \qed
929: \end{proof}
930:
931: \begin{theorem}\label{theorem:si-decision-procedure}
932: The \si-algorithm is a non-deterministic decision procedure for satisfiability
933: and subsumption of \si-concepts.
934: \end{theorem}
935:
936: \begin{proof}
937: Theorem~\ref{theorem:si-decision-procedure} is an immediate consequence of
938: Lemma~\ref{lem:si-tableau}, \ref{lemma:si-termination},
939: \ref{lemma:si-soundness}, and \ref{lemma:si-completeness}. Moreover, since \si
940: is closed under negation, subsumption of concepts $C\sqsubseteq D$ can be
941: reduced to the \mbox{(un-)}satisfiability of $C\sqcap \neg D$. \qed
942: \end{proof}
943:
944: \subsection{Complexity}
945:
946: In Lemma~\ref{lemma:si-termination} we have seen that the depths of a completion
947: tree generated by the \si-algorithm is bounded exponentially in the size of the
948: input concept. To show that the algorithm can indeed be implemented to run in
949: polynomial space, we need to carry out a closer analysis of the length of paths
950: in a completion tree.
951:
952:
953: In Lemma~\ref{lemma:si-blocking} and \ref{lemma:si-poly_paths}, we establish a
954: polynomial bound on the length of paths in the completion tree in a manner
955: similar to that used for the modal logic $\mathsf{S4}$ and $\alc_{R^+}$ in
956: \cite{HalpernMoses92,Sattler-KI-1996}. It then remains to show that such a tree can
957: be constructed using only polynomial space.
958:
959: \begin{lemma}\label{lemma:si-blocking}
960: Let $C$ be an \si-concept and $m = \sharp \textit{sub}(C)$, $n > m^3$, and
961: $R \in \overline \Roles_C$ be a role with $\Tr(R)$. Let $x_1,\dots,x_n$ be successive nodes of a
962: completion tree generated for $C$ by the \si-algorithm with
963: $\Lab\tuple{x_i}{x_{i+1}} = R$ for $1 \leq i < n$. If the \rulefa- or the
964: \rulefatr-rules cannot be applied to these nodes, then there is a blocked node
965: $x_i$ among them.
966: \end{lemma}
967:
968: \begin{proof}
969: For each node $x$ of the completion tree, $\BLab(x)$ only contains two kinds
970: of concepts: the concept that triggered the generation of the node $x$,
971: denoted by $C_x$, and concepts which were propagated \emph{down} the
972: completion tree by the first alternative of the \rulefa- or \rulefatr-rules.
973: Moreover, $\BLab(x) \subseteq \Lab(x)$ holds for any node in the completion
974: tree.
975:
976: Firstly, consider the elements of $\BLab(x_i)$ for $i\geq1$. Let $C_{x_i}$ denote
977: the concept that caused the generation of the node $x_i$. Then $\BLab(x_i) -
978: \{C_{x_i}\}$ contains only concepts which have been inserted using the
979: \rulefa- or the \rulefatr-rule. Let $D \in \BLab(x_i) - \{C_{x_i}\}$. Then
980: either $\all{R}{D} \in \Lab(x_{i-1})$ and the \rulefatr-rule makes sure that
981: $\all{R}{D} \in \BLab(x_i)$, or $D$ is already of the from $\all{R}{D'}$ and
982: has been inserted into $\BLab(x_i)$ by an application of the \rulefatr-rule to
983: $x_{i-1}$. In both cases, it follows that the \rulefa- or the \rulefatr-rule
984: yield $D \in \BLab(x_{i+1})$. Hence we have
985: \[
986: \BLab(x_i) - \{C_{x_i}\} \subseteq \BLab(x_{i+1}) \ \text{for all $1 \leq i <
987: n$},
988: \]
989: and, since we have $m$ choices for $C_{x_i}$,
990: \[
991: \sharp \{ \BLab(x_i) \mid 1 \leq i \leq n\} \leq m^2.
992: \]
993: Secondly, consider $\Lab(x_i)/\Inv(R)$. Again, the \rulefa- and the
994: \rulefatr-rules yield
995: \[
996: \Lab(x_i)/\Inv(R) \subseteq \Lab(x_{i-1})/\Inv(R) \ \text{for all $1 < i \leq
997: n$},
998: \]
999: which implies
1000: \[
1001: \sharp \{ \Lab(x_i)/\Inv(R) \mid 1 \leq i \leq n\} \leq m.
1002: \]
1003: Summing up, within $m^3+1$ nodes, there must be at least two nodes $x_j, x_k$
1004: which satisfy
1005: \[
1006: \BLab(x_j) = \BLab(x_k) \quad \text{and} \quad \Lab(x_j)/\Inv(R) =
1007: \Lab(x_k)/\Inv(R).
1008: \]
1009: This implies that one of these nodes is blocked by the other. \qed
1010: \end{proof}
1011:
1012: We will now use this lemma to give a polynomial bound on the length of paths in
1013: a completion tree generated by the completion rules.
1014:
1015: \begin{lemma}\label{lemma:si-poly_paths}
1016: The paths of a completion tree generated by the \si-algorithm for a
1017: concept $C$ have a length of at most $m^4$ where $m = \sharp \textit{sub}(C)$.
1018: \end{lemma}
1019:
1020: \begin{proof}
1021: Let $\Tree$ be a completion tree generated for $C$ by the \si-algorithm. For
1022: every node $x$ of \Tree we define $\ell(x) = \max \{ |D| \mid D \in
1023: \Lab(x)\}$. If $x$ is a predecessor of $y$ in \Tree, then this implies
1024: $\ell(x) \geq \ell(y)$. If not $\Tr(R)$ and $\Lab\tuple{x}{y} = R$, then this
1025: implies $\ell(x) > \ell(y)$. Furthermore, for $R_1 \neq R_2$ (but possibly
1026: $R_1 = \Inv(R_2)$), $\Lab\tuple{x}{y} = R_1$ and $\Lab\tuple{y}{z} = R_2$
1027: implies $\ell(x) > \ell(z)$.
1028:
1029: The only way that the maximal length of concepts does not decrease
1030: is along a pure $R$-path with $\Tr(R)$. However, the \rulefa- and
1031: the \rulefatr-rule must be applied before the \ruleex-rule may
1032: generate a new successor. Together with Lemma~\ref{lemma:si-blocking},
1033: this guarantees that these pure $R$-paths have a length of at most
1034: $m^3$.
1035:
1036: Summing up, we can have a path of length at most $m^3$ before
1037: decreasing the maximal length of the concept in the node labels (or
1038: blocking occurs), which can happen at most $m$ times and thus yields
1039: an upper bound of $m^4$ on the length of paths in a completion tree.
1040: \qed
1041: \end{proof}
1042:
1043:
1044: Note that the extra condition for the \ruleex-rule, which delays its
1045: application until no other rules are applicable, is necessary to prevent the
1046: generation of paths of exponential length. Consider the following example for
1047: some $R$ with $\Tr(R)$:
1048: %
1049: \begin{align*}
1050: C &= \some{R}{D} \sqcap \all{R}{(\some{R}{D})} \sqcap \all{R^{-1}}{A_0} \\
1051: D &= (\all{R^{-1}}{A_1} \sqcup \all{R^{-1}}{B_1}) \sqcap \dots \sqcap
1052: (\all{R^{-1}}{A_n} \sqcup \all{R^{-1}}{B_n})
1053: \end{align*}
1054:
1055: When started with a root node $x_0$ labelled $\BLab(x_0) = \Lab(x_0) = \{C\}$,
1056: the tableau algorithm generates a successor node $x_1$ with
1057: %
1058: \[\BLab(x_1) = \{ D, \exists R.D, \all{R}{(\some{R}{D})} \} \]
1059: %
1060: which, in turn, is capable of generating a further successor $x_2$ with
1061: $\BLab(x_2) = \BLab(x_1)$. Without blocking, this would lead to an infinite path
1062: in the completion tree. Obviously, for $x_1$ and $x_2$, the first part of the
1063: blocking condition is satisfied since $\BLab(x_2) \subseteq \BLab(x_1)$.
1064: However, the second condition causes a problem since, in this example, we can
1065: generate $2^n$ different sets of universal restrictions along $R^{-1}$ for each
1066: node. If we can apply the \ruleex-rule freely, then the algorithm might generate
1067: all of these $2^n$ nodes to find out that (after finally applying the
1068: \rulefatr-rule that causes propagation of the concepts of the form $\all
1069: {R^{-1}} E$ upward in the tree) within the first $n+1$ nodes on this path
1070: there is a blocked one.
1071:
1072: \begin{lemma}
1073: The \si-algorithm can be implemented in \pspace.
1074: \end{lemma}
1075:
1076: \begin{proof}
1077: Let $C$ be the \si-concept to be tested for satisfiability. We can
1078: assume $C$ to be in NNF because every \si-concept can be turned into
1079: NNF in linear time.
1080:
1081: Let $m = \sharp \textit{sub}(C)$. For each node $x$ of the completion tree,
1082: the labels $\Lab(x)$ and $\BLab(x)$ can be stored using $m$ bits for each set.
1083: Starting from the initial tree consisting of only a single node $x_0$ with
1084: $\Lab(x_0) = \BLab(x_0) = \{ D \}$, the expansion rules, as given in
1085: Figure~\ref{fig:si-rules}, are applied. If a clash is generated, then the algorithm
1086: fails and returns ``$C$ is unsatisfiable''. Otherwise, the completion tree is
1087: generated in a depth-first way: the algorithm keeps track of exactly one path
1088: of the completion tree by memorizing, for each node $x$, which of the
1089: $\some{R}{D}$-concepts in $\Lab(x)$ successors have yet to be generated. This
1090: can be done using additional $m$ bits for each node. The ``deletion'' of all
1091: successors in the \rulefa- or the \rulefatr-rule of a node $x$ is then simply
1092: realized by setting all these additional bits to ``has yet to be generated''.
1093: There are three possible results of an investigation of a child of $x$:
1094:
1095: \begin{itemize}
1096: \item A clash is detected. This stops the algorithm with ``$C$ is
1097: unsatisfiable''.
1098: \item The \rulefa- or the \rulefatr-rule leads to an increase of
1099: $\Lab(x)$. This causes reconsideration of all children of $x$,
1100: re-using the space used for former children of $x$.
1101: \item Neither of these first two cases happens. We can then forget
1102: about this subtree and start the investigation of another child
1103: of $x$. If all children have been investigated, we consider $x$'s
1104: predecessor.
1105: \end{itemize}
1106:
1107: %If it is not blocked we start to create successors for the present node, one
1108: %after the other, reusing space. We can keep track of the successors which have
1109: %already been tested, using $m$ additional bits for each node. For a newly
1110: %created successor we firstly try to apply the $\forall$- and the
1111: %$\forall_+$-rule to the present node and the successor until none of the apply
1112: %and then switch to the successor. If we find a blocked node or have considered
1113: %all necessary successor nodes, we return to the predecessor.
1114:
1115: Proceeding like this, the algorithm can be implemented using $2m +
1116: m$ bits for each node, where the $2m$ bits are used to store the two
1117: labels of the node, while $m$ bits are used to keep track of the
1118: successors already generated. Since we reuse the memory for the
1119: successors, we only have to store one path of the completion tree at
1120: a time. From Lemma~\ref{lemma:si-poly_paths}, the length of this path
1121: is bounded by $m^4$. Summing up, we can test for the existence of a
1122: completion tree using $\mathcal{O}(m^5)$ bits.
1123:
1124: Unfortunately, due to the \ruleor-rule, the \si-algorithm is a
1125: non-deterministic algorithm. However, Savitch's theorem \cite{Savitch} tells
1126: us that there is a deterministic implementation of this algorithm using at
1127: most $\mathcal{O}(m^{10})$ bits, which is still a polynomial bound. \qed
1128: \end{proof}
1129:
1130: Since \alc is a fragment of \si, satisfiability of \si-concepts is \pspace-hard,
1131: which yields:
1132:
1133: \begin{theorem}
1134: Satisfiability and subsumption of \si-concepts is \pspace-complete.
1135: \end{theorem}
1136:
1137: There is an immediate optimization of the algorithm which has been omitted for
1138: the sake of the clarity of the presentation. We have only disallowed the
1139: application of the \ruleex-rule to a blocked node, which is sufficient to
1140: guarantee the termination of the algorithm. It is also possible to disallow the
1141: application of more rules to a blocked node without violating the soundness or
1142: the completeness of the algorithm, if the notion of blocking is slightly
1143: adapted. It then becomes necessary to distinguish directly and indirectly
1144: blocked nodes. More details can be found in~\cite{HorrocksSattler-DL-1998}. The
1145: technique presented there will stop the expansion of a blocked node earlier
1146: during the runtime of the algorithm and hence will save some work.
1147:
1148: %%% Local Variables:
1149: %%% mode: latex
1150: %%% TeX-master: "main"
1151: %%% End:
1152: