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.
CITATION STYLE
Motik, B., & Horrocks, I. (2008). Individual reuse in description logic reasoning. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 242–258). https://doi.org/10.1007/978-3-540-71070-7_20
Mendeley helps you to discover research relevant for your work.