Practical reasoning with qualified number restrictions: A hybrid Abox calculus for the description logic 𝒮ℋ𝒬

Abstract

This article presents a hybrid Abox tableau calculus for 𝒮ℋ𝒬 which extends the basic description logic 𝒜ℒ𝒞 with role hierarchies, transitive roles, and qualified number restrictions. The prominent feature of our hybrid calculus is that it reduces reasoning about qualified number restrictions to integer linear programming. The calculus decides 𝒮ℋ𝒬 Abox consistency w.r.t. a Tbox containing general axioms. The presented approach ensures a more informed calculus which adequately handles the interaction between numerical and logical restrictions in 𝒮ℋ𝒬 concept and individual descriptions. A prototype reasoner for deciding 𝒜ℒ𝒞ℋ𝒬 concept satisfiability has been implemented. An empirical evaluation of our hybrid reasoner and its integrated optimization techniques for a set of synthesized benchmarks featuring qualified number restrictions clearly demonstrates the effectiveness of our hybrid calculus.