Abstract

We present a hybrid tableau calculus for the description logic (DL) SHIQ. The presented algorithm decides SHIQ ABox consistency and uses an algebraic approach for more informed
reasoning about qualified number restrictions (QNRs). Benefiting from integer linear programming and several optimization techniques to deal with the interaction of QNRs and inverse roles, our approach provides a more deterministic and informed calculus. In addition, a prototype reasoner based on the hybrid calculus has been implemented that decides concept satisfiability for ALCHIQ. We provide a set of benchmarks that demonstrate the effectiveness of our hybrid reasoner in comparison to other DL reasoners.