Redundancy in Logic II: 2CNF and Horn Propositional Formulae

Abstract

We report complexity results about redundancy of formulae in 2CNF form. We first consider the problem of checking redundancy and show some algorithms that are slightly better than the trivial one. We then analyze problems related to finding irredundant equivalent subsets (I.E.S.) of a given set. The concept of cyclicity proved to be relevant to the complexity of these problems. Some results about Horn formulae are also shown.

Corrected figures on Theorem 10; added and modified some references

References in corpus (4)

• Redundancy in Logic I: CNF Propositional Formulae
• Approximating the Minimum Equivalent Digraph
• Redundancy in Logic III: Non-Mononotonic Reasoning
• Merging Locally Correct Knowledge Bases: A Preliminary Report

Cited by in corpus (6)

• Redundancy in Logic III: Non-Mononotonic Reasoning
• Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality
• On Forgetting in Tractable Propositional Fragments
• The classification of minimally unsatisfiable 2-CNFs -- a fundamental study
• The Horn Non-Clausal Class and its Polynomiality
• SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --