Past exam of the computer science course of the University of Oxford / 2015 / Knowledge representation and reasoning / 2 / b / Solution

Use the substitution version of TBox unfolding from part (a), and abbreviateThe notation $\overline{L}$ is the negation normal form of $\neg L$. The unfolded input description logic concept isFor the remaining TBox, turn each general concept inclusion $X⊑Y$ into $\neg X\bigsqcup Y$, and unfold all defined names. The global description logic concept to add at every generated node isIn the last line, negating $\exists R.(\exists R.A\bigsqcup \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^{\prime }$ 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 isThere 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.

A concrete model confirms the open branch: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}}$.