EL2MCS: Axiom Pinpointing in EL+ Description Logics

EL2MCS is a SAT-based tool for axiom pinpointing in EL+ Description Logics. It exploits the relationship between minimal axiom sets (MinAs) and minimal unsatisfiable subformulas (MUSes) of an encoded Horn formula, as well as explicit minimal hitting set dualization of the MUSes and minimal correction subsets (MCSes) of the Horn formula.

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

You can also be interested in EL2MUS.

Print/export