U. Hustadt, B. Motik, and U. Sattler (2004c): ``Reasoning for Description Logics around SHIQ in a Resolution Framework.'' FZI-Report 3-8-04/04, FZI Karlsruhe, Germany.
Abstract, BibTeX, PDF.

We present several algorithms for reasoning with description logics closely related to SHIQ. Firstly, we present an algorithm for deciding satisfiability of SHIQ knowl edge bases. Then, to enable representing concrete data such as strings or integers, we devise a general approach for reasoning with concrete domains in the framework of resolution, and apply it to obtain a procedure for deciding SHIQ(D). For unary coding of numbers, this procedure is worst-case optimal, i.e. it runs in exponential time. Motivated by the prospects of reusing optimization techniques from deductive databases, such as magic sets, we devise an algorithm for reducing SHIQ(D) knowledge bases to disjunctive datalog programs. Furthermore, we show that so-called DL-safe rules can be combined with disjunctive programs obtained by our transformation to increase the expressivity of the logic, without affecting decidability. We show that our algorithms can easily be extended to handle answering conjunctive queries over SHIQ(D) knowledge bases. Finally, we extend our algorithms to support metamodel- ing. Since SHIQ(D) is closely related to OWL-DL, our algorithms provide alternative mechanisms for reasoning in the Semantic Web. [an error occurred while processing this directive]