关键词: 冗余子句,冗余文字,无冗余等价子集,可满足性

Abstract: We mainly studied the redundancy of clause and literal in the propositional logic formula．Some equivalent descriptions of necessary,useful and useless clause for a particular set of clauses were given respectively,and the irredundant equivalent subsets of any set of clauses were discussed．In addition,an approach of identification of redundant literal was presented．At last,an equivalent condition of the redundancy clause was obtained by using the concept of satisfiability．These results serve as the theoretical foundation of a new method for simplifying the propositional logic formula.

Key words: Redundancy clause,Redundancy literal,Irredundant equivalent subset,Satisfiability