一句话：研究 EL 描述逻辑中带负约束的去合一问题，证明 dismatching 与局部可解性为 NP 完全。
描述逻辑中的合一是检测本体冗余的重要手段，而负约束可用于排除不期望的合一子，因此有必要研究去合一。一般 EL 去合一问题的可解性仍开放。本文针对两个特殊情况给出 NP 完全性结果：dismatching，要求每个负约束的一侧为 ground；以及去合一问题的局部可解性，即仅考虑由输入问题中出现的项构造的解。方法上，作者先将 dismatching 归约到局部去合一，然后提出两个互补的 NP 算法来寻找局部解，从而建立相应复杂度上界，并结合下界得到 NP 完全性。结果表明，尽管一般情形未决，这些受限形式仍可有效判定。
Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic $\mathcal{EL}$ to disunification since negative constraints can be used to avoid unwanted unifiers. While decidability of the solvability of general $\mathcal{EL}$-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we consider only solutions that are constructed from terms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of disunification problems.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BaaderBM16,
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 = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:1)2016}
}