A Resolution−Based Decision Procedure for SHOIQ
Yevgeny Kazakov and Boris Motik
Abstract
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.
Details
| Journal |
Journal of Automated Reasoning |
| Number |
2−3 |
| Pages |
89−116 |
| Volume |
40 |
| Year |
2008 |
Links
Related pages
|
People |
|
|
Activities |