BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies

DOI10.1007/978-3-319-40970-2_32zbMath1475.68368OpenAlexW2487667488MaRDI QIDQ2818038

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

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_32

Mathematics Subject Classification ID

Knowledge representation (68T30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (6)

The Bayesian ontology language \(\mathcal {BEL}\) ⋮ Counting minimal unsatisfiable subsets ⋮ Understanding the complexity of axiom pinpointing in lightweight description logics ⋮ Pinpointing axioms in ontologies via ASP ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ Hypergraph-based inference rules for computing \(\mathcal{EL}^+\)-ontology justifications

Uses Software

• Ltur
• CEL
• BEACON
• Just
• MaxHS
• EL2MCS
• HgMUS

Cites Work

• Unnamed Item
• Fast, flexible MUS enumeration
• A theory of diagnosis from first principles
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Redundancy in logic. I: CNF propositional formulae
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Unification as a complexity measure for logic programming
• Consistent subsets of inconsistent systems: structure and behaviour
• Enumerating Infeasibility: Finding Multiple MUSes Quickly
• Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis

This page was built for publication: BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies