Individual Reuse in Description Logic Reasoning

9 years 3 months ago
Individual Reuse in Description Logic Reasoning
Abstract. Tableau calculi are the state-of-the-art for reasoning in description logics (DL). Despite recent improvements, tableau-based reasoners still cannot process certain knowledge bases (KBs), mainly because they end up building very large models. To address this, we propose a tableau calculus with individual reuse: to satisfy an existential assertion, our calculus nondeterministically tries to reuse individuals from the model generated thus far. We present two expansion strategies: one is applicable to the DL ELOH and gives us a worst-case optimal algorithm, and the other is applicable to the DL SHOIQ. Using this technique, our reasoner can process several KBs that no other reasoner can.
Boris Motik, Ian Horrocks
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Boris Motik, Ian Horrocks
Comments (0)