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 . So we can use concept definitions to normalize a formula back to its original properties by substituting by . For acyclic TBoxes this normalization will termintate but results can get exponentially large.
