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 OWLDL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for 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.
Details
| Book Title |
IJCAR |
| Pages |
662−677 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
4130 |
| Year |
2006 |
Links
Related pages
|
People |
|
|
Activities |