Skip to main content
Thesis defences

PhD Oral Exam - Jelena Vlasenko, Computer Science

Saturation-based Algebraic Reasoning for Description Logic ALCHQ

Date & time
Tuesday, April 2, 2024
10 a.m. – 1 p.m.

This event is free


School of Graduate Studies


Nadeem Butt


ER Building
2155 Guy St.
Room 1072

Wheel chair accessible


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.


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.

Back to top

© Concordia University