論文の概要: 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ライブラリの枠組みで機械化されています。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Faithful Logical Reasoning via Symbolic Chain-of-Thought [39.94884827166363]
  シンボリック表現と論理規則をChain-of-Thoughtプロンプトと統合するフレームワークであるSymbCoTを提案する。 我々は、SymbCoTがCoT法よりも大幅に改善されていることを示す。 これは、論理的推論のために記号表現と規則をCoTに結合する最初の方法である。
  論文  参考訳（メタデータ） (2024-05-28T16:55:33Z)
• 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)
• LeanReasoner: Boosting Complex Logical Reasoning with Lean [19.486080494198724]
  大規模言語モデル(LLM)は、論理的不整合とそのような推論の固有の難しさのために、複雑な論理的推論に苦しむことが多い。 これらの課題に対処するために、定理実証フレームワークであるLeanを使用します。 論理的推論問題をリーン内の定理にフォーマルにすることで、対応する定理を証明または証明することで、それらを解決することができる。
  論文  参考訳（メタデータ） (2024-03-20T05:29:06Z)
• 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)
• Beyond Chain-of-Thought, Effective Graph-of-Thought Reasoning in Language Models [74.40196814292426]
  本稿では,人間の思考過程をチェーンとしてだけでなく,グラフとしてモデル化するグラフ・オブ・ソート(GoT)推論を提案する。 GoTは人間の思考の連続しない性質を捉え、思考プロセスのより現実的なモデリングを可能にします。 テキストのみの推論タスクとマルチモーダル推論タスクでGoTの性能を評価する。
  論文  参考訳（メタデータ） (2023-05-26T02:15:09Z)
• 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)
• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory [0.0]
  従属型理論の構成的設定における有限一階満足度(FSAT)について検討する。 非論理的記号の1階のシグネチャによって、FSATの完全な分類を与える。 全ての結果は、合成不決定性証明の増大するCoqライブラリーの枠組みで機械化されている。
  論文  参考訳（メタデータ） (2020-04-15T23:26:04Z)

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

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