Debugging ει+ ontologies through Horn MUS enumeration

Alexey Ignatiev, Joao Marques-Silva, Carlos Mencía, Rafael Peñaloza

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearch


In description logics (DLs), axiom pinpointing refers to the problem of enumerating the minimal subsets of axioms from an ontology that entail a given consequence. Recent developments on axiom pinpointing for the light-weight DL EL+ are based on translating this problem into the enumeration of all minimally unsatisfiable subformulas (MUSes) of a propositional formula, and using advanced SAT-based techniques for solving it. Further optimizations have been obtained by targeting the MUS enumerator to the specific properties of the formula obtained. In this paper we describe different improvements that have been considered since the translation was first proposed. Through an empirical study, we analyse the behaviour of these techniques and how it depends on different characteristics of the original pinpointing problem, and the translated SAT formula.

Original languageEnglish
Title of host publicationProceedings of the 30th International Workshop on Description Logics
EditorsAlessandro Artale, Birte Glimm, Roman Kontchakov
Place of PublicationAachen Germany
PublisherRheinisch-Westfaelische Technische Hochschule Aachen
Number of pages13
ISBN (Electronic)007418796
Publication statusPublished - 2017
Externally publishedYes
EventInternational Workshop on Description Logics 2017 - Montpellier, France
Duration: 18 Jul 201721 Jul 2017
Conference number: 30th

Publication series

NameCEUR Workshop Proceedings
PublisherRheinisch-Westfaelische Technische Hochschule Aachen * Lehrstuhl Informatik V
ISSN (Electronic)1613-0073


ConferenceInternational Workshop on Description Logics 2017
Abbreviated titleDL 2017
Internet address

Cite this