The Study Of Redundancy Property Of Propositional Logic And First-order Logic

Simplifications of CNF(Conjunctive Normal Form)formulas are significant research content of propositional logic satisfiable problem(SAT)solving and first-order logic theorem proving,however,during the processing of simplifications,the correction and rationality of simplifications have to be guaranteed,therefore,redundancy research of CNF formulas of propositional logic and first-order logic is indispensable.It is full of meaningness no matter in theory or in application,analysis of the relationship of different parts of CNF formulas in propositional logic and first-order logic to identify the redundant property of variables,literals or clauses in CNF formulas.Profound research on redundancy properties of CNF formulas in propositional logic and first-order logic is mainly focused on in this dissertation,also related to those redundancy properties' applications.First of all,the relationship of different parts of CNF formuals in propositional logic and first-order logic is analyzed and multiple kinds of unified princiles of clause elimination are constructed.Soundess of theose unified principles of clause elimination have been proved;Besides,abundant clause elimination methods have been proposed according to those unified principles;What's more,properties of those clause elimination methods have been discussed.Finally,a part of clause elimination methods are implemented as procedures and optimized to validate the simplification effect of those clause elimination methods for propositional CNF formulas,as preprocessing techniques of propositional logic SAT solvers.The work of this dissertation is mainly as follows:Part 1,the unified principle of implication modulo resolution in propositional logic has been built,of which the soundness has been proved.Based on the unified principle,various clasue elimination methods have been proposed,meanwhile,the soundness of clause elimination methods also have been proved.Designing specific algorithms for those clause elimination methods,and evaluating the efficiency of those clause elimination methods as preprocessing techniques of propositional SAT solvers.Part 2,the unified principle called as multi-literal implication modulo resolution in propositional logic has been demonstrated and its soundness in propositional CNF formulas has been proved.Besides,diverse clause elimination methods have been created based on the principle,of which the soundness exist.Finally,the algorithm of set-blocked clause elimination has been designed,by modifying the mainstream algorithm framework of blocked clause elimination.Part 3,the unified principle equality implication modulo resolution adopted in first-order CNF formulas with equality has been constructed.Multiple clause elimination methods have been lifted in CNF formulas with equality,including equality resolution asymmetric validation clause elimination,equality resolution subsumption clause elimination and equality covered clause elimination.The soundness and two kinds of properties of those clause elimination methods have been discussed.Besides,the soundness of existing simplification methods predicate elimination and equality-blocked clause elimination can also be proved via the principle.Part 4,four types of novel redundant properties in first-order logic have been defined,set-blocked clause,extended set-blocked clause,equality-set-blocked clause and extended equality-set-blocked clause.The former two are redundant properties in CNF formulas without equality in first-order logic,while the latter two are redundant properties in CNF formulas with equality in first-order logic.The soundeness of the four redundant properties has been proved in corresponsive kinds of CNF formulas.What's more,the effectivess and confluence property of the four types of redundant properties have been discussed.Part 5,the two unified principles multi-literal implication modulo resolution and equality multi-literal implication modulo resolution in first-order logic have been constructed.The soundness of former is proved in CNF fomulas without equality in first-order logic has been proved,while the soundness of latter has been proved in CNF formulas with equality in first-order logic.The two principles are separately more effective than implication modulo resolution and equality implication modulo resolution,which has been proved.Under the framework of the two princples,various clause elimination methods have been proposed and compared with clause elimination methods under the principles implication modulo resolution and equality implication modulo resolution with respect to effiectiveness.In the end,the soundness of set-blocked clause elimination and equality-set-blocked clause elimination which have been proposed in Part 4 has been proved via multi-literal implication modulo resolution and equality multi-literal implication modulo resolution.