The Classification Of Set Of Clauses In Propositional Logic

Theorem mechanical proving aims at the building of computing systems that automate the process of proving theorems. Since the 1950s theorem automated proving has been become one of the active research topics of computer science and successfully used in mathematics, hardware test and verification, software generation and verification, protocol verification, and artificial intelligence. The detection and elimination of redundant clauses from prepositional formulas in automated theorem proving has been a vital issue in various applications. Based on existing researches, this paper focuses on the knowledge of clauses and literals in the propositional logic. Include the following aspects as the major achievements:1. The literals of set of clauses in propositional logic are divided into three categories, namely the necessary literals, useful literals and useless literals, the definition of three kinds of literals are presented respectively, The corresponding equivalent description methods are given respectively, and then discuss the relationship between the three literals. So as to obtain necessary literals are useful literals of set of clauses, useless literals are redundant literals.2. Based on the classification of literals of set of clauses, the discriminant method about the three literals are given. By using satisfiability of set of clauses then give the equivalent conditions about three literals and related satisfiability of set of clauses. The judgement theorem of literals of set of clauses are provided and design different algorithms.3. Study the property of the redundant clauses, the equivalence theorem of redundant clauses of propositional logic are provided, and then the related properties about useful clauses, necessary clauses and useless clauses are given. Based on the satisfiability of set of clause, a judgement method of redundant clauses of set of clauses including useful clauses, necessary clauses and useless clauses are given, and verified by practical example.