关键词: 命题逻辑, 矛盾体, 矛盾体的复合性质, 不可满足性

Abstract: Artificial Intelligence (AI) is a discipline that simulates some thinking processes and intelligent behaviors of human beings with computers. The resolution principle in automatic reasoning is a concise, reliable and complete reasoning rule. The contradiction separation based dynamic multi-clause synergized automated deduction is not only a crucial extension of resolution principle, but also has higher deductive efficiency. Due to the complex structure of contradictions and fewer generation strategies, the paper proposes different strategies for compounding the partial clauses of two or more contradictions on the basis of the dynamic deduction reliability theorem and completeness theorem of contradictions, which provides an effective method for the construction of contradictions.

Key words: propositional logic;contradiction;compound , properties of contradictions;unsatisfiability