Optimized Reasoning in Description Logics Using Hypertableaux

We present a novel reasoning calculus for Description Logics (DLs)-knowledge representation formalisms with applications in areas such as the Semantic Web. In order to reduce the nondeterminism due to general inclusion axioms, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. To prevent the calculus from generating large models, we introduce "anywhere" pairwise blocking. Our preliminary implementation shows significant performance improvements on several well-known ontologies. To the best of our knowledge, our reasoner is currently the only one that can classify the original version of the GALEN terminology. © Springer-Verlag Berlin Heidelberg 2007.