Abstract

In this work we present a novel calculus for the description logic ALCHQ implemented in a reasoner named Avalanche. ALCHQ permits intersection, disjunction, and negation of concepts. It also allows existential and universal restrictions, role hierarchy, and qualified number restrictions that are of particular interest to us. Avalanche incorporates a number of widely applied and well known optimization techniques such as saturation, resolution, and linear optimization. We apply saturation to create a compressed version of a saturation graph. As a result, the overall size of the constructed model can be kept reasonably small. We employ resolution techniques in order to reason on disjunctions that are part of our calculus. Finally and most importantly, we leverage linear optimization to handle qualified number restrictions. We transform qualified number restrictions into linear programs and then apply the Branch-and-Price algorithm to solve them in the most efficient way. This novel approach gives us a clear advantage over the other reasoners that implement a more traditional procedure to deal with qualified number restrictions as there are ontologies containing entailments caused by the presence of qualified number restrictions that can be classified only by Avalanche.