Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909947583791104 |
|---|---|
| author | Sochański, Michał Wałęga, Przemysław Andrzej Zawidzki, Michał |
| author_facet | Sochański, Michał Wałęga, Przemysław Andrzej Zawidzki, Michał |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_06604 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction Sochański, Michał Wałęga, Przemysław Andrzej Zawidzki, Michał Logic in Computer Science 03B70, 03B60, 03B35, 68T27 I.2.4; I.2.3; F.4.3; D.3.1 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. |
| title | Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction |
| topic | Logic in Computer Science 03B70, 03B60, 03B35, 68T27 I.2.4; I.2.3; F.4.3; D.3.1 |
| url | https://arxiv.org/abs/2512.06604 |