論文の概要: Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)

• arxiv url: http://arxiv.org/abs/2609.07345v2
• Date: Wed, 09 Sep 2026 18:16:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-11 14:47:34.261183
• Title: Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
• Title（参考訳）: HOLにおけるモナディック二階述語論理--自動化された信心(拡張プレプリント)による深度と浅度
• Authors: Christoph Benzmueller, Daniel Kirchner,
• Abstract要約: Isabelle/HOLでは、先行研究のディープ・アンド・シャロー埋め込み手法をモナディック二階述語論理に適用する。 3つの埋め込みが並行して開発され、深層埋め込み、最大浅層埋め込み、最小浅層埋め込みである。 中心的な貢献は、完全に機械化された2階下方へのローウェンハイム・スコレムの定理である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments explicitly; and a minimal-shallow embedding -- a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus -- capture-avoiding substitution, renaming, and a substitution lemma per namespace -- in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and largely automated. Our central contribution is a fully mechanised two-sorted downward Loewenheim-Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading validates strictly more formulas, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 2-colorability are refuted throughout.
• Abstract（参考訳）: Isabelle/HOLでは、先行研究のディープ・アンド・シャロー埋め込み手法をモナディック二階述語論理(MSO)に適用する。 ディープ埋め込み(明示的な満足度関係を持つインダクティブデータ型)、接続子と量化子を直接HOLに変換する最大シュロー埋め込み(英語版)、解釈と両方の代入を明示的に持参する最小シュロー埋め込み(英語版)、これらのパラメータを修正するローカライズ(英語版) -- 式型をブールに分解するローカライズ)である。 新規成分の有効化は、2種類の置換装置 -- キャプチャー回避置換、リネーム、名前空間ごとの置換レムマ -- であり、各バインダーが他方に対して透過的であり、3つの埋め込みの忠実さは機械化され、大部分が自動化されている。 最小の埋め込みは(可算)代入範囲に対する深い妥当性を回復し、この範囲相対的な読影は MSO の一般(ヘンキン型)読影と一致することを示す。 いずれの読影も最小限の埋め込みから復元され、認識された解釈でのみ異なる:これら全ては一般的な読影のためのものであり、標準の完全なモデルの基本的な部分構造のみである。 ブール閉包とグラフスキーマは、完全な2階のドメインの下に保持されるが、最小の埋め込みでは失敗し、二分法は具体化され、到達性と2色性は全会一致で否定される。

関連論文リスト

• Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
  汎用的なテキスト埋め込みはそのようなタスクに広くデプロイされているが、意味的類似性は意味的に似ているがタスク固有の例を示すことができる。 本稿では,凍結したテキスト埋め込み上に構築された幾何正規化モジュールであるPGCL(Prototype-Guided Contrastive Learning)を紹介する。
  論文  参考訳（メタデータ） (2026-08-15T13:19:25Z)
• First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint) [0.08594140167290099]
  Isabelle/HOLは、深層埋め込み、重量級最大浅層埋め込み、軽量の極小浅層埋め込みである。 中心的な技術的貢献は、(可算)下向きのルウェンハイム・スコレム定理の定数領域クリプケ意味論の下でのFMLの機械化である。
  論文  参考訳（メタデータ） (2026-07-12T19:03:54Z)
• LimiX-2M: Mitigating Low-Rank Collapse and Attention Bottlenecks in Tabular Foundation Models [56.999481798138625]
  LimiX-2Mは2Mパラメータモデルであり、広く使われているベンチマークでTabPFN-v2とTabICLのベースラインを上回っている。 本稿では,強力なタブラル基礎モデル(TFM)のための統一トークン化・ルートフレームワークを提案する。 その結果、TFMにおける精度-効率トレードオフを改善するキーレバーとして、バリューアウェアトークン化とリードアウト整列ルーティングが強調された。
  論文  参考訳（メタデータ） (2026-06-03T06:07:33Z)
• Latent Reasoning via Sentence Embedding Prediction [41.06552269338159]
  本稿では,次の文の連続的な埋め込みを自動回帰予測することにより,事前訓練されたトークンレベルのLMを文空間内での操作に適応させるフレームワークを提案する。 以上の結果から,事前学習したLMは,遅延埋め込み空間内での抽象的構造的推論に効果的に移行できることが示唆された。
  論文  参考訳（メタデータ） (2025-05-28T10:28:35Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Repetition Improves Language Model Embeddings [86.71985212601258]
  「echo Embeddings」は、自動回帰言語モデルをアーキテクチャの変更や微調整を必要とせず、強力なテキスト埋め込みモデルに変換する。 我々のゼロショット埋め込みは、マスク付き言語モデリングトレーニングを施した双方向変換LMで得られたものとほぼ一致します。
  論文  参考訳（メタデータ） (2024-02-23T17:25:10Z)
• Out-of-Manifold Regularization in Contextual Embedding Space for Text Classification [22.931314501371805]
  空間の残りの部分を見つけ、正規化するための新しいアプローチを提案します。 実際に観察された単語から得られた2つの埋め込みに基づいて, アウトオブマニフォールド埋め込みを合成する。 判別器は、入力埋め込みがマニホールド内に位置するかどうかを検出するように訓練され、同時に、ジェネレーターは、容易にマニホールド外として識別できる新しい埋め込みを生成するように最適化される。
  論文  参考訳（メタデータ） (2021-05-14T10:17:59Z)

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

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