Redundancy in Logic II: 2CNF and Horn Propositional Formulae

TL;DR

This paper investigates the computational complexity of redundancy problems in 2CNF and Horn propositional formulae, providing algorithms and complexity insights for checking redundancy and finding irredundant subsets.

Contribution

It offers new algorithms and complexity analyses for redundancy checking and irredundant subset identification in 2CNF and Horn formulae, highlighting the role of cyclicity.

Findings

Redundancy checking algorithms outperform trivial methods.

Complexity results depend on the concept of cyclicity.

Some results extend to Horn 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.