## Redundancy in Logic II: 2CNF and Horn Propositional
Formulae

**Paolo Liberatore**
*Artificial Intelligence*

We report results about the redundancy of formulae in 2CNF form.
In particular, we give a slight improvement over the trivial
redundancy algorithm and give some complexity results about some
problems related to finding Irredundant Equivalent Subsets
(I.E.S.) of 2CNF formulae. The problems of checking whether a
2CNF formula has a unique I.E.S. and checking whether a clause in
is all its I.E.S.'s are polynomial. Checking whether a 2CNF
formula has an I.E.S. of a given size and checking whether a
clause is in some I.E.S.'s of a 2CNF formula are polynomial or
NP-complete depending on whether the formula is cyclic. Some
results about Horn formulae are also reported.

@article{libe-08,
title = {Redundancy in Logic II: 2CNF and Horn Propositional
Formulae},
year = {2008},
author = {Liberatore, Paolo},
journal = {Artificial Intelligence},
pages = {265--299},
number = {2--3},
volume = {172},
}

doi: 10.1016/j.artint.2007.06.003