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.
Book Title
IJCAR
Pages
662−677
Publisher
Springer
Series
Lecture Notes in Computer Science
Volume
4130
Year
2006