Redundancy in logic I: CNF propositional formulae

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},
 }