ECAI-2002 Conference Paper

[full paper]

The Complexity of Checking Redundancy of CNF Propositional Formulae

Paolo Liberatore

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.

Keywords: Knowledge Representation, Deduction, computational complexity

Citation: Paolo Liberatore: The Complexity of Checking Redundancy of CNF Propositional Formulae. In F. van Harmelen (ed.): ECAI2002, Proceedings of the 15th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2002, pp.262-266.