Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT

The problem of reasoning with qualified number restrictions in Description Logics (DLs) has been investigated since the very first research steps in automated reasoning for DLs. Moreover, developing techniques for optimized reasoning with qualified number restrictions and has gained further importance since qualified number restrictions have been added to the forthcoming standard OWL 2 for Semantic Web applications. On the one hand, however, actual DL reasoning techniques, often lack of efficiency in handling those features, especially when the number of restrictions or the values involved are high. On the other hand the manifold problem of reasoning including numerical constraints is a well-established and thoroughly investigate problem in the SMT community, in which a lot of effort is continuously spent in order to enhance the efficiency of reasoning techniques for such kind of problems. In this paper we propose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. The idea is to encode an ALCQ ontology into a formula in Satisfiability Modulo the Theory of Costs (SMT(C)), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Integers (LA(Z)), and to exploit the power of modern SMT solvers to compute every concept-satisfiability query on a given ontology. We have implemented and tested our approach (called ALCQ2SMT_C) and some optimizations on a wide set of synthesized benchmark formulas, comparing the approach with the main state-of-the-art tools available. Our empirical evaluation confirms the potential of the approach.