When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.
Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.
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 that is further expanded by applying additional completion rules to ensure soundness and completeness of the proposed calculus. 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 powerful column generation algorithm Branch-and-Price 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.