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

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.