A Hypertableau Calculus for SHIQ

We present a novel reasoning calculus for the Description Logic SHIQ. 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.

• Type: Conference
• Year: 2007
• Where: DLOG
• Authors: Boris Motik, Rob Shearer, Ian Horrocks
• Keywords: Automated Reasoning, Calculus, Description Logic Shiq, DLOG 2007, General Inclusion Axioms