The Study Of Standard Contradiction Based On Propositional Logic

Automatic reasoning is an interdisciplinary subject of mathematical logic and computer science,which has been widely applied in the fields of software and hardware,knowledge representation and knowledge reasoning,expert system,question answering system,semantic web,knowledge graph,model reasoning research in artificial intelligence,mathematical theorem proving and so on.Resolution is a simple,reliable and complete reasoning rule in automatic reasoning.After nearly half a century of development,a large number of researchers have done a lot of work based on binary resolution,which has effectively improved the efficiency of automatic reasoning based on resolution.The standard Contradiction Separation Rule is an important extension of the binary resolution,which overcomes the limitation that only two clauses involved in each deduction of the binary resolution,and the deletion rule is based on complementary pair of two clauses.For a given set of clauses,if the number of literals in the standard contradiction is larger and the spatial structure is more complex,then in the deductive process,after deleting the standard contradiction,the contradiction separation clauses is simpler,and the deductive result can be obtained more quickly,thus the efficiency of automatic reasoning can be improved.Therefore,the clearer we study the structure of standard contradiction,the more we can improve the efficiency of automatic reasoning based on the deductive theory of Contradiction Separation Rule.However,the research on the structure of standard contradiction is still rare.Based on the deductive theory of Contradiction Separation Rule in propositional logic,this paper has done the following work on the structure of standard contradiction:(1)This paper puts forward a kind of special standard contradiction,that is,complete standard contradiction,and studies some basic properties of complete standard contradiction.we study the strategy of adding literals to the original clauses set after adding clauses to the complete standard contradiction and the change rule of the non-expansibility of clauses in the new clauses set after adding clause and literals to the complete contradiction.According to the relevance between the literals in the new clause and the literals in the original complete standard contradiction,the new clauses are divided into five categories,each of which corresponds to different adding strategies and different non extensibility rules.(2)This paper propose the concept of minimum standard contradiction and obtain the corresponding properties and theorems.The laws of minimum standard contradiction after adding clauses and related literals to the complete standard contradiction be studied.Because there are five different strategies of adding clauses and related literals in the complete standard contradiction,there are five related presentation laws of minimum standard contradiction.(3)This paper proves that the minimum standard contradiction and the complete standard contradiction can be converted into each other by adding literals and clauses in theory and gives a variety of specific strategies for continuously constructing the complete standard contradiction based on the complete standard contradiction.