Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction

Definite descriptions are expressions of the form "the unique $x$ satisfying property $C$," which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an alternative to proper names (IDs), which lack semantic content and serve merely as placeholders. In this paper, we introduce two extensions of the well-known description logic $\mathcal{ALC}$ with local and global definite descriptions, denoted $\mathcal{ALC}ι_L$ and $\mathcal{ALC}ι_G$, respectively. We define appropriate bisimulation notions for these logics, enabling an analysis of their expressiveness. We show that although both logics share the same tight ExpTime complexity bounds for concept and ontology satisfiability, $\mathcal{ALC}ι_G$ is strictly more expressive than $\mathcal{ALC}ι_L$. Moreover, we present tableau-based decision procedures for satisfiability in both logics, provide their implementation, and report on a series of experiments. The empirical results demonstrate the practical utility of the implementation and reveal interesting correlations between performance and structural properties of the input formulas.