Efficient Reasoning for Inconsistent Horn Formulae
From MaRDI portal
Publication:2835881
DOI10.1007/978-3-319-48758-8_22zbMath1483.68381OpenAlexW2540198404MaRDI QIDQ2835881
Alexey Ignatiev, Rafael Peñaloza, Carlos Mencía, João P. Marques-Silva
Publication date: 30 November 2016
Published in: Logics in Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-48758-8_22
Related Items (4)
On Tackling Explanation Redundancy in Decision Trees ⋮ Understanding the complexity of axiom pinpointing in lightweight description logics ⋮ From simplification to a partial theory solver for non-linear real polynomial constraints ⋮ On the complexity of inconsistency measurement
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the query complexity of selecting minimal sets for monotone predicates
- Resolution-based lower bounds in MaxSAT
- Solving satisfiability in less than \(2^ n\) steps
- A theory of diagnosis from first principles
- On generating all maximal independent sets
- LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
- Investigations on autark assignments
- The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies
- Redundancy in logic. II: 2CNF and Horn propositional formulae
- Redundancy in logic. I: CNF propositional formulae
- MCS Extraction with Sublinear Oracle Queries
- BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies
- Horn Clause Solvers for Program Verification
- Complexity of Axiom Pinpointing in the DL-Lite Family of Description Logics
- Towards efficient MUS extraction
- Computing Maximal Autarkies with Few and Simple Oracle Queries
- 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
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Unit Refutations and Horn Sets
- The complexity of logic-based abduction
- NP-completeness: A retrospective
- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
- On sentences which are true of direct unions of algebras
This page was built for publication: Efficient Reasoning for Inconsistent Horn Formulae
