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 完全性结果,并表明一些在常域下不可判定的表达性逻辑在扩张域下变得可判定(但具有 Ackermann 难度)。最后,我们对时间逻辑的可判定性进行了细粒度分析。