Fugu-MT 論文翻訳(概要): A Coq Formalization of Unification Modulo Exclusive-Or

論文の概要: A Coq Formalization of Unification Modulo Exclusive-Or

arxiv url: http://arxiv.org/abs/2502.09225v1
Date: Thu, 13 Feb 2025 11:51:37 GMT
ステータス: 翻訳完了
システム内更新日: 2025-02-14 13:46:57.368487
Title: A Coq Formalization of Unification Modulo Exclusive-Or
Title（参考訳）: 統一モデュロ排他的手法のコク形式化
Authors: Yichi Xu, Daniel J. Dougherty, Rose Bohrer,
Abstract要約: 我々は、XOR-ユニフィケーション、すなわち排他的あるいは排他的理論の統一化に焦点をあてる。証明アシスタントCoqでは,XOR統一問題を解くアルゴリズムを実装している。我々はプログラミング言語OCamlの実装を得る。
参考スコア（独自算出の注目度）: 0.0
License:
Abstract: Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml.
Abstract（参考訳）: 等式統一は、自動定理証明やセキュリティプロトコル分析など、多くの分野において重要な問題である。本稿では,XOR-ユニフィケーション,すなわち排他的あるいは排他的理論の統一化に焦点をあてる。この理論には、結合性、可換性、Nilpotency、アイデンティティの存在という性質を持つ作用素が含まれる。証明アシスタントCoqでは,Lu と Lynch にインスパイアされた XOR 統一問題を解くアルゴリズムを実装し,音,完全,終端の証明を行う。 Coqのコード抽出機能を使って、プログラミング言語OCamlの実装を得る。

関連論文リスト

VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
論文参考訳（メタデータ） (2024-12-11T19:17:28Z)
Mitigating Misleading Chain-of-Thought Reasoning with Selective Filtering [59.495717939664246]
大規模言語モデルは、複雑な問題を解くためにチェーン・オブ・ソート(CoT)推論技術を活用することで、顕著な能力を示した。本稿では,選択フィルタリング推論(SelF-Reasoner)と呼ばれる新しい手法を提案する。 SelF-ReasonerはScienceQA、ECQA、LastLetterタスクに対して、微調整されたT5ベースラインを一貫して改善する。
論文参考訳（メタデータ） (2024-03-28T06:28:35Z)
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)
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions [0.0]
インダクティブ・コンストラクションの計算におけるオラクル計算可能性とチューリング再現性の概念を総合的に展開する。通常、合成手法では、メタレベル関数に基づいたオラクル計算の定義を用いる。チューリングの再現性は上半格子を形成し、決定可能性を持ち、真理値の再現性よりも厳密に表現可能であることを示す。
論文参考訳（メタデータ） (2023-07-28T13:16:46Z)
Complex Query Answering on Eventuality Knowledge Graph with Implicit Logical Constraints [48.831178420807646]
我々は、EVentuality中心のKGに基づいて、ニューラルネットワークを利用して複雑な論理的クエリに応答する新しいフレームワークを提案する。複合事象性クエリ・アンサーリング(CEQA)は、時間的順序と事象の発生を規定する暗黙の論理的制約を考察する。また、CEQAタスク上での最先端のニューラルクエリエンコーダの性能を大幅に向上させるメモリ拡張クエリ(MEQE)を提案する。
論文参考訳（メタデータ） (2023-05-30T14:29:24Z)
A Formalization of Operads in Coq [0.0]
本稿では,証明アシスタントであるCoqで操作された関数の形式化について論じる。 CoqはV-SPELLS内でのメタ言語開発のための公式な数学的基盤を提供する。私たちの研究は、私たちの知る限りでは、重要な自動化を備えた証明アシスタント内でのオペラッドの初めての公式化も提供しています。
論文参考訳（メタデータ） (2023-03-15T19:29:40Z)
Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
ヒルベルト空間全体の部分空間への発展を制限する混合作用素を構築するための枠組みを提案する。我々は,「ワンホット」状態の部分空間を保存するために設計された「XY」ミキサーを,多くの計算基底状態によって与えられる部分空間の一般の場合に一般化する。我々の分析は、現在知られているよりもCXゲートが少ない"XY"ミキサーのトロタライズも有効である。
論文参考訳（メタデータ） (2022-03-11T17:19:26Z)
Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文参考訳（メタデータ） (2022-03-03T10:07:32Z)
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens [0.7614628596146599]
依存型理論の構成的設定において有限一階満足度(FSAT)を研究する。非論理的記号の1階署名に応じて、FSATの完全な分類を行います。全ての結果は, 合成不決定性の増大するCoqライブラリの枠組みで機械化されている。
論文参考訳（メタデータ） (2021-04-29T16:05:31Z)
From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
論文参考訳（メタデータ） (2020-06-05T10:56:52Z)
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory [0.0]
従属型理論の構成的設定における有限一階満足度(FSAT)について検討する。非論理的記号の1階のシグネチャによって、FSATの完全な分類を与える。全ての結果は、合成不決定性証明の増大するCoqライブラリーの枠組みで機械化されている。
論文参考訳（メタデータ） (2020-04-15T23:26:04Z)

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