Towards Multi-Clause Automated Deduction and Theorem Generation: Constructing and Applying Standard Contradictions

Trustworthy AI requires reasoning systems that are both powerful and transparent. Automated Reasoning (AR) is central to formal reasoning, yet classical binary resolution is limited: each step handles only two clauses and removes at most two literals. To move beyond this bottleneck, the concepts of standard contradiction and contradiction-separation-based deduction were introduced in 2018. This paper extends that framework by systematically constructing and applying standard contradictions for multi-clause deduction and automated theorem generation. We focus on two key forms—the maximum triangular and triangular-type standard contradictions—and present methods for building them. Using these structures, we develop a procedure to test the satisfiability of clause sets and derive formulas to count the sub-contradictions they contain. These results establish a foundation for dynamic multi-clause automated deduction and theorem generation, expanding the expressive and deductive reach of reasoning systems beyond the classical binary paradigm.