論文の概要: A Cyclic Proof System for HFLN

• arxiv url: http://arxiv.org/abs/2010.14891v3
• Date: Thu, 12 Aug 2021 07:22:03 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-02 05:37:39.369061
• Title: A Cyclic Proof System for HFLN
• Title（参考訳）: HFLNの周期的証明システム
• Authors: Mayuko Kori, Takeshi Tsukada and Naoki Kobayashi
• Abstract要約: 循環的証明システムにより、明示的な帰納的推論なしに帰納的推論を行うことができる。 本稿では,自然数と交互に固定点を持つ高階述語論理であるHFLNの巡回証明システムを提案する。 循環証明システムの潜在的な応用は、高次プログラムの半自動検証である。
• 参考スコア（独自算出の注目度）: 2.281744214415521
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.'s recent work on reductions from program verification to HFLN validity checking.
• Abstract（参考訳）: 巡回証明システムにより、明示的な帰納法なしで帰納的推論を行うことができる。 本稿では,自然数と交互に固定点を持つ高階述語論理であるHFLNの巡回証明システムを提案する。 我々の知識は、高階論理のための最初の循環的証明システムである。 高次述語の存在と定点の交互化のため、我々の巡回証明システムは、ブロザストンとシンプソンの当初のシステムよりもより繊細な大域的条件を必要とする。 我々は,本システムの大域的条件と健全性を確認することの判定可能性を証明するとともに,循環証明システムの無限変種に対する標準完全性の制限形式を証明した。 小林らが最近行ったプログラム検証からhfln妥当性チェックへの削減に関する研究に基づく、高次プログラムの半自動検証が、循環的証明システムの潜在的な応用である。

関連論文リスト

• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
  本稿では,メルクル木包摂証明のためのOR論理に基づく新しい証明集約手法を提案する。 木内の葉の数に依存しない証明サイズを実現し、有効な葉のハッシュ1つを用いて検証を行う。 提案手法は,ゼロ知識証明システムのスケーラビリティ,効率,柔軟性を著しく向上させる可能性がある。
  論文  参考訳（メタデータ） (2024-05-13T17:15:38Z)
• Causal Layering via Conditional Entropy [85.01590667411956]
  因果発見は、生成した観測可能なデータから観測されていない因果グラフに関する情報を回収することを目的としている。 我々は、条件付きエントロピーオラクルを介してデータにアクセスすることによって、グラフの階層化を回復する方法を提供する。
  論文  参考訳（メタデータ） (2024-01-19T05:18:28Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)
• LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
  LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。 LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
  論文  参考訳（メタデータ） (2022-12-20T18:06:03Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Renormalization method for proving frustration-free local spin chains are gapped [0.0]
  スピン鎖が隙間があることを示すために、厳密な再正規化法を導入する。 このアプローチは、ギャップを持つ系の基底状態が崩壊する相関を示すという事実を利用する。 提案手法を適用し, 従来確立されていた手法が不確定であった場合でも, 2つの興味深いモデルがギャップを埋められ, 証明が完了したことを示す。
  論文  参考訳（メタデータ） (2021-11-17T19:37:22Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)
• Proof Complexity of Symbolic QBF Reasoning [6.85316573653194]
  OBDD(Ordered Binary Decision Diagrams)を用いたQBF(Quantified Boolean Formulas)のシンボリック証明システムの導入と検討 これらのシステムは記号量子化子除去を行うqbfソルバをキャプチャし、有界パス幅と量子化子複雑性の公式の短い証明を与える。 我々は,通信複雑性から既知の下限を取り除く戦略抽出に基づく記号的qbf証明システムのための下限手法を開発した。
  論文  参考訳（メタデータ） (2021-04-06T15:01:56Z)

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

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