Fugu-MT 論文翻訳(概要): Range-Restricted Interpolation through Clausal Tableaux

論文の概要: Range-Restricted Interpolation through Clausal Tableaux

arxiv url: http://arxiv.org/abs/2306.03572v2
Date: Mon, 24 Jul 2023 07:33:49 GMT
ステータス: 処理完了
システム内更新日: 2023-07-25 20:55:13.039282
Title: Range-Restricted Interpolation through Clausal Tableaux
Title（参考訳）: clausal tableaux による範囲制限補間
Authors: Christoph Wernhard
Abstract要約: 一階述語論理の入力からクレイグの出力へ、範囲制限とホーン特性の変動がどのように受け継がれるかを示す。証明システムは、一階ATPに由来するクラウスアル・タドーである。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.
Abstract（参考訳）: 一階述語論理におけるクレイグ補間(Craig interpolation)の出力への入力から、範囲制限のバリエーションとホーン特性の変換方法を示す。証明システムはclausal tableauxであり、一階のatpに由来する。この結果は、一般に証明変換によって達成できるクララザウ構造の制限によって誘導され、また、ソース証明が分解/パラモディフィケーションによっても得られる。主な用途は、クエリ合成と補間による再構成である。我々の方法論的アプローチは、高度に最適化された一階述語プローバーを組み込むことにより、証明構造上の操作を実現可能な実装の即時的な視点と組み合わせる。

関連論文リスト

Uncertainty Quantification with Bayesian Higher Order ReLU KANs [0.0]
本稿では,コルモゴロフ・アルノルドネットワークの領域における不確実性定量化手法について紹介する。簡単な一次元関数を含む一連の閉包試験により,本手法の有効性を検証した。本稿では,ある項を包含することで導入された機能的依存関係を正しく識別する手法の能力を実証する。
論文参考訳（メタデータ） (2024-10-02T15:57:18Z)
Formally Certified Approximate Model Counting [25.20597060311209]
本稿では、その出力近似の品質に関する保証を正式に保証した、近似モデルカウントのための最初の認証フレームワークを提案する。 i)Isabelle/HOL証明アシスタントにおけるアルゴリズムのPAC保証の静的かつ1回限りの公式な証明、(ii)証明証明書を用いた外部CNF-XORソルバに対するApproxMCの呼び出しの動的かつ1回実行による検証。
論文参考訳（メタデータ） (2024-06-17T11:02:04Z)
Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
本稿では,ニューラルネットワークトレーニングを安定化(大規模)するための原理的手法として,線形アヘッドの理論解析を提案する。最適化過程の不安定性は、しばしば損失ランドスケープの非単調性によって引き起こされるものであり、非拡張作用素の理論を活用することによって線型性がいかに役立つかを示す。
論文参考訳（メタデータ） (2023-10-20T12:45:12Z)
Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
論文参考訳（メタデータ） (2023-10-05T07:10:40Z)
Accelerated Cyclic Coordinate Dual Averaging with Extrapolation for Composite Convex Optimization [20.11028799145883]
複合凸最適化のための外挿法 (A-CODER) を用いた加速サイクル座標二元平均化法を提案する。 A-CODERは,前処理よりもブロック数に依存して最適な収束率が得られることを示す。目的関数の滑らかな成分が有限和形式で表現できるような設定では、A-CODERの分散還元変種であるVR-A-CODERを導入し、最先端の複雑性を保証する。
論文参考訳（メタデータ） (2023-03-28T19:46:30Z)
Understanding and Constructing Latent Modality Structures in Multi-modal Representation Learning [53.68371566336254]
優れたパフォーマンスの鍵は、完全なモダリティアライメントではなく、有意義な潜在モダリティ構造にある、と我々は主張する。具体的には,1)モダリティ内正規化のための深い特徴分離損失,2)モダリティ間正規化のためのブラウン橋損失,3)モダリティ内正規化およびモダリティ間正規化のための幾何学的整合損失を設計する。
論文参考訳（メタデータ） (2023-03-10T14:38:49Z)
Linearization Algorithms for Fully Composite Optimization [61.20539085730636]
本稿では,完全合成最適化問題を凸コンパクト集合で解くための一階アルゴリズムについて検討する。微分可能および非微分可能を別々に扱い、滑らかな部分のみを線形化することで目的の構造を利用する。
論文参考訳（メタデータ） (2023-02-24T18:41:48Z)
Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
最近のデータセットは、標準的なシーケンス・ツー・シーケンスモデルにおける体系的な一般化能力の欠如を露呈している。本稿では,セq2seqモデルの振る舞いを分析し,相互排他バイアスの欠如と全例を記憶する傾向の2つの要因を同定する。広範に使用されている2つの構成性データセット上で、標準的なシーケンス・ツー・シーケンスモデルを用いて、経験的改善を示す。
論文参考訳（メタデータ） (2022-11-28T17:36:41Z)
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving [0.0]
ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
論文参考訳（メタデータ） (2022-09-26T11:23:17Z)
GroupifyVAE: from Group-based Definition to VAE-based Unsupervised Representation Disentanglement [91.9003001845855]
他の誘導バイアスを導入しないと、VAEベースの非監視的非絡み合いは実現できない。グループ理論に基づく定義から導かれる制約を非確率的帰納的バイアスとして活用し,vaeに基づく教師なし不連続に対処する。提案手法の有効性を検証するために,5つのデータセット上で,vaeベースモデルが最も目立つ1800モデルをトレーニングした。
論文参考訳（メタデータ） (2021-02-20T09:49:51Z)
Partial Orders, Residuation, and First-Order Linear Logic [0.20305676256390934]
各列の先行式上の一意線型順序を定義するような部分順序制約を加えることで、多くの有用な論理作用素を定義できることを示す。
論文参考訳（メタデータ） (2020-08-14T13:06:21Z)

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