| The simplification of logical formula in propositional logic is one of the important research directions in the field of computer science and artificial intelligence.With the increasing complexity of practical problems,the number of redundant literals and redundant clauses in the propositional logic clause sets is also increasing.When solving by computer,it will occupy a lot of computing time and storage space,which will seriously affect the efficiency of solving.Eliminating the redundancy of logical formulas can not only effectively improve the calculation efficiency,but also simplify the knowledge base and make the knowledge is easier to understand.Therefore,it is of great significance to eliminate redundant literals and redundant clauses in the clause set.This paper studies the redundant literals and redundant clauses of a special kind of clause set-ternary clause set in the propositional logic system.The main research work is as follows.1.Based on the academic idea of literal classification,the ternary clause set is classified according to the relevant definitions and properties of redundant literal.According to the characteristics of each kind of ternary clause set,the discrimination methods of necessary literal,useful literal and useless literal in the ternary clause set are given,and these discrimination methods are explained through specific examples.Finally,these discrimination methods are extended to the k-ary clause set.At the same time,for a special class of ternary clause set,an algorithm to determine redundant literal is designed.2.Drawing on the academic idea of clause classification,ternary clause sets are classified according to the related concepts and properties of redundant clauses.According to the different structural forms of ternary clause sets,the discriminative methods of redundant clauses in ternary clause sets are classified,and these discrimination methods are explained through specific examples.Finally,these discriminative methods are extended to the k-ary clause set and for a special class of ternary clause set,an algorithm for determining redundant clauses is designed. |
