= Solution
Use the substitution version of <TBox unfolding> from part (a), and abbreviate
$$
L=A_0\sqcap\neg B,\qquad \overline L=\neg A_0\sqcup B.
$$
The notation $\overline L$ is the <negation normal form> of $\neg L$. The unfolded input <description logic concept> is
$$
\boxed{D'=L\sqcap\forall R.(L\sqcap B).}
$$
For the remaining <TBox>, turn each <general concept inclusion> $X\sqsubseteq Y$ into $\neg X\sqcup Y$, and unfold all defined names. The global <description logic concept> to add at every generated node is
$$
\boxed{\begin{aligned}
\Gamma=C_{\mathcal T_g}'={}&\forall R.\exists P.\top\\
&\sqcap(\forall R.\overline L\sqcup\exists R.\exists R.L)\\
&\sqcap\bigl(\forall R.(\forall R.\overline L\sqcap\forall R.\neg B)\sqcup\forall R.L\bigr).
\end{aligned}}
$$
In the last line, negating $\exists R.(\exists R.A\sqcup\exists R.B)$ gives $\forall R.(\forall R.\neg A\sqcap\forall R.\neg B)$. Both levels of universal restriction are needed.
Start the <tableau algorithm for ALC> with a root $x$ labelled $D'$ and $\Gamma$. Expand the <logical conjunctions>. For the disjunction from (2), choose $\forall R.\overline L$. For the disjunction from (3), choose $\forall R.L$. Apart from the compound formulas already processed, the root label is
$$
\mathcal L(x)=\{A_0,\neg B,\forall R.(L\sqcap B),\forall R.\exists P.\top,\forall R.\overline L,\forall R.L\}.
$$
There is no existential restriction at $x$, so no successor needs to be generated. In particular, $\forall R.\exists P.\top$ creates a $P$-successor only at an existing $R$-successor; it creates no $R$-successor itself. The branch is complete and has no <tableau clash>. There is $\boxed{\text{no directly blocked node}}$: the open completion graph has only its root. The universal restrictions can have incompatible fillers without creating a <tableau clash> when there are no successors.
For comparison, choosing the other alternative $\exists R.\exists R.L$ from (2) creates an $R$-successor $y$. The root restriction $\forall R.(L\sqcap B)$ puts $A_0,\neg B,B$ in $\mathcal L(y)$, giving a <tableau clash> immediately. That branch closes before <direct blocking in description logic> is needed. The figure records the processed formulas through the label $\Gamma$ and displays the decisive labels explicitly.
\Image[/past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/knowledge-representation-2015-tableau.png]
{title=An open one-node completion and the closed alternative; neither branch contains a directly blocked node}
A concrete model confirms the open branch:
$$
\boxed{\Delta^{\mathcal I}=\{d\},\quad A^{\mathcal I}=\{d\},\quad B^{\mathcal I}=C^{\mathcal I}=\varnothing,\quad R^{\mathcal I}=P^{\mathcal I}=\varnothing.}
$$
All three remaining <general concept inclusions> hold because their relevant $R$-successor requirements are vacuous. The definition of $C$ and the disjointness condition hold as well. Thus $\boxed{D\text{ is satisfiable with respect to }\mathcal T}$.
Back to article page
