Doctoral Seminar: Jelena Vlasenko

Speaker: Jelena Vlasenko

Supervisor: Dr. V. Haarslev

Supervisory Committee:
Drs. F. Khendek, L. Kosseim, J. Rilling

Title: Saturation-based Algebraic Reasoning for Description Logic ALCQ

Date: Thursday, March 30, 2017

Time: 11:40 a.m.

Place: EV 3.309

ABSTRACT

In this work, we present a new highly optimized reasoning algorithm named Avalanche for the description logic ALCQ. We take as a basis the description language EL that allows only two operations - intersection of concepts and existential restrictions. Then, we extend EL with qualified cardinality restrictions Q, complex concept negation C, disjunctions U, and propose a reasoning algorithm for the resulting language ALCQ, where ALC is a common abbreviation for ELCU. The proposed algorithm leverages a number of widely applied techniques such as lazy unfolding, absorption, saturation, and linear optimization. Absorption is used to facilitate the lazy unfolding of complex axioms, thus reducing the indeterminism of the constructed model. Saturation is applied to create a saturated version of a completion graph that will be further expanded by applying additional completion rules. The goal of the saturation phase is to reduce the overall size of the constructed model. Finally, linear optimization is leveraged in order to handle qualified number restrictions. The goal of this work is to build an algorithm that would be able to reason on knowledge bases more effectively than the other existing algorithms.