Consequence-based and fixed-parameter tractable reasoning in description logics
详细信息 查看全文
- 作者：Franti拧ek Siman膷铆k ; Boris Motik ; Ian Horrocks
- 关键词：Description logics ; Parameterized complexity ; Treewidth
- 刊名：Artificial Intelligence
- 出版年：April, 2014
- 年：2014
- 卷：209
- 期：Complete
- 页码：29-77
- 全文大小：1233 K
文摘
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鈥攁 graph-like structure that, roughly speaking, summarizes the models relevant during ontology reasoning. We identify width and length as decomposition parameters that determine the 鈥渓evel鈥?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.