Reasoning Algebraically with Description Logics

Semantic Web applications based on the Web Ontology Language (OWL) often require the use of numbers in class descriptions for expressing cardinality restrictions on properties or even classes. Some of these cardinalities are specified explicitly, but quite a few are entailed and need to be discovered by reasoning procedures. Due to the Description Logic (DL) foundation of OWL, those reasoning services are offered by DL reasoners. Existing DL reasoners employ reasoning procedures that are arithmetically uninformed and substitute arithmetic reasoning by "don't know" non-determinism in order to cover all possible cases. This lack of information about arithmetic problems dramatically degrades the performance of DL reasoners in many cases, especially with ontologies relying on the use of Nominals and Qualied Cardinality Restrictions. The contribution of this thesis is twofold: on the theoretical level, it presents algebra�ic reasoning with DL (ReAl DL) using a sound, complete, and terminating reasoning procedure for the DL SHOQ. ReAl DL combines tableau reasoning procedures with algebraic methods, namely Integer Programming, to ensure arithmetically better informed reasoning. SHOQ extends the standard DL ALC with transitive roles, role hierarchies, qualified cardinality restrictions (QCRs), and nominals, and forms an expressive subset of OWL. Although the proposed algebraic tableau is double exponential in the worst case, it deals with cardinalities with an additional level of information and properties that make the calculus amenable and well suited for optimizations. In order for ReAl DL to have a practical merit, suited optimizations are proposed towards achieving an efficient reasoning approach that addresses the sources of complexity related to nominals and QCRs. On the practical level, a running prototype reasoner (HARD) is implemented based on the proposed calculus and optimizations. HARD is used to evaluate the practical merit of ReAl DL, as well as the effectiveness of the proposed optimizations. Experimental results based on real world and synthetic ontologies show that ReAl DL outperforms existing reasoning approaches in handling the interactions between nominals and QCRs. ReAl DL also comes with some interesting features such as the ability to handle ontologies with cyclic descriptions without adopting special blocking strategies. ReAl DL can form a basis to provide more efficient reasoning support for ontologies using nominals or QCRs