= Solution
Using the absorbed <TBox> with its primitive inclusion, translate <description logic concepts> as unary predicates and <description logic roles> as binary predicates. <Concept satisfiability> means that some element belongs to $A\sqcap C$, while every element satisfies the <TBox> axioms. The required <first-order sentence> is
$$
\boxed{\begin{aligned}
&\exists x\,(A(x)\land C(x))\\
{}\land{}&\forall u\,(A(u)\to\neg B(u))\\
{}\land{}&\forall u\,\bigl(C(u)\leftrightarrow\exists v\,P(u,v)\bigr).
\end{aligned}}
$$
Only $\mathcal T_u$ is included here, as requested. There is no requirement to satisfy (1), (2) or (3). For instance, one element with $A=C=\{d\}$, $B=\varnothing$ and $P=\{(d,d)\}$ satisfies this <first-order sentence>.
Alternatively, unfolding the absorbed <TBox> first gives the existential <first-order sentence> $\exists x\exists y\,(A_0(x)\land\neg B(x)\land P(x,y))$. The interpretation of the eliminated names is then recovered by $A=A_0\setminus B$ and $C=\{x:\exists y\,P(x,y)\}$.
Back to article page
