The role of unsatisfiable Boolean constraints in lightweight description logics

Lightweight Description Logics (e.g. EL, EL+ etc.) are commonly used languagesto represent life science ontologies. In such languages ontology classification– the problem of computing all the subsumption relations – is tractableand used to characterize all the classes and properties in any given ontology.Despite the fact that classification is tractable in EL+, axiom pinpointing – theproblem of computing the reasons of an (unintended) subsumption relation –is still worst-case exponential. This thesis proposes state-of-the art SAT-basedaxiom pinpointing methods for the Lightweight Description Logic EL+. Theseaxiom pinpointing methods emanate from the analysis of minimal unsatisfiableboolean constraints using hitting set dualization that is also related toReiter’s model-based diagnosis. Its consequences are significant both in termsof algorithms (i.e., MUS extraction and enumeration methods) as well as understandingaxiom pinpointing in Lightweight Description Logics through theprism of minimal unsatisfiable boolean constraints and its related problems(i.e., hypergraph transversal).