Fugu-MT 論文翻訳(概要): Experiments with Choice in Dependently-Typed Higher-Order Logic

論文の概要: Experiments with Choice in Dependently-Typed Higher-Order Logic

arxiv url: http://arxiv.org/abs/2410.08874v1
Date: Fri, 11 Oct 2024 14:49:45 GMT
ステータス: 処理完了
システム内更新日: 2024-10-30 21:26:05.864484
Title: Experiments with Choice in Dependently-Typed Higher-Order Logic
Title（参考訳）: 依存型高階論理における選択実験
Authors: Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk,
Abstract要約: ヒルベルトの不定選択作用素 $epsilon$ により DHOL 項構造を拡張する。選択項のHOL選択への変換を定義し、既存のDHOLからHOLへの変換を拡張する。選択を必要とするHOL問題に対する拡張翻訳の評価を行った。
参考スコア（独自算出の注目度）: 3.072340427031969
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator $\epsilon$, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.
Abstract（参考訳）: 最近、DHOLと呼ばれる高階論理の拡張が導入され、言語を依存型で豊かにし、強力な拡張型理論を生み出した。本稿では,DHOLに選択を付加する方法を2つ提案する。我々は、ヒルベルトの不定選択作用素$\epsilon$によりDHOL項構造を拡張し、選択項のHOL選択への変換を定義し、既存のDHOLからHOLへの変換を拡張し、翻訳の延長が完全であることを示し、音性について議論する。我々は最終的に、選択を必要とするHOL問題の集合に対する拡張翻訳を評価する。

関連論文リスト

Intensional FOL: Many-Sorted Extension [0.0]
IFOLで使用される概念は、それらをソートされた属性のリストに関連付けており、そのソートもインテンショナルな概念である。非ソートIFOL(Intensional FOL)を多ソートIFOLに拡張する要件は主に、自然言語が暗黙的に多ソートであるという事実に基づいている。
論文参考訳（メタデータ） (2024-09-03T19:50:57Z)
Multilingual Contrastive Decoding via Language-Agnostic Layers Skipping [60.458273797431836]
対照的なレイヤ(DoLa)によるデコーディングは、大規模言語モデルの生成品質を改善するために設計されている。このアプローチは英語以外のタスクではうまくいきません。モデルの前方通過における言語遷移に関する従来の解釈可能性の研究から着想を得て,改良されたコントラスト復号アルゴリズムを提案する。
論文参考訳（メタデータ） (2024-07-15T15:14:01Z)
Towards Effective Disambiguation for Machine Translation with Large Language Models [65.80775710657672]
我々は「あいまいな文」を翻訳する大規模言語モデルの能力について研究する。実験の結果,提案手法はDeepLやNLLBといった最先端システムと5つの言語方向のうち4つで一致し,性能を向上できることがわかった。
論文参考訳（メタデータ） (2023-09-20T22:22:52Z)
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint [0.0]
高階論理 HOL は、型付きデータ構造を表現および推論するための非常に単純な構文と意味論を提供します。依存型理論はそのようなリッチな型システムを提供するが、HOLとはかなり概念的な違いがある。本稿では,HOLのスタイルと概念的枠組みを維持した,依存型拡張DHOLを提案する。
論文参考訳（メタデータ） (2023-05-24T17:40:54Z)
FOLIO: Natural Language Reasoning with First-Order Logic [147.50480350846726]
我々は、自然言語(NL)における推論のための人間注釈付き、論理的に複雑で多様なデータセットであるFOLIOを提示する。 FOLIOは1,430の例(一意の結論)で構成され、それぞれが487の前提のうちの1つと組み合わせて、それぞれの結論の妥当性を導出的に推論する。 NL推論とNL-FOL変換の両方において、複数の最先端言語モデルをベンチマークする。
論文参考訳（メタデータ） (2022-09-02T06:50:11Z)
A unified logical framework for explanations in classifier systems [10.256904719009471]
本稿では,二項入力分類器とその性質の推論を支援するセテリスパリバスの性質のモーダル言語を提案する。我々は、モデルの族を研究し、言語の濃度に関する2つの証明システムとしてそれを公理化し、我々の公理学の完全性を示す。我々は、この言語を利用して反実的条件を定式化し、帰納的、対照的な、反実的説明を含む様々な説明概念を定式化する。
論文参考訳（メタデータ） (2021-05-30T07:49:56Z)
Superposition with Lambdas [59.87497175616048]
匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
論文参考訳（メタデータ） (2021-01-31T13:53:17Z)
Proof-theoretic aspects of NL$\lambda$ [0.0]
論理式 NL$lambda$ の証明理論解析について述べる。証明ネットの新しい計算を導入し、論理学の逐次計算に関して、それが健全で完備であることを証明する。 2つの形式主義で提案される自然言語分析には,予期せぬ収束があることが示されている。
論文参考訳（メタデータ） (2020-10-23T08:13:39Z)
Constructing a Family Tree of Ten Indo-European Languages with Delexicalized Cross-linguistic Transfer Patterns [57.86480614673034]
我々は,デレクシカル化転送を,解釈可能なツリー・ツー・ストリングパターンとツリー・ツー・ツリーパターンとして定式化する。これにより、言語間移動を定量的に探索し、第二言語習得の問い合わせを拡張することができる。
論文参考訳（メタデータ） (2020-07-17T15:56:54Z)
Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文参考訳（メタデータ） (2020-05-05T12:10:21Z)

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