Automated Reasoning in ALCQ via SMT

Reasoning techniques for qualified number restrictions (QNRs) in De- scription Logics (DLs) have been investigated in the past but they mostly do not make use of the arithmetic knowledge implied by QNRs. In this paper we pro- pose and investigate a novel approach for concept satisfiability in acyclic ALCQ ontologies. It is based on the idea of encoding an ALCQ ontology into a for- mula in Satisfiability Modulo the Theory of Costs (SMT ( C ) ), which is a specific and computationally much cheaper subcase of Linear Arithmetic under the Inte- gers, and to exploit the power of modern SMT solvers to compute every concept- satisfiability query on a given ontology. We implemented and tested our approach, which includes a very effective individuals-partitioning technique, on a wide set of synthesized benchmark formulas, comparing the approach with the main state- of-the-art DL reasoners available. Our empirical evaluation confirms the potential of the approach