Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing

DOI10.1007/978-3-319-24318-4_24MaRDI QIDQ3453236zbMATH OpenOpenAlexFDO

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)

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(7)

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

Describes a project that uses

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)