論文の概要: Implementing the First-Order Logic of Here and There

• arxiv url: http://arxiv.org/abs/2601.03848v1
• Date: Wed, 07 Jan 2026 12:08:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-09 02:15:23.494578
• Title: Implementing the First-Order Logic of Here and There
• Title（参考訳）: 当地における一階論理の実装
• Authors: Jens Otten, Torsten Schaub,
• Abstract要約: ここでは、この一階述語論理に対する自動定理証明器について述べる(HT)。 これらは、HTの論理とHTの論理を直観論理に公理的に埋め込むためのネイティブシーケント計算に基づいている。 すべてのプローバーは、一階式の大きなベンチマークセットで評価される。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.
• Abstract（参考訳）: ここでは、この一階述語論理に対する自動定理証明器(HT)を提案する。 これらは、HTの論理とHTの論理を直観論理に公理的に埋め込むためのネイティブシーケント計算に基づいている。 逐次計算における解析的証明探索は自由変数とスコレム化を用いて最適化される。 埋め込みは直観論的一階述語論理のシーケント、表、接続計算と組み合わせて用いられる。 すべてのプローバーは、より効率的なHTプローバーの開発の基礎となる、一階式の大きなベンチマークセットで評価される。

関連論文リスト

• Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics [0.0]
  我々は,ホルン論理の規則を用いて,カルテシアン圏の対象を推論するための前方連鎖法と正規形式アルゴリズムを開発した。 また、一階述語論理の多階述語理論、文脈、断片化をサポートするために一階述語統一を適応する。
  論文  参考訳（メタデータ） (2025-04-27T18:02:02Z)
• FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference [0.9048611509540079]
  論理的推論の一次元順序付け問題を解くシステムを開発した。 自然言語の前提と候補文を一階述語論理に変換する。 BIGbenchの論理推論タスクでは100%の精度を実現し、AR-LSATの構文的に単純化されたサブセットでは88%の精度を実現している。
  論文  参考訳（メタデータ） (2025-02-12T13:58:42Z)
• Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
  カリキュラムベースの論理認識型チューニングフレームワークであるLACTを提案する。 具体的には、任意の一階論理クエリをバイナリツリー分解によって拡張する。 広く使われているデータセットに対する実験では、LATは高度な手法よりも大幅に改善(平均+5.5% MRRスコア)し、新しい最先端技術を実現している。
  論文  参考訳（メタデータ） (2024-05-02T18:12:08Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
  論理的な記号や表現をテキストで理解し、答えにたどり着くよう提案します。 このような論理的情報に基づいて,文脈拡張フレームワークとデータ拡張アルゴリズムを提案する。 本手法は最先端の性能を実現し,論理駆動コンテキスト拡張フレームワークとデータ拡張アルゴリズムの両方が精度向上に寄与する。
  論文  参考訳（メタデータ） (2021-05-08T10:09:36Z)
• Superposition with Lambdas [59.87497175616048]
  匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。 推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
  論文  参考訳（メタデータ） (2021-01-31T13:53:17Z)
• RNNLogic: Learning Logic Rules for Reasoning on Knowledge Graphs [91.71504177786792]
  本稿では知識グラフに基づく推論のための論理規則の学習について研究する。 論理規則は、予測に使用されるときに解釈可能な説明を提供するとともに、他のタスクに一般化することができる。 既存の手法は、検索スペースの検索の問題や、スパース報酬による非効率な最適化に悩まされている。
  論文  参考訳（メタデータ） (2020-10-08T14:47:02Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。 計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
  論文  参考訳（メタデータ） (2020-05-05T12:10:21Z)
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
  本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。 実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
  論文  参考訳（メタデータ） (2020-02-02T16:07:15Z)

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

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