将 $\mathcal{EL}$ 中的统一扩展到非统一：不匹配与局部非统一的情形
计算机科学中的逻辑
2019-03-14 v2 人工智能
摘要
描述逻辑中的统一已被引入作为一种检测本体中冗余的手段。我们尝试将描述逻辑 中统一的已知可判定性结果扩展到非统一，因为负约束可用于避免不需要的统一子。虽然一般 -非统一问题可解性的可判定性仍然是一个未决问题，但我们在两个有趣的特例中获得了 NP-完全性结果：不匹配问题，其中每个负约束的一侧必须是基项；以及非统一问题的局部可解性，其中我们仅考虑由输入问题中出现的项构成的解。更具体地说，我们首先证明不匹配可以归约为局部非统一，然后提供了两种互补的 NP 算法用于寻找非统一问题的局部解。
引用
@article{arxiv.1609.05621,
title = {Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification},
author = {Franz Baader and Stefan Borgwardt and Barbara Morawska},
journal= {arXiv preprint arXiv:1609.05621},
year = {2019}
}
备注
32 pages, extended version of a paper from RTA'15