TBox unfolding
= TBox unfolding
{c}
Substitution of acyclic concept definitions into expressions to be tested. Primitive inclusions require care: $A\sqsubseteq D$ can be represented using a fresh name $A_0$ by $A\equiv A_0\sqcap D$, but is not equivalent to $A\equiv D$.