Mastersthesis,
Non-standard inference for explaining subsumption in the description logic EL with general concept inclusions and complex role inclusions
Technische Universitat Dresden, (2007)
Abstract
Ontologies 11 are now ubiquitous and many of them are currently being ported into logical formalisms, most notably description logic (DL) 2. It is inevitable that such migration might introduces inconsistencies – both in terms of logically and ontologically – which could be far from obvious. This motivates the recent research topic of explanation of DLbased ontologies. Explanation comes in two flavors: pinpointing 5, 21, 15 which addresses the source of inconsistencies found in the ontology and debugging 14 which recovers the ontology into a consistent state. Since the latter often requires information from the former, we consider axiom pinpointing as essential for both flavors of the explanation problem. Much of the research in this area is focusing on expressive DLs, in which standard reasoning alone is already highly intractable. In this paper, we investigate this problem in a tractable extension of EL which is useful in life science applications. We have discovered that pinpointing is inherently intractable – despite the tractable logic considered – if all information is required. This is due to the combinatorial blow-up of possible sets of axioms. We develop a labelled algorithm for axiom pinpointing based on the EL subsumption algorithm and the known labelling technique used in tableau algorithm. For implementation purposes, we restrict this algorithm to computation of only partial information, for which polynomial-time algorithm can be obtained. We have experimented this approach on GALEN 18 and found that even partial information can already help ease the way an ontology is being debugged.
