  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.
