模态和描述逻辑的统一和容许问题的不确定性
Undecidability of the unification and admissibility problems for modal and description logics
摘要：
我们表明，统一问题`是否有一个替代实例的一个给定的公式，是证明在一个给定的逻辑？对于用泛模态扩充的基本模态逻辑K和K_4，因此，推理规则的容许性问题对于这些逻辑也是不可判定的。这些是标准可判定模态逻辑的第一个例子，其中统一和容许问题是不可判定的。我们还证明了不可判定性的统一和容许问题的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 logic with transitive roles, inverse roles, and role hierarchies (such as SHI and SHIQ).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
