Individual Reuse in Description Logic Reasoning.

Journal article

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. © 2008 Springer-Verlag Berlin Heidelberg.

Authors: Motik, B; Horrocks, I

• Publication status: Published
• Publisher: Springer
• Journal: IJCAR
• Volume: 5195
• Pages: 242-258
• Publication date: 2008-01-01
• DOI: 10.1007/978-3-540-71070-7_20
• EISSN: 1611-3349
• ISSN: 0302-9743
• Language: English