Consequence-based reasoning for ontology classification

Thesis

Description logics (DLs) are knowledge representation languages that provide the theoretical underpinning for modern ontology languages such as OWL and serve as the basis for the development of ontology reasoners and tools.

Most modern ontology reasoners are based on optimized tableau algorithms, which perform reasoning by trying to build counter-models. More recently, another kind of reasoning algorithms has been introduced that, instead of building counter-models, directly derive logical consequences of axioms in the ontology using inference rules. Such consequence-based algorithms were first introduced for the EL family of DLs, and later extended to more expressive Horn DLs. However, up until now, consequence-based algorithms could not handle non-Horn features such as disjunctions.

We consider several complementary aspects of consequence-based reasoning in this thesis. Firstly, we describe the parallelized consequence-based reasoner ELK, which is currently the fastest reasoner for EL ontologies. Secondly, we demonstrate how consequence-based algorithms can be extended to handle disjunctions using inference rules reminiscent of ordered resolution. Finally, we combine our consequence-based framework with methods based on tree decompositions, and thus obtain what we believe are the first fixed-parameter tractability results for subsumption reasoning in DLs.

Authors: Simancik, F

• Publication date: 2013
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: Oxford University, UK
• Language: English
• Keywords: description logics; classification; algorithms and optimization
• Subjects: Artificial Intelligence; Applications and algorithms