On Free Description Logics with Definite Descriptions

TL;DR

This paper extends basic description logics with definite descriptions, showing reasoning complexity remains manageable, characterizing their expressive power, and laying groundwork for automated description generation.

Contribution

It introduces free description logics with definite descriptions, analyzes their reasoning complexity, and establishes foundations for automated description generation.

Findings

Reasoning complexity remains similar to original languages.

Characterization of expressive power via bisimulation.

Polynomial-time reduction for reasoning in related logics.

Abstract

Definite descriptions are phrases of the form 'the $x$ such that $\varphi$', used to refer to single entities in a context. They are often more meaningful to users than individual names alone, in particular when modelling or querying data over ontologies. We investigate free description logics with both individual names and definite descriptions as terms of the language, while also accounting for their possible lack of denotation. We focus on the extensions of $\mathcal{ALC}$ and, respectively, $\mathcal{EL}$ with nominals, the universal role, and definite descriptions. We show that standard reasoning in these extensions is not harder than in the original languages, and we characterise the expressive power of concepts relative to first-order formulas using a suitable notion of bisimulation. Moreover, we lay the foundations for automated support for definite descriptions generation by studying the complexity of deciding the existence of definite descriptions for an individual under an ontology. Finally, we provide a polynomial-time reduction of reasoning in other free description logic languages based on dual-domain semantics to the case of partial interpretations.