I.: Hypertableau Reasoning for Description Logics

We present a novel reasoning calculus for the Description Logic SHOIQ+—a knowl-edge representation formalism 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 intro-duce anywhere pairwise blocking. We also present a new way of ensuring termination while allowing for nomials, inverse roles, and number restrictions—a combination of DL constructs that has proven notoriously difficult to handle. Our preliminary implementa-tion 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