Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Michał Sochański, Przemysław Andrzej Wałęga, Michał Zawidzki

TL;DR

This work introduces three extensions of the description logic ALC to support two types of definite descriptions: local (ALCι_L) and global (ALCι_G), with a combined form (ALCι). It develops novel bisimulation concepts to analyze expressiveness, shows ExpTime-complete satisfiability for all three, and proves that ALCι_L is strictly less expressive than ALCι_G, while ALCι_G and ALCι are equally expressive. Tableau-based decision procedures are provided for all three logics, and an implementation along with experiments demonstrates the practical feasibility and informs performance trends related to the presence and structure of definite descriptions. Overall, the paper advances both the theoretical understanding and practical tooling for reasoning with definite descriptions in Description Logics.

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}ι_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.

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

TL;DR

This work introduces three extensions of the description logic ALC to support two types of definite descriptions: local (ALCι_L) and global (ALCι_G), with a combined form (ALCι). It develops novel bisimulation concepts to analyze expressiveness, shows ExpTime-complete satisfiability for all three, and proves that ALCι_L is strictly less expressive than ALCι_G, while ALCι_G and ALCι are equally expressive. Tableau-based decision procedures are provided for all three logics, and an implementation along with experiments demonstrates the practical feasibility and informs performance trends related to the presence and structure of definite descriptions. Overall, the paper advances both the theoretical understanding and practical tooling for reasoning with definite descriptions in Description Logics.

Abstract

Definite descriptions are expressions of the form "the unique satisfying property ," 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 with local and global definite descriptions, denoted and , 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, is strictly more expressive than . 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.

Paper Structure

This paper contains 10 sections, 13 theorems, 33 equations, 3 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Description Logics with Definite Descriptions
  3. Syntax
  4. Semantics
  5. Expressiveness and Complexity
  6. Tableaux Systems
  7. Implementation and Experiments
  8. Generator
  9. Experiments and results
  10. Conclusions

Key Result

Theorem 1

In $\mathcal{ALC}\iota_L$, $\mathcal{ALC}\iota_G$, and $\mathcal{ALC}\iota$, both concept and ontology satisfiability are $\textsc{ExpTime}$-complete.

Figures (3)

  • Figure 1: Maximal $\mathcal{ALC}\iota_L$ bisimulation between $\mathcal{I}$ and $\mathcal{J}$
  • Figure 2: Rules of $\mathtt{TAB}_{\mathcal{ALC}\iota}$
  • Figure 3: Runtimes for concepts with only GDs, only LDs, and without DDs; dashed lines represent average runtimes

Theorems & Definitions (40)

  • Theorem 1
  • proof : Proof sketch
  • Proposition 2
  • proof : Proof sketch
  • Definition 3
  • Example 4
  • Definition 5
  • Theorem 6
  • proof : Proof sketch
  • Theorem 7
  • ...and 30 more