Description Logic TBoxes: Model-theoretic Characterizations and Rewritability
Carsten Lutz, Robert Piro and Frank Wolter
We characterize the expressive power of description logic (DL) TBoxes relative to first-order logic, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. The characterizations are based on a wide range of semantic notions such as bisimulation, equisimulation, disjoint union, and direct product. We demonstrate their usefulness by a first study of the following novel family of decision problems, closely related to TBox approximation: given a TBox T formulated in a DL L, decide whether T can be equivalently rewritten as a TBox in the fragment L' of L. For example, we consider the case where L is the expressive, but computationally costly DL ALC while L' is the less expressive, but tractable DL EL.