BEACON: an efficient SAT-based tool for debugging ει+ ontologies

M. Fareed Arif, Carlos Mencía, Alexey Ignatiev, Norbert Manthey, Rafael Peñaloza, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

20 Citations (Scopus)


Description Logics (DLs) are knowledge representation and reasoning formalisms used in many settings. Among them, the εL 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 errorprone process which often leads to unintended inferences. This paper presents the BEACON tool for debugging εL+ ontologies. BEACON builds on earlier work relating minimal justifications (MinAs) of εL+ ontologies and MUSes of a Horn formula, and integrates state-of-the-art algorithms for solving different function problems in the SAT domain.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2016
Subtitle of host publication19th International Conference Bordeaux, France, July 5–8, 2016 Proceedings
EditorsNadia Creignou, Daniel Le Berre
Place of PublicationCham Switzerland
Number of pages10
ISBN (Electronic)9783319409702
ISBN (Print)9783319409696
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2016 - Bordeaux, France
Duration: 5 Jul 20168 Jul 2016
Conference number: 19th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2016
Abbreviated titleSAT 2016
Internet address

Cite this