模态与时间自由描述逻辑中的非严格指示词(扩展版)
Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)
AI总结:
本研究提出带非严格限定摹状词与名称的模态描述逻辑,关联一阶模态逻辑单变量片段可满足性,证明$\n mathbf{S5}^{n}$等逻辑概念可满足性为NEXPTIME完全,还分析了时态逻辑可判定性。
摘要:
限定摹状词(如“KR 2024的大会主席”)是知识表示中用于对象识别的语义透明机制。在一阶模态逻辑中,限定摹状词的非严格性已被广泛研究,这一特性允许它们在不同状态下指示不同对象(或不指示任何对象)。我们提出了带有非严格限定摹状词和名称的表达性模态描述逻辑,并研究了可满足性问题的可判定性与复杂度。我们首先系统地将带计数的一阶模态逻辑单变量片段的可满足性与我们的模态描述逻辑关联起来。随后,我们证明了基础认知多智能体逻辑$\n mathbf{S5}^{n}$及其邻近逻辑的概念可满足性具有NEXPTIME完全性这一颇具前景的结果,并表明一些在常论域下不可判定的表达性逻辑在论域扩张时变得可判定(但具有Ackermann难度)。最后,我们对时态逻辑的可判定性进行了细粒度分析。
英文摘要:
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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。