模态逻辑与描述逻辑统一问题与可接受性问题的不可判定性
计算机科学中的逻辑
2007-05-23 v1 人工智能
摘要
我们证明，统一问题（是否存在给定公式的替换实例可在给定逻辑中证明）对以普遍模态扩展的基本模态逻辑K和K4是不可判定的。这意味着这些逻辑下推理规则的可接受性问题也是不可判定的。这都是首个具有标准可判定性模态逻辑，其中统一和可接受性问题均不可判定的例子。我们还证明了对于K和K4（使用至少两种模态算子和名词，而非普遍模态）的统一和可接受性问题也是不可判定的，从而表明这些问题对基本混合逻辑也是不可判定的。最近，统一问题被引入作为描述逻辑的重要推理服务。K带名词的不可判定性证明可用于显示以名词（如ALCO和SHIQO）的布尔描述逻辑的统一问题不可判定。K带普遍模态的不可判定性证明可用于显示以角色框（如SHI和SHIQ）的布尔描述逻辑的统一问题不可判定，该描述逻辑包含传递角色、逆向角色和角色层次结构。
引用
@article{arxiv.cs/0609052,
title = {Undecidability of the unification and admissibility problems for modal and description logics},
author = {Frank Wolter and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:cs/0609052},
year = {2007}
}