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.

翻译：限定摹状词是形如“满足性质C的唯一x”的表达式，允许通过对象的区分性特征来指称对象。它们在本体论和查询语言中扮演着关键角色，为缺乏语义内容、仅作为占位符使用的专有名称（ID）提供了一种替代方案。本文在著名的描述逻辑ALC基础上，引入了局部和全局两类限定摹状词的扩展，分别记为ALCιL和ALCιG。我们为这些逻辑定义了适当的互模拟概念，从而能够分析其表达能力。我们证明，尽管两种逻辑在概念和本体可满足性上具有相同的紧致ExpTime复杂度界限，但ALCιG的表达能力严格强于ALCιL。此外，我们为两种逻辑的可满足性问题提出了基于表推演（tableau）的判定过程，提供了其实现，并报告了一系列实验。实证结果表明该实现具有实际效用，并揭示了性能与输入公式结构特性之间有趣的相关性。