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

TL;DR

The paper develops modalised free description logics with non-rigid definite descriptions and names, and systematically analyzes satisfiability/decidability across constant and expanding domains in both modal and temporal settings. It builds a network of reductions linking modal DL satisfiability to first-order modal logics with counting, proves NExpTime upper bounds for core logics like ${\mathbf{S5}}^{n}$ and its neighbors, and identifies where expanding-domain semantics restore decidability or create hardness (Ackermann-hard) for various expressive logics, including ${\mathbf{K}}^{n}$, ${\mathbf{K_f}^{*n}}$, and temporal fragments. The work introduces technical tools like normal forms, spy-points, nominals/definite-descriptions translations, and quasimodels to obtain exponential-size model properties and to transfer results between different semantic settings. It also offers strong links between non-rigid designators and counting via the ${\mathcal{ML}}_{\text{Diff}}^{n}$ logic, enabling cross-pollination of decidability results between modal DLs and first-order modal logics. The findings advance understanding of the boundary between decidability and intractability in expressive modal/temporal DLs, with implications for ontology-based knowledge representation in dynamic and epistemic domains.

Abstract

Definite descriptions, such as 'the General Chair of KR 2024', are a semantically transparent device for object identification in knowledge representation. In first-order modal logic, definite descriptions have been widely investigated for their non-rigidity, which allows them to designate different objects (or none at all) at different states. We propose expressive modal description logics with non-rigid definite descriptions and names, and investigate decidability and complexity of the satisfaction problem. We first systematically link satisfiability for the one-variable fragment of first-order modal logic with counting to our modal description logics. Then, we prove a promising NEXPTIME-completeness result for concept satisfiability for the fundamental epistemic multi-agent logic $\mathbf{S5}^{n}$ and its neighbours, and show that some expressive logics that are undecidable with constant domain become decidable (but Ackermann-hard) with expanding domains. Finally, we conduct a fine-grained analysis of decidability of temporal logics.

Theorems & Definitions (90)

• Remark 1: Encoding of assertions
• Proposition 0
• Proposition 0
• Proposition 0
• Lemma 0
• Lemma 0
• Lemma 0
• Proposition 0
• Proposition 0
• Proposition 0