Ullrich Hustadt, Boris Motik, and Ulrike Sattler
As applications of description logics proliferate, efficient reasoning with large ABoxes (sets of individuals with descriptions) becomes ever more important. Motivated by the prospects of reusing optimization techniques from deductive databases, in this paper, we present a novel approach to checking consistency of ABoxes, instance checking and query answering, w.r.t. ontologies formulated using a slight restriction of the description logic SHIQ. Our approach proceeds in three steps: (i) the ontology is translated into first-order clauses, (ii) TBox and RBox clauses are saturated using a resolution-based decision procedure, and (iii) the saturated set of clauses is translated into a disjunctive datalog program. Thus, query answering can be performed using the resulting program, while applying all existing optimization techniques, such as join-order optimizations or magic sets. Equally important, the resolution-based decision procedure we present is for unary coding of numbers worst-case optimal, i.e. it runs in ExpTime.