論文の概要: Proof-theoretic aspects of NL$\lambda$

• arxiv url: http://arxiv.org/abs/2010.12223v1
• Date: Fri, 23 Oct 2020 08:13:39 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-03 22:35:45.191328
• Title: Proof-theoretic aspects of NL$\lambda$
• Title（参考訳）: NL$\lambda$の証明論的側面
• Authors: Richard Moot (TEXTE, LIRMM, CNRS)
• Abstract要約: 論理式 NL$lambda$ の証明理論解析について述べる。 証明ネットの新しい計算を導入し、論理学の逐次計算に関して、それが健全で完備であることを証明する。 2つの形式主義で提案される自然言語分析には,予期せぬ収束があることが示されている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a proof-theoretic analysis of the logic NL$\lambda$ (Barker \& Shan 2014, Barker 2019). We notably introduce a novel calculus of proof nets and prove it is sound and complete with respect to the sequent calculus for the logic. We study decidability and complexity of the logic using this new calculus, proving a new upper bound for complexity of the logic (showing it is in NP) and a new lower bound for the class of formal language generated by the formalism (mildly context-sensitive languages extended with a permutation closure operation). Finally, thanks to this new calculus, we present a novel comparison between NL$\lambda$ and the hybrid type-logical grammars of Kubota \& Levine (2020). We show there is an unexpected convergence of the natural language analyses proposed in the two formalism. In addition to studying the proof-theoretic properties of NL$\lambda$, we greatly extends its linguistic coverage.
• Abstract（参考訳）: 我々は論理 nl$\lambda$ (barker \& shan 2014 barker 2019) の証明論的解析を行う。 特に,証明ネットの新たな計算法を導入し,論理のシークエント計算に関して健全かつ完備であることを証明した。 この新たな計算を用いて論理の決定可能性と複雑性について検討し、論理の複雑さに対する新しい上限(NPである)と形式主義によって生成される形式言語のクラスに対する新しい下位境界(置換クロージャ操作で拡張された文脈に敏感な言語)を証明した。 最後に,この新しい計算法により,nl$\lambda$ と kubota \& levine (2020) のハイブリッド型論理文法の比較を行った。 2つの形式論で提案された自然言語解析の予期せぬ収束があることを示す。 nl$\lambda$ の証明論的性質の研究に加えて、その言語的範囲を大きく広げた。

関連論文リスト

• A Theory of Interpretable Approximations [61.90216959710842]
  我々は、ある基底クラス $mathcalH$ の概念の小さな集合によってターゲット概念 $c$ を近似するという考え方を研究する。 任意の$mathcalH$と$c$のペアに対して、これらのケースのちょうど1つが成り立つ: (i) $c$を任意の精度で$mathcalH$で近似することはできない。 解釈可能な近似の場合、近似の複雑さに関するわずかに非自明なa-priori保証でさえ、定数(分布自由かつ精度)の近似を意味することを示す。
  論文  参考訳（メタデータ） (2024-06-15T06:43:45Z)
• $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof [0.0]
  それらを生成することができる文法の表現力に応じて言語を分類することは、計算言語学における根本的な問題である。 本稿では,各証明が検証された(すなわち,証明支援者によってチェックされる)アルゴリズムに繋がるかどうかを,MCFGを通して解析できるかどうかを体系的に研究する,計算的および証明理論的な視点から,既存の証明を解析する。
  論文  参考訳（メタデータ） (2024-05-15T14:51:11Z)
• 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)
• Simulating Structural Plasticity of the Brain more Scalable than Expected [69.39201743340747]
  Rinkeらは、Barnes-Hutアルゴリズムの変種を用いて、現在のハードウェア上で最大10億のニューロンに対して構造的可塑性をシミュレートするスケーラブルなアルゴリズムを導入した。 アルゴリズムを慎重に検討すると、理論ランタイムは$O(n log2 n)$と分類できる。
  論文  参考訳（メタデータ） (2022-10-11T09:02:43Z)
• A Logic-Based Framework for Natural Language Inference in Dutch [1.0178220223515955]
  オランダ語文ペア間の関係を導出するための枠組みを提案する。 提案するフレームワークは、推論ラベルにつながる検査可能な証明を生成するために、論理ベースの推論に依存している。 我々は最近作成されたオランダの自然言語推論データセットの推論パイプラインを評価する。
  論文  参考訳（メタデータ） (2021-10-07T10:34:46Z)
• 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)
• The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus [0.0]
  ランベク・グリシン計算に基づく木に隣接した言語の証明論的特徴付けを行う。 純粋に構造的な結合性、有用性、HLGの証明ネットに関するグラフ理論的議論など、いくつかの新しい手法が証明に導入されている。
  論文  参考訳（メタデータ） (2021-01-10T22:28:05Z)
• RNNs can generate bounded hierarchical languages with optimal memory [113.73133308478612]
  RNNは、自然言語構文の足場を反映した境界階層言語を効率的に生成できることを示す。 Dyck-($k$,$m$)は、よくネストされた括弧($k$型)と$m$バウンドされたネスト深さの言語である。 明示的な構成により,$O(m log k)$ hidden units の RNN がメモリの指数的削減に十分であることを示す。
  論文  参考訳（メタデータ） (2020-10-15T04:42:29Z)
• Neural Proof Nets [0.8379286663107844]
  本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
  論文  参考訳（メタデータ） (2020-09-26T22:48:47Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。 計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
  論文  参考訳（メタデータ） (2020-05-05T12:10:21Z)

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

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