Terminology

This is the Subgraph of a Semantic Network spanned by the isa links and relations between concepts.

Usually you want to have a small TBox that is really precise. Because Inference is done on the TBox and not on the ABox. The ABox may contain a LOT of objects.

A TBox is called acyclic when it does not contain recursive concept definitions.

A formula is called normalized with respect to a TBox iff it does not contain concepts defined in $\mathcal{T}$. So we can use concept definitions to normalize a formula back to its original properties by substituting $c$ by $C$. For acyclic TBoxes this normalization will termintate but results can get exponentially large.