Skip to main content
Thesis defences

PhD Oral Exam - Nikoo Zolfaghar Karahroodi, Computer Science

Consequence-based Algebraic Reasoning for SHOQ

Date & time
Wednesday, April 3, 2024
10 a.m. – 1 p.m.

This event is free


School of Graduate Studies


Nadeem Butt


ER Building
2155 Guy St.
Room 1222

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.


Qualifies Cardinality Restrictions (QCRs) and nominals are the two constructors in OWL 2 DL to apply numerical restrictions on domain concepts and relations. Utilizing these constructors in designing real-world ontologies is unavoidable in many domains, particularly in modelling structures with complex objects. Most existing DL reasoners employ arithmetically uninformed processes to reason about these numeric restrictions by exploring all possible cases.

Meanwhile, Consequence-based (CB) reasoning algorithms have proven to have a phenomenal performance in practice. However, they had yet to be extended for the expressive DL SHOQ - a DL that supports naming and counting quantifiers. This research presents a novel consequence-based algorithm to classify SHOQ while handling the arithmetic interaction between QCRs and Nominals using atomic decomposition and integer linear programming. The proposed calculus can classify the whole ontology in one round. We have implemented our calculus in a prototype reasoner called CARON.

Empirical evaluation of our implementation demonstrates that CARON outperforms existing reasoners in handling numerical restrictions. At the same time, it offers a competitive performance compared to other state-of-the-art systems. Our results also show that CARON nicely complements existing reasoners for handling numerical restrictions since it provides an arithmetically informed process for handling these constructors. Accordingly, the calculus and implementation presented in this thesis are critical to improving practical reasoning with expressive DLs, including numerical restrictions.

Back to top

© Concordia University