Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing

DOI10.1007/978-3-319-24318-4_24zbMATH Open1471.68173arXiv1505.04365OpenAlexW952867079MaRDI QIDQ3453236FDOQ3453236

Authors: M. Fareed Arif, Carlos Mencía, Joao Marques-Silva 

Publication date: 20 November 2015

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

Abstract: The enumeration of minimal unsatisfiable subsets (MUSes) finds a growing number of practical applications, that includes a wide range of diagnosis problems. As a concrete example, the problem of axiom pinpointing in the EL family of description logics (DLs) can be modeled as the enumeration of the group-MUSes of Horn formulae. In turn, axiom pinpointing for the EL family of DLs finds important applications, such as debugging medical ontologies, of which SNOMED CT is the best known example. The main contribution of this paper is to develop an efficient group-MUS enumerator for Horn formulae, HGMUS, that finds immediate application in axiom pinpointing for the EL family of DLs. In the process of developing HGMUS, the paper also identifies performance bottlenecks of existing solutions. The new algorithm is shown to outperform all alternative approaches when the problem domain targeted by group-MUS enumeration of Horn formulae is axiom pinpointing for the EL family of DLs, with a representative suite of examples taken from different medical ontologies.

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

Recommendations

• Fast, flexible MUS enumeration
• Efficient reasoning for inconsistent Horn formulae
• Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
• Enumerating infeasibility: finding multiple MUSes quickly
• Towards efficient MUS extraction

Mathematics Subject Classification ID

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

Cites Work

• Theory and Applications of Satisfiability Testing
• optsat: A Tool for Solving SAT Related Optimization Problems
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Axiom Pinpointing in General Tableaux
• Consistent subsets of inconsistent systems: structure and behaviour
• Title not available (Why is that?)
• A theory of diagnosis from first principles
• Fast, flexible MUS enumeration
• Towards efficient MUS extraction
• Combining approaches for solving satisfiability problems with qualitative preferences
• Enumerating infeasibility: finding multiple MUSes quickly
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Unification as a complexity measure for logic programming
• Mechanizing Mathematical Reasoning
• Error-tolerant reasoning in the description logic \(\mathcal{EL}\)
• Debugging incoherent terminologies
• MaxSAT-based encodings for Group MaxSAT
• Complexity of Axiom Pinpointing in the DL-Lite Family of Description Logics
• Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
• Optimal implementation of watched literals and more general techniques

Cited In (7)

• Hypergraph-based inference rules for computing \(\mathcal{EL}^+\)-ontology justifications
• BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
• On Tackling Explanation Redundancy in Decision Trees
• On the complexity of inconsistency measurement
• HgMUS
• Efficient reasoning for inconsistent Horn formulae
• The Bayesian ontology language \(\mathcal {BEL}\)

Uses Software

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

This page was built for publication: Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453236)