Redundancy in Logic I: CNF Propositional Formulae
arXiv:cs/0211031 · doi:10.1016/j.artint.2004.11.002
Abstract
A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study the problem of checking whether a CNF formula (a set of clauses) is redundant, that is, it contains clauses that can be derived from the other ones. Any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset (I.E.S.) We study the complexity of some related problems: verification, checking existence of a I.E.S. with a given size, checking necessary and possible presence of clauses in I.E.S.'s, and uniqueness. We also consider the problem of redundancy with different definitions of equivalence.
Extended and revised version of a paper that has been presented at ECAI 2002
References in corpus (1)
Cited by in corpus (10)
- On Redundant Topological Constraints
- Redundancy in Logic II: 2CNF and Horn Propositional Formulae
- Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
- Redundancy in Logic III: Non-Mononotonic Reasoning
- Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality
- On Efficiently Explaining Graph-Based Classifiers
- Logic Mining Using Neural Networks
- Minimal Assumptions Refinement for GR(1) Specifications
- Some notes on model rotation
- SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --