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

• URL: http://arxiv.org/abs/2511.04092v1
• Date: Thu, 06 Nov 2025 06:03:54 GMT
• Title: An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
• Authors: Yang Xu, Peiyao Liu, Shuwei Chen, Jun Liu,
• Abstract summary: This paper proposes a novel automated theorem generation theory and tool.<n>It defines and proves, for the first time, a new logical structure known as rectangular standard contradiction.<n>To implement this theory, an efficient template-based ATG algorithm is designed.
• Score: 8.21204701022347
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• Resolving Zadehs Paradox Axiomatic Possibility Theory as a Foundation for Reliable Artificial Intelligence [0.0]
  This work advances and substantiates the thesis that the resolution of this crisis lies in the domain of possibility theory.<n>The aim of this work is to demonstrate that possibility theory is not merely an alternative, but provides a fundamental resolution to DST paradoxes.
  arXiv  Detail & Related papers  (2025-12-04T21:13:16Z)
• Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction [11.18154335347018]
  This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation.<n>By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning.
  arXiv  Detail & Related papers  (2025-10-12T17:03:33Z)
• Contradictions [9.602468627573215]
  This paper focuses on the systematic construction of standard contradictions.<n>We propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction.<n>We derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction.
  arXiv  Detail & Related papers  (2025-09-07T13:47:51Z)
• Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
  This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process is identical to the unique equilibrium of an unbounded revision dialogue between a system and its environment.<n>By unifying concepts from fixed point theory, game semantics, ordinal analysis, and type theory, this research establishes a broadly accessible yet formally rigorous foundation for reasoning about infinite self referential systems.
  arXiv  Detail & Related papers  (2025-07-25T13:12:55Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Theorem-Validated Reverse Chain-of-Thought Problem Generation for Geometric Reasoning [53.13514542825493]
  We introduce a two-stage Theorem-d Reverse Chain-of-Thought Reasoning Synthesis (TRCoT) framework.<n>The first stage, TR-Engine, synthesizes theorem-grounded geometric diagrams with structured descriptions and properties.<n>The second stage, TR-Reasoner, employs reverse reasoning to iteratively refine question-answer pairs by cross-validating geometric properties and description fragments.
  arXiv  Detail & Related papers  (2024-10-23T13:58:39Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  Humans can develop new theorems to explore broader and more complex mathematical results. Current generative language models (LMs) have achieved significant improvement in automatically proving theorems. This paper proposes an Automated Theorem Generation benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems.
  arXiv  Detail & Related papers  (2024-05-05T02:06:37Z)
• The unstable formula theorem revisited via algorithms [18.557423328068122]
  In response to gaps in existing learning models, we introduce a new statistical learning model, called Probably Eventually Correct'' or PEC.<n>We characterize Littlestone (stable) classes in terms of this model.<n>In order to obtain a characterization of Littlestone classes in terms of frequent definitions, we build an equivalence theorem highlighting what is common to many existing approximation algorithms.
  arXiv  Detail & Related papers  (2022-12-09T18:53:34Z)
• Deriving Theorems in Implicational Linear Logic, Declaratively [0.0]
  We show how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. As applications, we generate datasets for correctness and scalability testing of linear logic theorem provers and training data for neural networks working on theorem proving challenges.
  arXiv  Detail & Related papers  (2020-09-22T00:48:45Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.