Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing

DOI10.1007/978-3-319-24318-4_24zbMath1471.68173arXiv1505.04365OpenAlexW952867079MaRDI QIDQ3453236

Carlos Mencía, M. Fareed Arif, João P. Marques-Silva

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1505.04365

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Medical applications (general) (92C50) Knowledge representation (68T30) Computational aspects of satisfiability (68R07)

Related Items (7)

The Bayesian ontology language \(\mathcal {BEL}\) ⋮ On Tackling Explanation Redundancy in Decision Trees ⋮ BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies ⋮ HgMUS ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ On the complexity of inconsistency measurement ⋮ Hypergraph-based inference rules for computing \(\mathcal{EL}^+\)-ontology justifications

Uses Software

• MiniSat
• Pellet
• Ltur
• CEL
• Just
• EL2MCS
• QUICKXPLAIN

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
• Debugging incoherent terminologies
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Optimal Implementation of Watched Literals and More General Techniques
• Error-Tolerant Reasoning in the Description Logic $\mathcal{E{\kern-.1em}L}$
• Complexity of Axiom Pinpointing in the DL-Lite Family of Description Logics
• Towards efficient MUS extraction
• Combining approaches for solving satisfiability problems with qualitative preferences
• Axiom Pinpointing in General Tableaux
• optsat: A Tool for Solving SAT Related Optimization Problems
• 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
• MaxSAT-based encodings for Group MaxSAT
• Enumerating Infeasibility: Finding Multiple MUSes Quickly
• Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
• Theory and Applications of Satisfiability Testing
• Mechanizing Mathematical Reasoning

This page was built for publication: Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing