## Redundancy in logic I: CNF propositional formulae

**Paolo Liberatore**
*Artificial Intelligence*

A knowledge base is redundant if it contains parts that can be
inferred from the rest of it. We study some problems related to
the redundancy of a CNF formula. In particular, any CNF formula
can be made irredundant by deleting some of its clauses: what
results is an irredundant equivalent subset. We study the
complexity of problems related to irredundant equivalent subsets:
verification, checking existence of an irredundant equivalent
subset with a given size, checking necessary and possible
presence of clauses in irredundant equivalent subsets, and
uniqueness. We also consider the problem of redundancy with
different definitions of equivalence.

@article{libe-05-c,
title = {Redundancy in logic I: CNF propositional formulae},
year = {2005},
author = {Liberatore, Paolo},
journal = {Artificial Intelligence},
pages = {203--232},
number = {2},
volume = {163},
}

doi: 10.1016/j.artint.2004.11.002