論文の概要: An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction

• arxiv url: http://arxiv.org/abs/2511.04092v1
• Date: Thu, 06 Nov 2025 06:03:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-07 20:17:53.32505
• Title: An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
• Title（参考訳）: 矩形標準コントラディションに基づく理論基礎を持つ自動定理発生装置
• Authors: Yang Xu, Peiyao Liu, Shuwei Chen, Jun Liu,
• Abstract要約: 本稿では,新しい自動定理生成理論とツールを提案する。 それは初めて、長方形標準矛盾と呼ばれる新しい論理構造を定義し、証明する。 この理論を実装するために、効率的なテンプレートベースのATGアルゴリズムが設計されている。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 現在、非自明で論理的に妥当な定理を体系的に生成する厳密な理論体系が欠如している。 本稿では,この限界に対処し,新しい自動定理生成理論とツールを提案する。 本稿では, 独特な導出的優位性を持つ標準矛盾の概念に基づいて, 初めて, 矩形標準矛盾と呼ばれる新しい論理構造を定義し, 証明する。 この構造を中心に、完全な自動定理生成(ATG)理論が提唱されている。 理論的な証明は、長方形標準矛盾の2つのコア特性を明らかにしている: 第一に、標準矛盾(必要十分ではない)、第二に、非冗長性を示す(残りの節集合は、任意の節を取り除いた後に満足できる)。 これらの性質を利用することで、矩形標準矛盾を前提部分集合$A$に分割し、その補集合$H$の否定を証明し、妥当な定理$A \vdash \neg H$を形成することができ、そのような定理はすべて論理的に同値である。 この理論を実現するために、効率的なテンプレートベースのATGアルゴリズムを設計し、矩形自動定理生成器を開発した。 この研究により、機械は「検証者」から「発見者」へ移行し、論理学と人工知能の分野における基礎研究のための新たな道を開くことができる。

関連論文リスト

• Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction [11.18154335347018]
  この研究は、矛盾分離の内部機構を形式化し拡張する一般化された矛盾構築アルゴリズムである拡張三角法(ETM)を提示する。 理論的抽象化と運用実装をブリッジすることで、EMMは矛盾分離パラダイムを、自動化推論のための一般化されたスケーラブルで実用的な競合モデルに進化させる。
  論文  参考訳（メタデータ） (2025-10-12T17:03:33Z)
• Contradictions [9.602468627573215]
  本稿では,標準矛盾を体系的に構築することに焦点を当てる。 本稿では,最大標準矛盾による節集合の満足度と不満足度を決定する手法を提案する。 最大三角形標準矛盾と三角型標準矛盾の両方に埋め込まれた標準部分矛盾の数を計算するための公式を導出する。
  論文  参考訳（メタデータ） (2025-09-07T13:47:51Z)
• Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
  本稿では, 自己参照プロセスの安定な結果が, システムと環境との非有界リビジョン対話のユニークな平衡と同一であることを示すことによって, アルペイ・アルゲブラに寄与する。 固定点論、ゲームセマンティクス、順序解析、型理論から概念を統一することにより、この研究は無限の自己参照システムについての推論において、広くアクセス可能で形式的に厳密な基礎を確立する。
  論文  参考訳（メタデータ） (2025-07-25T13:12:55Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Theorem-Validated Reverse Chain-of-Thought Problem Generation for Geometric Reasoning [53.13514542825493]
  TRCoT(Theorem-d Reverse Chain-of-Thought Reasoning Synthesis)フレームワークについて述べる。 最初の段階であるTR-Engineは、構造的な記述と性質を持つ定理基底幾何学図を合成する。 第2段階であるTR-Reasonerは、幾何特性と記述フラグメントを交互に検証することで、反復的に質問と回答のペアを洗練するためのリバース推論を採用している。
  論文  参考訳（メタデータ） (2024-10-23T13:58:39Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• The unstable formula theorem revisited via algorithms [18.557423328068122]
  既存の学習モデルのギャップに対応するために,確率的最終補正(PEC)と呼ばれる新しい統計学習モデルを導入する。 このモデルの観点からLittlestone(stable)クラスを特徴付けます。 頻繁な定義の観点からリトルストーンクラスの特徴づけを得るため、多くの既存近似アルゴリズムに共通する点を強調する同値定理を構築した。
  論文  参考訳（メタデータ） (2022-12-09T18:53:34Z)
• Deriving Theorems in Implicational Linear Logic, Declaratively [0.0]
  命題直観主義線形論理の含意的断片において、与えられた大きさのすべての定理を生成する方法を示す。 応用として、線形論理定理証明器の正確性とスケーラビリティ試験のためのデータセットを生成し、定理証明問題に取り組むニューラルネットワークのトレーニングデータを生成する。
  論文  参考訳（メタデータ） (2020-09-22T00:48:45Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。