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.
翻译:定描述词(如“KR 2024 大会主席”)是知识表示中一种语义透明的对象识别手段。在一阶模态逻辑中,定描述词因其非刚性而得到广泛研究,这使得它们能够在不同状态下指称不同的对象(或不指称任何对象)。我们提出了包含非刚性定描述词与名称的表达性模态描述逻辑,并研究了其可满足性问题的可判定性与计算复杂度。我们首先系统地将带计数的一阶模态逻辑单变元片段的可满足性问题与我们的模态描述逻辑相关联。随后,我们针对基本的多主体认知逻辑 $\mathbf{S5}^{n}$ 及其邻近逻辑,证明了概念可满足性问题具有前景广阔的 NEXPTIME 完全性结果,并证明某些在恒定域下不可判定的表达性逻辑在扩张域下可判定(但具有阿克曼难度)。最后,我们对时态逻辑的可判定性进行了细粒度分析。