EL2MUS: Axiom Pinpointing for the EL+ Description Logic

High-performance axiom pinpointing tool for ontologies described in the EL+ description logic.


EL2MUS is a high-performance tool for diagnosing ontologies represented with the EL+ description logic. EL2MUS is based on exploiting high performance Boolean Satisfiability (SAT) solvers and the relationship between subsert minimal axiom sets (MinAs) and minimal unsatisfiable subformulas (MUSes).


A Linux 64-bit executable (as well as supporting documentation) is available here.