Consequence-Based Reasoning for Description Logics with Disjunctions and Number Restrictions
Consequence-Based Reasoning for Description Logics with Disjunctions and Number Restrictions
复制标题
DOI：
10.1613/jair.1.11257
复制
发表时间：
2018-11
期刊：
影响因子：
--
通讯作者：
A. Bate;B. Motik;B. C. Grau;David Tena Cucala;F. Simančík;Ian Horrocks
中科院分区：
文献类型：
--
作者：
A. Bate;B. Motik;B. C. Grau;David Tena Cucala;F. Simančík;Ian Horrocks
描述逻辑（DL）本体的分类是现代数据管理应用程序中的关键计算问题，因此已大量努力致力于实用推理的开发和优化。基于后果的微积分将Hypertableau的思想和解决方案结合在一起，在实践中被证明非常有效。但是，现有的基于后果的微积分可以处理无限制的HORN DLS（不支持分离）或DLS。在本文中，我们克服了这一重要局限性，并提出了决定DL Alchiq+中概念包含的第一个基于结果的演算。我们的演算在指数时间内运行，假设数字的一致编码，并且在多项式时间内运行的ELH本体。在技术上涉及分离和数字限制的扩展：我们使用一阶子句捕获相关后果，而我们的推理规则适应了一阶定理证明的适应性偏差技术。通过使用众所周知的预处理步骤，微积分还可以决定SRIQ中的概念子弹出---富含DL，涵盖了OWL 2 DL的所有功能，除了标称和数据型。我们已经在称为红杉的新原因中实现了微积分。我们介绍了推理者的体系结构，并讨论了几种新颖而重要的实施技术，例如子句索引和冗余消除。最后，我们介绍了广泛的绩效评估的结果，该评估表明红杉与现有推理者具有竞争力。因此，我们在本文中提出的微积分和技术为描述逻辑推理的实际实施技术提供了重要的补充。
Classification of description logic (DL) ontologies is a key computational problem in modern data management applications, so considerable effort has been devoted to the development and optimisation of practical reasoning calculi. Consequence-based calculi combine ideas from hypertableau and resolution in a way that has proved very effective in practice. However, existing consequence-based calculi can handle either Horn DLs (which do not support disjunction) or DLs without number restrictions. In this paper, we overcome this important limitation and present the first consequence-based calculus for deciding concept subsumption in the DL ALCHIQ+. Our calculus runs in exponential time assuming unary coding of numbers, and on ELH ontologies it runs in polynomial time. The extension to disjunctions and number restrictions is technically involved: we capture the relevant consequences using first-order clauses, and our inference rules adapt paramodulation techniques from first-order theorem proving. By using a well-known preprocessing step, the calculus can also decide concept subsumptions in SRIQ---a rich DL that covers all features of OWL 2 DL apart from nominals and datatypes. We have implemented our calculus in a new reasoner called Sequoia. We present the architecture of our reasoner and discuss several novel and important implementation techniques such as clause indexing and redundancy elimination. Finally, we present the results of an extensive performance evaluation, which revealed Sequoia to be competitive with existing reasoners. Thus, the calculus and the techniques we present in this paper provide an important addition to the repertoire of practical implementation techniques for description logic reasoning.