On Contradictions Compound And Graphical Representation In Propositional Logic

Automatic reasoning is a significant branch in the field of artificial intelligence.Its main research directions include mechanical theorem proving,formal verification,requirement analysis verification,protocol verification and scientific management.The contradiction separation based dynamic multi-clause synergized automated deduction(referred to as theory of contradiction separation)is an extension of binary resolution.In the process of deductive reasoning,the contradiction is deduced as a whole,which offers efficient solution to the problems of binary resolution,including lengthy deductive process,unpronounced integrality,low resolution efficiency.Therefore,theory of contradiction separation has important research value in automatic reasoning.A contradiction is formed by the conjunction of several clauses,which are obtained through disjunctive operation of literals.Due to their complex structure,there are few wellknown types of contradictions and few methods for generating and discriminating contradictions,which results in the incomplete demonstration of the good performance of contradictions in automatic reasoning.Based on this,the research work of this paper is based on the reliability and completeness of the separation and deduction of contradictions,firstly,a new method of generating contradictions is proposed.Secondly,since the CNF formula(propositional logic formula)is associated with a directed bipartite graph,the directed bipartite graph is used to judge the contradiction of a special type of CNF formula.By compounding some clauses of two or more contradictions,this paper discusses the conditions required for generating contradictions,and the influence of propositional variables in compound clauses on the final structure of contradictions,so as to propose a new method for generating contradictions.Secondly,on the basis of the bipartite graph,the directed bipartite graph is defined and applied to judge the contradiction of the CNF formula,which shows that the CNF formulas associated with directed bipartite graphs of several special structures are contradictions.Finally,based on the theory proposed in this paper,the algorithm for generating contradictions is designed,which provides a reference for further generation of contradictions on the computer.