= Solution
Absorb (4) using the equivalence
$$
A\sqcap B\sqsubseteq\bot\quad\Longleftrightarrow\quad A\sqsubseteq\neg B.
$$
Thus we can take
$$
\boxed{\mathcal T_u=\{C\equiv\exists P.\top,\ A\sqsubseteq\neg B\},\qquad \mathcal T_g=\{(1),(2),(3)\}.}
$$
Here $A\sqsubseteq\neg B$ is a primitive inclusion, handled by adding $\neg B$ whenever $A$ labels a node. For literal substitution-based <TBox unfolding>, introduce a fresh <description logic concept> $A_0$ and replace the primitive inclusion by
$$
A\equiv A_0\sqcap\neg B.
$$
This preserves the original models after forgetting $A_0$: any model of the primitive inclusion extends by taking $A_0=A$, and any model of the new definition satisfies the primitive inclusion. The fresh name is important. Replacing $A$ by $\neg B$ alone would incorrectly assert that every non-$B$ element is an $A$ element.
Back to article page
