A Resolution-Based Decision Procedure for SHOIQ

14 years 7 months ago
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.
Yevgeny Kazakov, Boris Motik
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Yevgeny Kazakov, Boris Motik
Comments (0)