2015/05/17 by M. Fareed Arif, Arif, M. Fareed, Carlos Mencía +4
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.48550/arxiv.1505.04365
arxiv created 2015/05/17 · openalex publication_date 2015/05/17 · arxiv updated 2015/05/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.