Qualified Cardinality Restrictions (QCRs) and nominals are the two constructors in OWL 2 DL to apply numerical restrictions on domain concepts and relations. Utilizing these constructors in designing real-world ontologies is unavoidable in many domains, particularly in modelling structures with complex objects. Most existing DL reasoners employ arithmetically uninformed processes to reason about these numeric restrictions by exploring all possible cases.
Meanwhile, Consequence-Based (CB) reasoning algorithms have proven to have a phenomenal performance in practice. However, they have yet to be extended for the expressive DL SHOQ - a DL that supports named individuals and cardinality restrictions. This research presents a novel consequence-based algorithm to classify SHOQ while handling the arithmetic interaction between QCRs and Nominals using atomic decomposition and integer linear programming. The proposed calculus can classify the whole ontology in one round. We have implemented our calculus in a prototype reasoner called CARON.
Empirical evaluation of our implementation demonstrates that CARON outperforms existing reasoners in handling numerical restrictions. At the same time, it offers a competitive performance compared to other state-of-the-art systems. Our results also show that CARON nicely complements existing reasoners for handling numerical restrictions since it provides an arithmetically informed process for handling these constructors. Accordingly, the calculus and implementation presented in this thesis are critical to improving practical reasoning with expressive DLs, including numerical restrictions.