Consequence-based reasoning in Lightweight Description Logic EL+
Description Logics (DLs) are knowledge representation and reasoning formalisms widely used in many practical settings. Among them, the EL family of DLs stands out due to the availability of polynomial-time inference algorithms and its ability to represent knowledge from domains such as medical informatics. However, the construction of an ontology is an error-prone process which often leads to unintended inferences. This work presents the BEACON SAT-based tool for debugging EL+ ontologies. BEACON builds on earlier work relating minimal justifications (MinAs) of EL + ontologies and MUSes of a Horn formula, and it integrates state-of-the-art algorithms for solving different function problems in the SAT domain.
