Consequence-based and fixed-parameter tractable reasoning in description logics

作     者：Simancik, Frantisek Motik, Boris Horrocks, Ian 

作者机构：Univ Oxford Dept Comp Sci Oxford OX1 2JD England 

出 版 物：《ARTIFICIAL INTELLIGENCE》 (Artif Intell)

年 卷 期：2014年第209卷第1期

页      面：29-77页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：EPSRC [EP/L012138/1  EP/H051511/1  EP/K00607X/1  EP/G02085X/1] Funding Source: UKRI 

主　　题：Description logics Parameterized complexity Treewidth 

摘      要：In this paper we investigate the consequence-based algorithms that are nowadays commonly used for subsumption reasoning with description logic ontologies, presenting the following novel results. First, we present a very general consequence-based reasoning algorithm that can be instantiated so as to capture the essential features of the known algorithms. Second, we use this algorithm to develop a novel framework for a quantitative and parametric analysis of the complexity of subsumption reasoning in description logic ontologies. Our approach is based on the notion of a decomposition a graph-like structure that, roughly speaking, summarizes the models relevant during ontology reasoning. We identify width and length as decomposition parameters that determine the level of combinatorial reasoning. We prove that, when parameterized by a decomposition, our consequence-based algorithm runs in time that is fixed-parameter tractable in width and length. Third, we briefly discuss how length and width characterize the behavior of tableau algorithms. Fourth, we show that the width and length of existing ontologies are reasonably small, which, we believe, explains the good performance of consequence-based algorithms in practice. We thus obtain a sound foundation for a practical implementation of ontology reasoners, as well as a way to analyze the reasoners performance. (C) 2014 Elsevier B.V. All rights reserved.