## The Complexity of Checking Redundancy of CNF Propositional
Formulae

**Paolo Liberatore**
*Proceedings of the Fifteenth European Conference on Artificial
Intelligence (ECAI 2002)*

A knowledge base is redundant if it contains parts that can be
inferred from the rest of it. We study the problem of checking
whether a CNF formula (a set of clauses) is redundant, that is,
it contains clauses that can be derived from the other ones. Any
CNF formula can be made irredundant by deleting some of its
clauses: what results is an irredundant equivalent subset
(I.E.S.) We study the complexity of some related problems:
verification, checking existence of a I.E.S. with a given size,
checking necessary and possible presence of clauses in I.E.S.'s,
and uniqueness.

@inproceedings{libe-02-c,
title = {The Complexity of Checking Redundancy of CNF
Propositional Formulae},
year = {2002},
author = {Liberatore, Paolo},
booktitle = {Proceedings of the Fifteenth European Conference on
Artificial Intelligence (ECAI 2002)},
pages = {262--266},
}

HTTP download.