Undecidability of the unification and admissibility problems for modal and description logics
Undecidability of the unification and admissibility problems for modal and description logics
复制标题
模态逻辑和描述逻辑的统一性和可接受性问题的不可判定性
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
F. Wolter;M. Zakharyaschev
我们证明了统一问题“是否存在在给定逻辑中可证明的给定公式的替换实例？”对于用通用模态扩展的基本模态逻辑 K 和 K4 是不可判定的。由此可见，推理规则的可接受性问题对于这些逻辑来说也是不可判定的。这些是标准可判定模态逻辑的第一个例子，其中统一性和可接受性问题是不可判定的。我们还证明了具有至少两个模态算子和名词（而不是通用模态）的 K 和 K4 的统一和可接受性问题的不可判定性，从而表明这些问题对于基本混合逻辑是不可判定的。最近，统一被引入作为描述逻辑的重要推理服务。 K 与名词的不可判定性证明可以用来证明布尔描述逻辑与名词（如 ALCO 和 SHIQO）统一的不可判定性。具有通用模态的 K 的不可判定性证明可以用来表明，对于具有传递角色、逆角色和角色层次结构（例如 SHI 和 SHIQ）的布尔描述逻辑，与角色框相关的统一问题是不可判定的。
We show that the unification problem “is there a substitution instance of a given formula that is provable in a given logic?” is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem for inference rules is undecidable for these logics as well. These are the first examples of standard decidable modal logics for which the unification and admissibility problems are undecidable. We also prove undecidability of the unification and admissibility problems for K and K4 with at least two modal operators and nominals (instead of the universal modality), thereby showing that these problems are undecidable for basic hybrid logics. Recently, unification has been introduced as an important reasoning service for description logics. The undecidability proof for K with nominals can be used to show the undecidability of unification for Boolean description logics with nominals (such as ALCO and SHIQO). The undecidability proof for K with the universal modality can be used to show that the unification problem relative to role boxes is undecidable for Boolean description logics with transitive roles, inverse roles, and role hierarchies (such as SHI and SHIQ).