| Sumari: | We present a resolution-based decision procedure for the description logic <em>SHOIQ</em>—the logic underlying the Semantic Web ontology language <em>OWLDL</em>. Our procedure is goal-oriented, and it naturally extends a similar procedure for <em>SHIQ</em>, which has proven itself in practice. Applying existing techniques for saturation-based decision procedures to <em>SHOIQ</em> 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.
|
|---|