Dynamic Automated Deduction by Contradiction Separation: The Standard Extension Algorithm
Yang Xu, Xingxing He, Shuwei Chen, Jun Liu, Xiaomei Zhong
TL;DR
The paper tackles the bottleneck of binary, pairwise reasoning in traditional ATP systems by formalizing the Standard Extension (SE) as a concrete procedural realization of Contradiction Separation (CSE). SE dynamically constructs standard contradictions through complementary literal extensions, unifying satisfiability and unsatisfiability checks in propositional and first-order logic and establishing soundness and completeness. It provides a unified deduction framework that generalizes traditional resolution, supports extraction of satisfying assignments when formulas are satisfiable, and serves as the core of a lineage of successful CSE-based provers (e.g., CSE, CSE_E, CSI_E, CSI_Enig) that have repeatedly performed in CASC competitions. The empirical results, across CASC editions from 2018–2025, demonstrate robust, scalable multi-clause reasoning capable of handling equality and unification in large benchmarks, indicating SE’s practical impact for next-generation automated theorem proving and neurosymbolic integration.
Abstract
Automated deduction seeks to enable machines to reason with mathematical precision and logical completeness. Classical resolution-based systems, such as Prover9, E, and Vampire, rely on binary inference, which inherently limits multi-clause synergy during proof search. The Contradiction Separation Extension (CSE) framework, introduced by Xu et al. (2018), overcame this theoretical limitation by extending deduction beyond binary inference. However, the original work did not specify how contradictions are algorithmically constructed and extended in practice. This paper presents the Standard Extension algorithm, the first explicit procedural realization of contradiction separation reasoning. The proposed method dynamically constructs contradictions through complementary literal extension, thereby operationalizing the CSE theory within a unified algorithm for satisfiability and unsatisfiability checking. The algorithm's soundness and completeness are formally proven, and its effectiveness is supported indirectly through the performance of CSE-based systems, including CSE, CSE-E, CSI-E, and CSI-Enig in major automated reasoning competitions (CASC) in the last few years. These results confirm that the Standard Extension mechanism constitutes a robust and practically validated foundation for dynamic, multi-clause automated deduction.