Abstract

Qualified cardinality restrictions are expressive language constructs which extend the basic description logic ALC with the ability of expressing numerical constraints about relationships. However, the well-known standard tableau algorithms perform weakly when dealing with cardinality restrictions. Therefore, an arithmetically informed approach seems to be inevitable when dealing with these cardinality restrictions. This thesis presents a hybrid tableau calculus for the description logic SHQ which extends ALC by qualified cardinality restrictions, role hierarchies, and transitive roles. The hybrid calculus is based on the so-called atomic decomposition technique and combines arithmetic and logical reasoning. The most prominent feature of this hybrid calculus is that it reduces reasoning about qualified number restrictions to integer linear programming. Therefore, according to the nature of arithmetic reasoning, this calculus is not affected by the size of numbers occurring in cardinality restrictions. Furthermore, we give evidence on how this method of hybrid reasoning can improve the performance of reasoning by organizing the search space more competently. An empirical evaluation of our hybrid reasoner for a set of synthesized benchmarks featuring qualified number restrictions clearly demonstrates its superior performance. In comparison to other standard description logic reasoners, our approach demonstrates an overall runtime improvement of several orders of magnitude.