Algebraic tableau reasoning for the description logic SHOQSHOQ

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 which 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 (OO) and qualified cardinality restrictions (QQ). In this article we present a new algebraic tableau reasoning procedure for the DL SHOQSHOQ that combines tableau procedures and algebraic methods, namely linear integer programming, to ensure arithmetically better informed reasoning procedures. SHOQSHOQ extends the standard DL ALCALC (which is equivalent to the multi-modal logic KmKm) with transitive roles, role hierarchies, qualified cardinality restrictions, and nominals, and forms an expressive subset of the web ontology language OWL 2. Although the proposed algebraic tableau (in analogy to standard tableau) is still double exponential in the worst case, it deals with cardinalities in a very informed way due to its arithmetic component and can be considered as a novel foundation for informed reasoning procedures addressing cardinality restrictions.