Non-Rigid Designators in Epistemic and Temporal Free Description Logics (Extended Version)

TL;DR

This paper extends description logics with definite descriptions, allowing non-rigid and possibly non-denoting terms, and analyzes the computational complexity of their satisfiability in epistemic and temporal contexts.

Contribution

It introduces epistemic and temporal description logics with non-rigid and partial descriptions, and studies their decidability and complexity.

Findings

Satisfiability in epistemic free description logics is NExpTime-complete.

Satisfiability in temporal free description logics over linear time is undecidable.

The framework generalizes standard description logics with non-rigid and partial descriptions.

Abstract

Definite descriptions, such as 'the smallest planet in the Solar System', have been recently recognised as semantically transparent devices for object identification in knowledge representation formalisms. Along with individual names, they have been introduced also in the context of description logic languages, enriching the expressivity of standard nominal constructors. Moreover, in the first-order modal logic literature, definite descriptions have been widely investigated for their non-rigid behaviour, which allows them to denote different objects at different states. In this direction, we introduce epistemic and temporal extensions of standard description logics, with nominals and the universal role, additionally equipped with definite descriptions constructors. Regarding names and descriptions, in these languages we allow for: possible lack of denotation, ensured by partial models, coming from free logic semantics as a generalisation of the classical ones; and non-rigid designation features, obtained by assigning to terms distinct values across states, as opposed to the standard rigidity condition on individual expressions. In the absence of the rigid designator assumption, we show that the satisfiability problem for epistemic free description logics is NExpTime-complete, while satisfiability for temporal free description logics over linear time structures is undecidable.