論文の概要: Circular Induction

• arxiv url: http://arxiv.org/abs/2605.24968v1
• Date: Sun, 24 May 2026 09:44:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-26 19:50:18.551685
• Title: Circular Induction
• Title（参考訳）: 循環誘導
• Authors: Dorel Lucanu, Grigore Rosu, Eugen Goriac, Georgiana Caltais,
• Abstract要約: この原理が帰納的証明手法の開発に有効であることを示す。 円周誘導は単純で柔軟性があり、汎用的であるため、異なる証明スキームを競合ツールに組み合わせるためのよい候補フレームワークである。 本稿では,円周法則を中心に構築された証明器であるCIRCにおける円周誘導の実施方法について述べる。
• 参考スコア（独自算出の注目度）: 0.05599792629509228
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Circularity Principle was successfully applied for developing a coinductive proving technique, known as circular coinduction. In this paper, we show that the same principle can be used to develop an inductive proving technique. A main advantage of this uniform approach is that the two proving techniques can be easily combined during the verification process. Circular induction is simple, flexible, generic, and therefore it is a good candidate framework for combining different proving schemes into a competitive tool. We exhibit this potential by presenting how the circular induction is implemented in CIRC, a prover built around the Circularity Principle. Disclaimer. This paper was written in 2010, at the time the CIRC prover was developed, and the main body reflects the state of the work and of the prover as of that date. For this arXiv technical report, only the related-work discussion (Section 6) and the concluding section have been revised: Section 6 has been extended to situate circular induction within the cyclic-proof and infinite-descent literature that has appeared or matured since 2010. No other part of the paper-its definitions, results, proofs, examples, or implementation description-has been modified, and the technical content should be read as a 2010 contribution. References to developments after 2010 appear only in the updated related-work section.
• Abstract（参考訳）: 円周原理(Circularity Principle)は円錐法として知られる造形的証明法の開発に成功している。 本稿では,帰納的証明手法の開発において,同じ原理が適用可能であることを示す。 この一様アプローチの主な利点は、2つの証明技法を検証プロセス中に簡単に組み合わせることができることである。 円周誘導は単純で柔軟性があり、汎用的であるため、異なる証明スキームを競合ツールに組み合わせるためのよい候補フレームワークである。 循環原理に基づいた証明器であるCIRCにおいて、円周誘導がどのように実装されているかを示すことで、この可能性を示す。 破壊者。 本論文は,CIRCエビデンサが開発された2010年に執筆され,本論文の本体は,その日時点の作業状況と証明者の状態を反映している。 このarXivテクニカルレポートでは,2010年以降に出現または成熟した循環型・無限大の文献において,循環型・無限大の円周誘導を満足させるよう,関連作業の議論(第6部)と結論節のみを改訂した。 ペーパーイットの定義、結果、証明、例、実装記述の他の部分は変更されておらず、技術的な内容は2010年のコントリビューションとして読むべきです。 2010年以降の開発に関する言及は、更新された関連作業セクションにのみ表示される。

関連論文リスト

• ARCHE: A Novel Task to Evaluate LLMs on Latent Reasoning Chain Extraction [70.53044880892196]
  本稿では、複雑な推論引数を標準推論パラダイムの組み合わせに分解し、Reasoning Logic Tree (RLT) という形で分解しなければならない、ARCHE(Latent Reasoning Chain extract)という新しいタスクを紹介する。 この作業を容易にするために,我々は,1,900以上の参照と38,000の視点を含む70のNature Communicationsの記事から得られた新しいベンチマークであるARCHE Benchをリリースする。 ARCHE Bench上での10のLLMの評価では、モデルがREAとECのトレードオフを示しており、完全な標準推論チェーンを抽出することはできません。
  論文  参考訳（メタデータ） (2025-11-16T07:37:09Z)
• On the Emergence of Induction Heads for In-Context Learning [121.64612469118464]
  本研究では, 2層トランスにおいて以前に同定されたメカニズムである誘導ヘッドの出現について検討する。 最小限の ICL タスクの定式化と改良型トランスフォーマアーキテクチャを用いて,この構造の起源を説明する。
  論文  参考訳（メタデータ） (2025-11-02T18:12:06Z)
• Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
  本稿では, 自己参照プロセスの安定な結果が, システムと環境との非有界リビジョン対話のユニークな平衡と同一であることを示すことによって, アルペイ・アルゲブラに寄与する。 固定点論、ゲームセマンティクス、順序解析、型理論から概念を統一することにより、この研究は無限の自己参照システムについての推論において、広くアクセス可能で形式的に厳密な基礎を確立する。
  論文  参考訳（メタデータ） (2025-07-25T13:12:55Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Pushing the Boundaries of Tractable Multiperspective Reasoning: A Deduction Calculus for Standpoint EL+ [2.9005223064604073]
  Standpoint EL は一般的な記述論理 EL のマルチモーダル拡張である。 本稿では,この定式化の表現性を推し進めることで,Standpoint EL+と呼ばれる拡張論理に到達できることを示す。 これは、原型的満足度チェックの推論計算を設計することで達成される。
  論文  参考訳（メタデータ） (2023-04-27T16:49:17Z)
• Real-time lattice gauge theory actions: unitarity, convergence, and path integral contour deformations [0.8702432681310401]
  星名、藤井、菊川(HFK)は先日、ウィルソン作用の離散化を連続実時間ゲージ理論に適用することはユニタリ理論に繋がらないことを指摘した。 本稿では,一元的リアルタイム転送行列を導出する別のリアルタイム格子ゲージ理論の作用を提案する。 実時間 U(1) と SU(3) 格子ゲージ理論の立証式モンテカルロ計算を行う。
  論文  参考訳（メタデータ） (2021-03-03T18:57:21Z)
• Coinduction Plain and Simple [0.0]
  コインダクション(Coinduction)とは、無限のストリームを定義する手法、いわゆるコデータ、およびコインダクテッド指定コデータの等価性を証明する技術である。 本稿では、まず、宣言型プログラミングにおける造語をレビューする。次に、コデータを特定するためによく使われる形式主義をレビューし、少し拡張する。第三に、元々は等式述語のみに規定されていた造語証明の原理を他の述語に一般化する。
  論文  参考訳（メタデータ） (2020-07-20T06:52:54Z)

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

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