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

TL;DR

This paper introduces two extensions of description logic with definite descriptions, analyzes their expressiveness and complexity, and provides tableau-based decision procedures with empirical evaluation.

Contribution

It defines local and global definite descriptions in description logic, compares their expressiveness and complexity, and develops practical decision procedures with experimental validation.

Findings

Both logics have ExpTime complexity for satisfiability.

Global definite descriptions are more expressive than local ones.

Empirical results show practical utility and performance correlations.

Abstract

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}\iota_L$ and $\mathcal{ALC}\iota_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}\iota_G$ is strictly more expressive than $\mathcal{ALC}\iota_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.