Research Redundancy Of Set Of Clauses In Propositional Logic

Detection and elimination of redundant clauses from propositional formulas in conjunctive normal form (CNF) is a fundamental problem with numerous application domains, including AI, and has been the subject of extensive research. Based on these existing researches, this paper will further discuss the redundancy clauses and redundancy literal of propositional logic. The main results of this paper are as follows:1. The clauses can be divided into three types:irredundant clauses, relatively redundant clauses and absolute redundant clauses. Some equivalent descriptions of three types of clauses for a particular set of clauses were given respectively. Let S be a set of clauses in propositional logic, C∈Sred, C is relatively redundant with respect to S if and only if there exists an irredundant equivalent subset S’of S, such that S’\{C}｜≠C; C is absolute redundant with respect to S if and only if S and S\{C} have same irredundant equivalent subset.2. Some equivalent propositions about redundancy clauses in set of clauses were presented when propositional logic formula implies a literal. Let S be a set of clauses which implies a literal l, if the clause C∈S does not contain l, then C is redundant in S if and only if it is redundant in (S\S(l))∪{l}. In further, we also give some equivalent propositions about the set of clauses which contain some redundant literals, and present some equivalent description of redundant literal. Suppose S={Cl,C2,…,Cn,D} is a set of clauses in propositional logic, D=x∨D1, and S’={D1,×,C1,C2,…, Cn}, then the literal x is redundant within D inSif and only if the clause Dl is redundant with respect to S’.3. This paper also discussed the relationships between the satisfiable core and minimally unsatisfiable subset of set of clauses with the redundancy of set of clauses. With the concept of satisfiability, this work proposed one judgment method of the redundancy clause and redundancy literal. That is, let S={C1,C2,…,Cn,D} be a set of clauses in propositional logic, where D does not contains any complementary literal. Then, D is a redundant clause with respect to S if and only if S’={C1,C2,…,Cn}∪D is unsatisfiable. On the other side, if D=x∨D1, then x is a redundant literal within the D in S if and only if the set of clauses{x,C1,C2,…,Cn}∪D1is unsatisfiable.