| Summary: | The resolution principle is a brief,reliable and complete inference rule in automated reasoning and the deductive theory of standard contradiction separation is an extension of binary resolution.Since the structure of the standard contradiction is very complex and there are few existing contradiction types and generation strategies,this paper first obtains multiple compound stra-tegies for generating new contradictions by compounding two or more contradictions based on the standard contradiction separation deduction theory in propositional logic.Then a kind of special standard contradiction structure,i.e.,composite regular stan-dard contradiction,is put forward to enrich the structural features of contradictions.Furthermore,the expandability of the diffe-rent clauses of the new contradictions obtained by compounding is discussed,which leads to corresponding literals adding strategies.Finally,algorithms for generating contradictions are proposed to provide a reference for further implementing the generation of new contradictions on computers.
|
|---|
