  The enumeration of minimal unsatisfiable subsets (MUSes) finds a growing
number of practical applications, that includes a wide range of diagnosis
problems. As a concrete example, the problem of axiom pinpointing in the EL
family of description logics (DLs) can be modeled as the enumeration of the
group-MUSes of Horn formulae. In turn, axiom pinpointing for the EL family of
DLs finds important applications, such as debugging medical ontologies, of
which SNOMED CT is the best known example. The main contribution of this paper
is to develop an efficient group-MUS enumerator for Horn formulae, HGMUS, that
finds immediate application in axiom pinpointing for the EL family of DLs. In
the process of developing HGMUS, the paper also identifies performance
bottlenecks of existing solutions. The new algorithm is shown to outperform all
alternative approaches when the problem domain targeted by group-MUS
enumeration of Horn formulae is axiom pinpointing for the EL family of DLs,
with a representative suite of examples taken from different medical
ontologies.
