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