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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:581368 |
| Date | January 2013 |
| Creators | Simancik, Frantisek |
| Contributors | Horrocks, Ian; Kazakov, Yevgeny |
| Publisher | University of Oxford |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://ora.ox.ac.uk/objects/uuid:5e16d4ca-d80b-413b-9701-28febcf15613 |
Page generated in 0.0017 seconds