Extended caching, backjumping and merging for expressive description logics

Abstract

With this contribution we push the boundary of some known optimisations such as caching to the very expressive Description Logic . The developed method is based on a sophisticated dependency management and a precise unsatisfiability caching technique, which further enables better informed tableau backtracking and more efficient pruning. Additionally, we optimise the handling of cardinality restrictions, by introducing a strategy called pool-based merging. We empirically evaluate the proposed optimisations within the novel reasoning system Konclude and show that the proposed optimisations indeed result in significant performance improvements. © 2012 Springer-Verlag.