Unification in the Description Logic EL
Unification in the Description Logic EL
复制标题
描述逻辑EL的统一
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Barbara Morawska
中科院分区：
文献类型：
--
作者：
F. Baader;Barbara Morawska
描述逻辑$数学{EL}$最近引起了相当大的关注，因为，一方面，重要的推理问题，如包含问题，是多项式的。另一方面，$mathcal{EL}$用于定义大型生物医学本体。描述逻辑中的统一性已经被提出作为一种新的推理服务，例如，可以用于检测本体中的冗余。本文的主要结果是：$数学{EL}$中的统一是可判定的。更准确地说，$数学{EL}$-合一是NP-完全的，因此具有与$数学{EL}$-匹配相同的复杂性。我们也展示了这一点，W.r.t.统一类型$mathcal{EL}$表现不太好：它的类型为零，这特别意味着存在没有有限完整的统一集的统一问题。
The Description Logic $mathcal{EL}$ has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, $mathcal{EL}$ is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in $mathcal{EL}$ is decidable. More precisely, $mathcal{EL}$-unification is NP-complete, and thus has the same complexity as $mathcal{EL}$-matching. We also show that, w.r.t. the unification type, $mathcal{EL}$ is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.