Description Logic TBoxes: Model-theoretic Characterizations and Rewritability

TL;DR

This paper provides semantic characterizations of the expressive power of various description logic TBoxes, enabling analysis of their rewritability into simpler DL fragments through model-theoretic notions.

Contribution

It introduces model-theoretic characterizations for DL TBoxes across different expressive levels, facilitating the study of their rewritability into lightweight DLs.

Findings

Characterizations based on bisimulation and related notions

Decidability results for TBox rewritability

Framework applicable to both expressive and lightweight DLs

Abstract

We characterize the expressive power of description logic (DL) TBoxes, both for expressive DLs such as ALC and ALCQIO and lightweight DLs such as DL-Lite and EL. Our characterizations are relative to first-order logic, based on a wide range of semantic notions such as bisimulation, equisimulation, disjoint union, and direct product. We exemplify the use of the characterizations by a first study of the following novel family of decision problems: 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.