論文の概要: Superposition with Delayed Unification
- arxiv url: http://arxiv.org/abs/2403.04775v1
- Date: Thu, 29 Feb 2024 11:35:49 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-18 06:29:47.022255
- Title: Superposition with Delayed Unification
- Title(参考訳): 遅延統一による重ね合わせ
- Authors: Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson,
- Abstract要約: 飽和に基づく証明システムでは、統一は原子と見なされている。
また、ユニフィケーションを計算レベルに移動させ、統一アルゴリズムのステップを推論に変換することもできる。
一階重ね合わせは、統一規則を計算レベルに移す際にも完備であることを示す。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.
- Abstract(参考訳): 古典的には、飽和に基づく証明システムでは、統一は原子と見なされてきた。
しかし、統一アルゴリズムのステップを推論に変換することで、ユニフィケーションを計算レベルに移すこともできる。
大きなあるいは無限のユニファイア集合を返す統一手順に依存する計算学では、ユニフィケーションを計算学に統合することは、ユニフィケーションと推論を包含する魅力的な方法である。
これは例えば、交流重ね合わせや高次重ね合わせに適用される。
一階重ね合わせは、統一規則を計算レベルに移す際にも完備であることを示す。
我々は、標準的な一階重ね合わせにおいても得られる利点について論じ、実験的な評価を提供する。
関連論文リスト
- Denoising Distillation Makes Event-Frame Transformers as Accurate Gaze Trackers [61.44701715285463]
本稿では,イベントデータとフレームデータの両方を用いた受動的視線推定の問題に取り組む。
本質的に異なる生理構造を考えると、与えられた状態に基づいて正確に推定することは困難である。
我々は、現在の状態からいくつかの事前登録されたアンカー状態への状態遷移の定量化として、視線推定を再構成する。
論文 参考訳(メタデータ) (2024-03-31T03:30:37Z) - Range-Restricted Interpolation through Clausal Tableaux [0.0]
一階述語論理の入力からクレイグの出力へ、範囲制限とホーン特性の変動がどのように受け継がれるかを示す。
証明システムは、一階ATPに由来するクラウスアル・タドーである。
論文 参考訳(メタデータ) (2023-06-06T10:42:40Z) - Computing the action ground state for the rotating nonlinear
Schr\"odinger equation [6.6772808699409705]
回転非線形シュリンガー方程式に対する作用基底状態の計算について考察する。
フォーカスの場合、制約を単純化する問題の等価な定式化を同定する。
デフォーカスの場合、制約のない最小化によって基底状態が得られることを示す。
論文 参考訳(メタデータ) (2022-03-12T09:15:27Z) - E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
逐次的変化検出のための基本的かつ汎用的なフレームワークを開発する。
私たちの手順は、平均走行距離のクリーンで無症状な境界が伴います。
統計的および計算効率の両方を達成するために,これらの混合物を設計する方法を示す。
論文 参考訳(メタデータ) (2022-03-07T17:25:02Z) - On the Benefits of Large Learning Rates for Kernel Methods [110.03020563291788]
本稿では,カーネル手法のコンテキストにおいて,現象を正確に特徴付けることができることを示す。
分離可能なヒルベルト空間における2次対象の最小化を考慮し、早期停止の場合、学習速度の選択が得られた解のスペクトル分解に影響を及ぼすことを示す。
論文 参考訳(メタデータ) (2022-02-28T13:01:04Z) - On the Convergence of Stochastic Extragradient for Bilinear Games with
Restarted Iteration Averaging [96.13485146617322]
本稿では, ステップサイズが一定であるSEG法の解析を行い, 良好な収束をもたらす手法のバリエーションを示す。
平均化で拡張した場合、SEGはナッシュ平衡に確実に収束し、スケジュールされた再起動手順を組み込むことで、その速度が確実に加速されることを証明した。
論文 参考訳(メタデータ) (2021-06-30T17:51:36Z) - Certifying Multilevel Coherence in the Motional State of a Trapped Ion [0.38813406044213633]
単一の捕捉されたイオンの3つの運動的フォック状態のコヒーレント重ねが実験的に証明されている。
このことは、高レベルのコヒーレンスを単純な非理想的制御法で検証し、検証できることを証明している。
論文 参考訳(メタデータ) (2021-06-24T12:05:29Z) - Superposition with Lambdas [59.87497175616048]
匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。
推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
論文 参考訳(メタデータ) (2021-01-31T13:53:17Z) - Thermal rectification through a nonlinear quantum resonator [0.0]
低次元量子系における温度補正観測に必要な条件を同定する。
整合性を高めるために、ラムシフトをどのように活用できるかを示す。
強い結合体制は、弱い結合体制から派生した境界に違反することを可能にする。
論文 参考訳(メタデータ) (2021-01-26T11:55:24Z) - Zeroth-Order Hybrid Gradient Descent: Towards A Principled Black-Box
Optimization Framework [100.36569795440889]
この作業は、一階情報を必要としない零次最適化(ZO)の反復である。
座標重要度サンプリングにおける優雅な設計により,ZO最適化法は複雑度と関数クエリコストの両面において効率的であることを示す。
論文 参考訳(メタデータ) (2020-12-21T17:29:58Z) - Convergence of Gradient Algorithms for Nonconvex $C^{1+\alpha}$ Cost
Functions [2.538209532048867]
勾配が収束する副生成物を示し、収束率に明示的な上限を与える。
これにより、ドオブマルティンの超ガレ収束定理によるほぼ確実な収束を証明できる。
論文 参考訳(メタデータ) (2020-12-01T16:48:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。