Hypertableau Reasoning for Description Logics
Hypertableau Reasoning for Description Logics
复制标题
DOI：
10.1613/jair.2811
复制
发表时间：
2009-01-01
影响因子：
5
通讯作者：
Horrocks, Ian
中科院分区：
文献类型：
--
作者：
Motik, Boris;Shearer, Rob;Horrocks, Ian
我们为描述逻辑shoiq（+）提供了一种新颖的推理演算 - 一种知识表示形式主义，其应用在语义网等领域。不必要的非确定性和大型模型的构建是在最先进的推理者中使用的基于图表的推理的两个主要来源。为了减少非确定性，我们将演算基于Hypertableau和Hypertableau和高分辨率结石，我们以阻塞条件扩展，以确保终止。为了减少构造模型的大小，我们引入了成对阻塞的任何位置。我们还提出了一项改进的名义介绍规则，该规则确保在存在名义，反向作用和数量限制的情况下终止 - DL构建体的组合被证明很难处理。我们的实施显示了几个知名本体论的最先进的推理者的绩效改善。
We present a novel reasoning calculus for the description logic SHOIQ(+)-a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce any where pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions-a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.