論文の概要: Optimistic Higher-Order Superposition

• arxiv url: http://arxiv.org/abs/2510.18429v1
• Date: Tue, 21 Oct 2025 09:05:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-25 03:08:13.218961
• Title: Optimistic Higher-Order Superposition
• Title（参考訳）: 最適高次重ね合わせ
• Authors: Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann,
• Abstract要約: 私たちは$lambda$-superposition calculusの"最適化"バージョンを紹介します。 節と共に格納された制約を使って爆発的な統一問題を遅らせ、より標的的な方法で機能拡張性を適用する。 証明器ではまだ実装されていないが、実例では、元の計算よりも優れているか、少なくとも有用に補完するであろうことを示唆している。
• 参考スコア（独自算出の注目度）: 39.146761527401424
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional extensionality axiom. In the present work, we introduce an "optimistic" version of $\lambda$-superposition that addresses these two issues. Specifically, our new calculus delays explosive unification problems using constraints stored along with the clauses, and it applies functional extensionality in a more targeted way. The calculus is sound and refutationally complete with respect to a Henkin semantics. We have yet to implement it in a prover, but examples suggest that it will outperform, or at least usefully complement, the original $\lambda$-superposition calculus.
• Abstract（参考訳）: $\lambda$-superposition calculus は高階公式の証明に成功している。 しかし、電卓のいくつかの部分は爆発的であり、特に高次ユニファイア列挙と機能的拡張性公理のためである。 この2つの問題に対処する$\lambda$-superpositionの"最適化"バージョンを紹介します。 具体的には, 節とともに格納された制約を用いて, 爆発的統一問題を遅延させ, より標的に機能的拡張性を適用した。 計算は、ヘンキンの意味論に関して、健全で難解に完備である。 証明器ではまだ実装していませんが、サンプルでは、オリジナルの$\lambda$-superposition calculusよりも優れているか、少なくとも役に立ちます。

関連論文リスト

• Non-Euclidean High-Order Smooth Convex Optimization [9.940728137241214]
  我々はH"より古い連続$q$-th微分を持つ凸対象の最適化のためのアルゴリズムを開発する。 提案アルゴリズムは,1leq pleq infty$ に対して $ell_p$-settings を含む,穏やかな条件下での一般ノルムに対して作用する。
  論文  参考訳（メタデータ） (2024-11-13T19:22:34Z)
• Tempered Calculus for ML: Application to Hyperbolic Model Embedding [70.61101116794549]
  MLで使用されるほとんどの数学的歪みは、本質的に自然界において積分的である。 本稿では,これらの歪みを改善するための基礎的理論とツールを公表し,機械学習の要件に対処する。 我々は、最近MLで注目を集めた問題、すなわち、ハイパーボリック埋め込みを「チープ」で正確なエンコーディングで適用する方法を示す。
  論文  参考訳（メタデータ） (2024-02-06T17:21:06Z)
• First and zeroth-order implementations of the regularized Newton method with lazy approximated Hessians [4.62316736194615]
  我々は一般の非自由$ノルムフリー問題のリップオーダー(ヘシアン-O)とゼロオーダー(微分自由)の実装を開発する。 また、アルゴリズムに遅延バウンダリ更新を加えて、これまで計算されたヘッセン近似行列を数回繰り返し再利用する。
  論文  参考訳（メタデータ） (2023-09-05T17:40:54Z)
• Superposition with Lambdas [59.87497175616048]
  匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。 推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
  論文  参考訳（メタデータ） (2021-01-31T13:53:17Z)
• High-Order Oracle Complexity of Smooth and Strongly Convex Optimization [31.714928102950584]
  非常に滑らかな (Lipschitz $k$-thorder derivative) 関数と強い凸関数を$k$-thorder Oracleへの呼び出しによって最適化する複雑性を考える。 我々は、関数を正確に$epsilon$まで最適化するために、固定された$k$で最悪の場合のオラクルの複雑さが$leftの順序にあることを証明している。
  論文  参考訳（メタデータ） (2020-10-13T19:18:15Z)
• Second-Order Information in Non-Convex Stochastic Optimization: Power and Limitations [54.42518331209581]
  私たちは発見するアルゴリズムを見つけます。 epsilon$-approximate stationary point ($|nabla F(x)|le epsilon$) using $(epsilon,gamma)$surimateランダムランダムポイント。 ここでの私たちの下限は、ノイズのないケースでも新規です。
  論文  参考訳（メタデータ） (2020-06-24T04:41:43Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。 計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
  論文  参考訳（メタデータ） (2020-05-05T12:10:21Z)

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

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