論文の概要: Trakhtenbrot's Theorem in Coq: Finite Model Theory through the
Constructive Lens
- arxiv url: http://arxiv.org/abs/2104.14445v1
- Date: Thu, 29 Apr 2021 16:05:31 GMT
- ステータス: 処理完了
- システム内更新日: 2021-04-30 17:28:39.185203
- Title: Trakhtenbrot's Theorem in Coq: Finite Model Theory through the
Constructive Lens
- Title(参考訳): coqにおけるtrakhtenbrotの定理:構成レンズによる有限モデル理論
- Authors: Dominik Kirst and Dominique Larchey-Wendling
- Abstract要約: 依存型理論の構成的設定において有限一階満足度(FSAT)を研究する。
非論理的記号の1階署名に応じて、FSATの完全な分類を行います。
全ての結果は, 合成不決定性の増大するCoqライブラリの枠組みで機械化されている。
- 参考スコア(独自算出の注目度): 0.7614628596146599
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We study finite first-order satisfiability (FSAT) in the constructive setting
of dependent type theory. Employing synthetic accounts of enumerability and
decidability, we give a full classification of FSAT depending on the
first-order signature of non-logical symbols. On the one hand, our development
focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as
the signature contains an at least binary relation symbol. Our proof proceeds
by a many-one reduction chain starting from the Post correspondence problem. On
the other hand, we establish the decidability of FSAT for monadic first-order
logic, i.e. where the signature only contains at most unary function and
relation symbols, as well as the enumerability of FSAT for arbitrary enumerable
signatures. To showcase an application of Trakthenbrot's theorem, we continue
our reduction chain with a many-one reduction from FSAT to separation logic.
All our results are mechanised in the framework of a growing Coq library of
synthetic undecidability proofs.
- Abstract(参考訳): 従属型理論の構成的設定における有限一階満足度(FSAT)について検討する。
可算性と決定可能性の総合的な説明を用いて、非論理記号の1次符号に依存するFSATの完全な分類を行う。
一方、我々の発展はトラクテンブロットの定理に焦点を合わせ、符号が少なくとも二項関係記号を含むと、FSATは決定不能であると述べた。
我々の証明はPost対応問題から始まる多くの還元鎖によって進行する。
一方、モナディックな一階述語論理に対する FSAT の決定可能性を確立する。
ここでは、シグネチャは、ほとんどの単項関数と関係シンボルと、任意のエヌマブルシグネチャに対するFSATのエヌマビリティのみを含む。
Trakthenbrot の定理の応用を実証するために、我々は FSAT から分離論理へ何度も還元された還元鎖を継続する。
すべての結果は、合成不確定性証明のcoqライブラリの枠組みで機械化されています。
関連論文リスト
- SymBa: Symbolic Backward Chaining for Multi-step Natural Language
Reasoning [6.961946145048321]
我々は,現在の後方連鎖実装の限界に対処するため,Symbic Backward Chaining(Symbolic Backward Chaining)を提案する。
SymBaでは、シンボリックトップダウンソルバが証明プロセス全体を制御し、LLMは、そのソルバがデッドエンドに遭遇したときのみ、単一の推論ステップを生成する。
この新しいソルバとLLMの統合により、SymBaは様々なマルチステップ推論ベンチマークにおいて、性能、証明忠実性、効率を大幅に改善する。
論文 参考訳(メタデータ) (2024-02-20T08:27:05Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [102.00359477458029]
本稿では,ニューラル・シンボリック統合法について述べる。
LLMフリーのシンボリック・ソルバを用いて、知識を用いた熟考的推論を行う。
論文 参考訳(メタデータ) (2023-11-16T11:26:21Z) - 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) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Superposition with Lambdas [59.87497175616048]
匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。
推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
論文 参考訳(メタデータ) (2021-01-31T13:53:17Z) - Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。
計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文 参考訳(メタデータ) (2020-05-05T12:10:21Z) - Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model
Theory [0.0]
従属型理論の構成的設定における有限一階満足度(FSAT)について検討する。
非論理的記号の1階のシグネチャによって、FSATの完全な分類を与える。
全ての結果は、合成不決定性証明の増大するCoqライブラリーの枠組みで機械化されている。
論文 参考訳(メタデータ) (2020-04-15T23:26:04Z) - Tensor Network Rewriting Strategies for Satisfiability and Counting [0.0]
#SATのインスタンスは、標準的な方法でテンソルネットワークとして表現できる。
3SAT や #P-complete のようなNP完全であることが知られているクラス、例えば #2SAT では、対応する書き換え規則がダイアグラムにハイパーエッジを導入している。
論文 参考訳(メタデータ) (2020-04-14T12:50:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。