An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction

TL;DR

This paper introduces a new logical structure called rectangular standard contradiction and develops an automated theorem generation theory and tool based on it, advancing the capabilities of machines in logical discovery.

Contribution

It defines and proves the properties of rectangular standard contradiction and constructs a complete ATG theory with an efficient algorithm and tool.

Findings

Rectangular standard contradiction is necessarily unsatisfiable and non-redundant.

Partitioning a contradiction yields valid, equivalent theorems.

The developed tool enables machines to generate theorems autonomously.

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.