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. Extending this procedure to SHOIQ using existing techniques is not straightforward because of nominals, number restrictions, and inverse roles--a combination known to cause termination problems. We overcome this difficulty by using basic superposition calculus extended with custom simplification rules.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Yevgeny Kazakov, Boris Motik
• Keywords: Automated Reasoning, Basic Superposition Calculus, CADE 2006, Resolution-based Decision Procedure, Similar Procedure