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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Boris Motik, Ian Horrocks
• Keywords: Automated Reasoning, CADE 2008, Certain Knowledge Bases, Description Logics, Worst-case Optimal Algorithm