Fugu-MT 論文翻訳(概要): Superposition for Lambda-Free Higher-Order Logic

論文の概要: Superposition for Lambda-Free Higher-Order Logic

arxiv url: http://arxiv.org/abs/2005.02094v4
Date: Fri, 9 Apr 2021 10:29:29 GMT
ステータス: 処理完了
システム内更新日: 2022-12-06 14:26:45.865985
Title: Superposition for Lambda-Free Higher-Order Logic
Title（参考訳）: ラムダフリー高階論理の重ね合わせ
Authors: Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
Abstract要約: 本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
参考スコア（独自算出の注目度）: 62.997667081978825
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
Abstract（参考訳）: 本稿では, 意図的および拡張的クラス数$\lambda$-free高階論理に対して, 部分的応用と適用変数を許容する2つの定式化法を導入する。計算は完全単調でなくてもよい項順でパラメタ化され、$\lambda$-free高階語彙パスとKnuth-Bendix順序を使うことができる。 Zipperposition 証明器に計算を実装し,Isabelle/HOL および TPTP ベンチマークで評価した。彼らは完全な高階論理のための完全かつ高効率な自動定理プローバーへの踏み石として期待できるように見える。

関連論文リスト

FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
タスク分解を用いて問題空間をトラバースする新しい手法を提案する。我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
論文参考訳（メタデータ） (2024-10-14T19:39:11Z)
Higher-Order DisCoCat (Peirce-Lambek-Montague semantics) [0.0]
本稿では,高階DisCoCat(カテゴリー構成分布)モデルの新たな定義を提案する。私たちのモデルは、プリミティブが論理式ではなく文字列図形に作用する計算に基づいて、モンタギュー意味論の変種と見なすことができる。
論文参考訳（メタデータ） (2023-11-29T17:04:15Z)
LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文参考訳（メタデータ） (2023-10-23T17:58:40Z)
LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。 LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
論文参考訳（メタデータ） (2022-12-20T18:06:03Z)
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought [10.524051272257614]
大規模言語モデル(LLM)は、チェーン・オブ・シークレット・プロンプトが与えられた顕著な推論能力を示している。本稿では, PrOntoQAと呼ばれる合成質問応答データセットを提案し, それぞれの例を合成世界モデルとして生成する。これにより、生成された連鎖を形式解析の象徴的な証明に解析することができる。
論文参考訳（メタデータ） (2022-10-03T21:34:32Z)
Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
マッチングやアリティ向上の活性化関数を用いて,任意の論理を単一層で学習できることが示される。我々は,非ゼロパラメータの数を信念関数の有効アリティに直接関連付ける基礎を用いて,信念表を表現する。これにより、パラメータの間隔を誘導することで論理的複雑性を低減する最適化アプローチが開かれる。
論文参考訳（メタデータ） (2022-03-16T22:47:53Z)
Higher-order Derivatives of Weighted Finite-state Machines [68.43084108204741]
本研究では、重み付き有限状態機械の正規化定数に関する高次微分の計算について検討する。文献に記載されていないすべての順序の導関数を評価するための一般アルゴリズムを提案する。我々のアルゴリズムは以前のアルゴリズムよりもはるかに高速である。
論文参考訳（メタデータ） (2021-06-01T19:51:55Z)
Superposition with Lambdas [59.87497175616048]
匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
論文参考訳（メタデータ） (2021-01-31T13:53:17Z)
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)

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

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