Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions

Yang Xu; Shuwei Chen; Hailin Guo; Jun Liu

cs.AIOct 30, 2026

Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions

Authors: Yang Xu, Shuwei Chen, Hailin Guo, Jun Liu

Organizations: School of Mathematics, Southwest Jiaotong University, Chengdu, 611756, China · National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu, 611756, Sichuan, China · School of Computing, Faculty of Computing, Engineering and the Built Environment, Ulster University, Belfast, Northern Ireland, United Kingdom

Abstract

Automated theorem generation (ATG) seeks to construct new theorems rather than merely prove given conjectures. Existing approaches typically generate candidate statements that require subsequent proof or formal verification. We propose a constructive framework for ATG in first-order logic based on triangular standard contradictions. The method constructs minimally unsatisfiable clause sets from selected first-order literals, then forms theorems by retaining some clauses as premises and taking the negation of one clause, or a conjunction of clauses, as the conclusion. Minimal unsatisfiability ensures that the remaining premises are satisfiable, avoiding trivial inference by explosion, while unsatisfiability of the full set guarantees the resulting entailment. Theorems are therefore correct by construction, without a separate proof procedure for each instance. Extending the previously developed $Δ_1$ generator, we introduce seven methods, $Δ_2$ -- $Δ_8$ , forming a unified family of eight theorem-generation methods. Four generators, $Δ_1$ -- $Δ_4$ , have been implemented and released. We also formulate a general $Δ$ -class method encompassing the family. Combinatorial analysis demonstrates the capacity to generate large numbers of distinct theorems systematically. This framework offers a principled foundation for automated theorem discovery and the construction of logically guaranteed knowledge.

Figures & tables

Panel of Figure 1 — Figure 1: Schematic representation of a triangular standard contradiction $\Pi(S)$ . Strictly speaking, the outer shape shown in the figure is a trapezoid; however, since its essential structure is triangular, we follow the established terminology and refer to it as triangular.

Panel of Figure 2 — Figure 2: A five-column triangular standard-contradiction example. The descending red line connects the generating-literal positions; the horizontal and vertical red segments indicate geometric placement and alignment. The lines do not represent logical operators or additional literals. The literals in each column form the disjuncts of the corresponding clause.

Panel of Figure 3 — Figure 3: Schematic representation of the full triangular standard contradiction underlying the $\Delta_{1}$ method.

Panel of Figure 4 — Figure 4: Schematic representation of a Type-I triangular sub-standard contradiction $\Pi(S)$ used in the $\Delta_{2}$ method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 5 — Figure 5: Schematic representation of a Type-II triangular standard contradiction $\Pi(S)$ used in the $\Delta_{3}$ method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 6 — Figure 6: Schematic representation of a Type-III triangular standard contradiction $\Pi(S)$ used in the $\Delta_{4}$ method. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 7 — Figure 7: Schematic representation of a Type-IV triangular standard contradiction $\Pi(S)$ used in the $\Delta_{5}$ method. The sets $L_{1}$ and $L_{2}$ represent the two parts of the literals distributed between $C_{n}$ and $C_{n+1}$ , respectively. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 8 — Figure 8: Schematic representation of a Type- $V(i)$ triangular standard contradiction $\Pi(S(i))$ used in the $\Delta_{6}(i)$ method, where $i\in\{n-1,\ldots,2\}$ . The sets $L_{1}$ and $L_{2}$ represent the two groups of literals separated at the index $i$ . The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 9 — Figure 9: Schematic representation of a Type- $VI(i)$ triangular standard contradiction $\Pi(S(i))$ used in the $\Delta_{7}(i)$ method, where $i\in\{n-1,\ldots,2\}$ . The sets $L_{1}=C_{i}\setminus\{x_{i}\}$ and $L_{2}=C_{n}\setminus\{x_{n}\}$ represent the two groups of complementary literals. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 10 — Figure 10: Schematic representation of a Type- $VII(i)$ triangular standard contradiction $\Pi(S(i))$ used in the $\Delta_{8}(i)$ method, where $i\in\{n-1,\ldots,2\}$ . The sets $L_{3}$ , $L_{4}$ , and $L_{5}$ represent the groups of literals distributed among $C_{n}$ , $C_{n+1}$ , and $C_{i}$ , respectively. The hatched region indicates the admissible region for interior literals according to Definition 4.1 .

Panel of Figure 11 — Figure 11: Schematic representation of the general construction of a minimally unsatisfiable clause set from a triangular standard contradiction. The literal $y$ has a predicate symbol that occurs nowhere else in the clause set.

First-Order Logic

See all 9 papers

Generative Logic: A Deterministic Reasoning Engine
Jul 25, 2025Nikolai SergeevAutomated Theorem Proving AI-Assisted Scientific Research
Generative Logic UG, Germany
A Minimal Agent for Automated Theorem Proving
Feb 27, 2026Borja Requena, Austin Letson, Krystian Nowakowski +2Large Language Model-Guided Theorem Proving Automated Theorem Proving
Axiomatic AI, Barcelona, Spain.
Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Jun 4, 2026Jui-Hui Chung, Ziyang Cai, Zihao Li +14Automated Theorem Proving Lean Theorem Proving
1Princeton Language and Intelligence, Princeton University · 2Amazon.

Jul 25, 2025J/K move · Enter open · S save

Generative Logic: A Deterministic Reasoning Engine

Nikolai Sergeev

Generative Logic UG, Germany

Automated Theorem Proving AI-Assisted Scientific Research

Open paper AskPDF arXiv

We present Generative Logic (GL), a deterministic computer architecture for automated mathematical reasoning. GL starts from axiomatic definitions written in a minimalist Mathematical Programming Language (MPL) and explores a configurable region of their deductive neighborhood. The definitions are compiled into a grid of Logic Blocks (LBs). An LB applies rules by hash-table lookups, and every statement it derives keeps its complete provenance. A run generates conjectures, removes those that counterexamples refute, tries to prove the rest, reduces the proved theorems to an essential core and writes every proof as navigable HTML. An independent verifier checks every proof step. From supplied definitions, GL derives the basic laws of Peano arithmetic and Gauss's summation formula. From previously proved lemmas, further definitions and a supplied list of conjectures, it builds a proof of the Fundamental Theorem of Arithmetic (FTA). These proofs are also exported to Lean 4 and checked by the Lean kernel. The next step is for GL to derive the FTA as well, without supplied conjectures. GL is designed together with a hardware architecture, the Mathematical Processing Unit (MPU).

Abstract

First-Order Logic

Explore similar work

Generative Logic: A Deterministic Reasoning Engine

A Minimal Agent for Automated Theorem Proving

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement