TBox ($\mathcal{T}$)

A collection of terminological axioms, including general concept inclusions, constraining the meanings of description logic concepts and description logic roles.

Rewriting suitable general axioms into definitions or primitive inclusions that can be processed when an atomic label is encountered. For example, $A\sqcap B⊑\perp$ can be absorbed as $A⊑\neg B$.

Substitution of acyclic concept definitions into expressions to be tested. Primitive inclusions require care: $A⊑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$.