Abstract

The growing demand for efficient knowledge representation and reasoning in the era of interconnected systems and extensive data collection motivates this thesis. Addressing the limitations of existing Description Logic (DL) reasoners, we focus on the challenges posed by qualified cardinality restrictions (QCRs), nominals, and inverse roles. These constructs, though crucial for expressive ontologies, often hinder computational efficiency in traditional reasoning approaches. Consequently, real-world ontologies either exclude them or employ very small numerical values. This motivates our exploration of a novel reasoning approach, employing algebraic methods, aiming to enhance DL reasoning with a focus on large numerical restrictions.

In this thesis, a novel algebraic tableau calculus for SHOIQ is presented for deciding ontology consistency. This hybrid approach integrates standard tableau-based reasoning with algebraic reasoning to handle a large number of nominals, QCRs, and their interaction with inverse roles. The algorithm extends the previously presented algebraic tableau algorithm for SHOI. Numerical restrictions imposed by nominals and qualified number restrictions are encoded into a set of linear inequalities. The knowledge about other axioms, such as universal restrictions, role hierarchy, subsumption and disjointness, is also embedded in order to get a more informed mapping of QCR satisfiability to feasibility. Column generation and branch-and-price algorithms are used to solve these inequalities. The feasibility test for the linear inequalities can be computed in polynomial time. Rigorous proofs ensure soundness, completeness, and termination of the reasoning procedure.

In practice, the proposed reasoning approach, implemented in the Cicada prototype, demonstrates its effectiveness against existing state-of-the-art reasoners. Empirical evaluations using synthetic and ORE 2014 datasets reveal Cicada's robust performance against increasing numerical values, showcasing its viability for handling expressive ontologies. Despite its more focused optimization techniques, Cicada outperforms other reasoners in certain scenarios, providing a promising avenue for practical applications requiring efficient DL reasoning.