Abstract: Automatic reasoning constitutes a critical research domain in artificial intelligence,where inference rules play a pivotal role in determining its efficiency.Deductive reasoning based on the separation of contradictions represents a reliable and complete inference rule,offering advantages such as multi-literal collaboration,multi-clause integration,and dynamic deduction.The construction method of contradictions significantly impacts the efficiency of deduction.In light of this,this paper first introduces a type of contradiction structure grounded in propositional logic,i.e.,multi-line standard contradictions,and elaborates on the compound strategies for such contradictions under various scenarios.Specifically,it outlines the conditions and methods for generating new standard contradictions by leveraging two multi-line standard contradictions,while distinguishing between common and characteristic conclusions regarding their compound properties.Secondly,the paper highlights that incorporating specific literals into clauses can transform multi-line standard contradictions into more streamlined linear standard contradictions,providing lite-rals addition strategies tailored to such contradictions.Additionally,an algorithm for generating multi-line standard contradictions within propositional logic is designed.Finally,the structure and properties of double-line contradictions and complete standard contradictions based on first-order logic are presented.

Key words: Propositional logic, First-order logic, Standard contradiction, Multi-lines standard contradiction, Composite strategy, Literals addition strategy