A Resolution-Based Decision Procedure for SHOIQ.

We present a resolution-based decision procedure for the description logic SHOIQ - the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for deriving saturation-based decision procedures to SHOIQ is not straightforward due to nominals, number restrictions, and inverse roles - a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus, extended with custom simplification rules. © Springer-Verlag Berlin Heidelberg 2006