An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
Yang Xu, Peiyao Liu, Shuwei Chen, Jun Liu
TL;DR
The paper addresses the lack of a rigorous theory for automatically generating non-trivial, logically valid theorems by introducing a new construct, the Rectangular Standard Contradiction, and proving its unsatisfiability and non-redundancy. It develops a complete Automated Theorem Generation (ATG) framework: from a generation literal set, a rectangular standard contradiction is built, and any partition into premises $A$ and hypothesis $H$ yields the theorem $A \vdash \neg H$, with all such theorems being logically equivalent. The authors advance a template-based ATG algorithm that decouples structure from content, enabling efficient generation of theorems, and implement a Rectangular ATG tool with public availability. This work shifts machines from mere verifiers to discoverers in logic and AI research, providing a foundation for automatic theorem discovery and future extension to first-order logic formulas.
Abstract
Currently, there is a lack of rigorous theoretical system for systematically generating non-trivial and logically valid theorems. Addressing this critical gap, this paper conducts research to propose a novel automated theorem generation theory and tool. Based on the concept of standard contradiction which possesses unique deductive advantages, this paper defines and proves, for the first time, a new logical structure known as rectangular standard contradiction. Centered on this structure, a complete Automated Theorem Generation (ATG) theory is put forward. Theoretical proofs clarify two core properties of rectangular standard contradiction: first, it is a standard contradiction (necessarily unsatisfiable); second, it exhibits non-redundancy (the remaining clause set becomes satisfiable after removing any clause). Leveraging these properties, this paper proves that partitioning a rectangular standard contradiction into a premise subset $A$ and negation of its complement $H$, a valid theorem $A \vdash \neg H$ can be formed, and all such theorems are logically equivalent. To implement this theory, an efficient template-based ATG algorithm is designed, and a Rectangular Automated Theorem Generator is developed. This research enables machines to transition from "verifiers" to "discoverers", opening up new avenues for fundamental research in the fields of logic and artificial intelligence.