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

• arxiv url: http://arxiv.org/abs/2607.10880v2
• Date: Fri, 17 Jul 2026 09:06:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-20 13:50:44.091462
• Title: First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
• Title（参考訳）: HOLにおける第1次モーダル論理--自明な信心を持つ深浅と浅浅の埋め込み(拡張プレプリント)
• Authors: Christoph Benzmüller, Daniel Kirchner,
• Abstract要約: Isabelle/HOLは、深層埋め込み、重量級最大浅層埋め込み、軽量の極小浅層埋め込みである。 中心的な技術的貢献は、(可算)下向きのルウェンハイム・スコレム定理の定数領域クリプケ意味論の下でのFMLの機械化である。
• 参考スコア（独自算出の注目度）: 0.08594140167290099
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings of FML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim-Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals -- where the locale's variable assignment, having countable domain V = nat, cannot be surjective onto the domain -- and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers.
• Abstract（参考訳）: 我々は、Isabelle/HOLにおいて、命題から一階のモーダル論理(FML)まで、定数ドメインKripkeセマンティクスを用いて、これまでの研究の深層・浅層埋め込み手法を拡張した。 古典的高階論理(HOL)へのFMLの3つの埋め込みは、ディープ埋め込み、ヘビーウェイトな最大浅層埋め込み、軽量なミニマル浅層埋め込みである。 最小シャロー埋め込みはイザベル/HOLローカリーズとして表現され、アクセシビリティ関係、世界インデックスの解釈、世界の宇宙、変数割り当てによってパラメトリクスされる。 中心的な技術的貢献は、(可算)下向きのレーヴェンハイム・スコレムの定理(英語版)(Löwenheim-Skolem theorem)の、定数領域のクリプケ意味論の下でのFMLの機械化である。 最小シャローローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカ展開カローカローカローカローカローカローカローカローカローカローカローカ展開カローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカローカ展開 先行研究は命題の断片のみを扱うため、第一次量化器に必要な置換機械(自由/有界変量述語、新変数関数、キャプチャー回避置換、アルファベット名変更、置換可能性述語、置換補題、サイズに基づく帰納原理)を開発する。

関連論文リスト

• How Useful is Causal Invariance for Domain Adaptation in Finite-Sample Settings? [58.740078141879984]
  機械学習モデルは、トレーニングされたソースディストリビューションとは異なるターゲットディストリビューションにデプロイされると、しばしば劣化する。 因果関係に基づく領域一般化における最近の研究は、共用因果構造が不変な予測因子を誘導する方法を示している。 本稿では,完全あるいは部分的な因果知識が,教師付きドメイン適応を確実に改善できるかどうかについて検討する。
  論文  参考訳（メタデータ） (2026-06-10T21:07:49Z)
• A Measure-Theoretic Analysis of Reasoning: Structural Generalization and Approximation Limits [17.425526755350948]
  離散軌跡を計量空間に投影し、領域シフトを定量化する。 カントロビッチ双対性を呼び起こすと、アーキテクチャ上のリプシッツ連続性と汎関数近似極限によるOOD一般化が成立する。
  論文  参考訳（メタデータ） (2026-05-19T15:00:51Z)
• Granular Ball Guided Stable Latent Domain Discovery for Domain-General Crowd Counting [19.18297173252027]
  そこで本研究では,一般群集カウントのためのグラニュラーボールガイド型安定潜時ドメイン探索フレームワークを提案する。 提案手法はまず, サンプルをコンパクトな局所粒状球体に分類し, 擬似ドメインを推論する代表として粒状球体をクラスタ化する。 検出された潜在ドメインの上に,伝達可能な意味表現を改善する2分岐学習フレームワークを開発する。
  論文  参考訳（メタデータ） (2026-03-25T09:12:35Z)
• A Geometrically-Grounded Drive for MDL-Based Optimization in Deep Learning [3.2452107817263003]
  本稿では,MDL(Minimum Description Length)の原理を深層ニューラルネットワークのトレーニング力学に根本的に統合する,新しい最適化フレームワークを提案する。 我々は、数値安定性(Theoremrefthm:stability)と凸性仮定の下での指数収束(Theoremrefthm:convergence_rate)の保証とともに、$O(N log N)$ per-iteration complexity(Theoremrefthm:complexity)の実用的な計算効率のアルゴリズムを提供する。 この研究は、より自律的で、一般化可能で、解釈可能なAIへの原則化された道を提供する
  論文  参考訳（メタデータ） (2026-03-12T08:31:00Z)
• Maximizing Local Entropy Where It Matters: Prefix-Aware Localized LLM Unlearning [15.968499313464408]
  本研究では,時間的・語彙的両面にわたる局所的なエントロピー目標によって駆動されるPALU(Prefix-Localized Unlearning)を提案する。 PALUは、最先端のベースラインに比べて、忘れることの有効性と実用性を維持するのに優れている。
  論文  参考訳（メタデータ） (2026-01-06T17:10:48Z)
• StyDeSty: Min-Max Stylization and Destylization for Single Domain Generalization [85.18995948334592]
  単一のドメインの一般化(単一DG)は、単一のトレーニングドメインからのみ見えないドメインに一般化可能な堅牢なモデルを学ぶことを目的としている。 最先端のアプローチは、主に新しいデータを合成するために、敵対的な摂動やスタイルの強化といったデータ拡張に頼っている。 データ拡張の過程で、ソースと擬似ドメインのアライメントを明示的に考慮したemphStyDeStyを提案する。
  論文  参考訳（メタデータ） (2024-06-01T02:41:34Z)
• Constrained Maximum Cross-Domain Likelihood for Domain Generalization [14.91361835243516]
  ドメインの一般化は、複数のソースドメイン上で一般化可能なモデルを学ぶことを目的としている。 本稿では,異なる領域の後方分布間のKL偏差を最小限に抑える新しい領域一般化法を提案する。 Digits-DG、PACS、Office-Home、MiniDomainNetの4つの標準ベンチマークデータセットの実験は、我々のメソッドの優れたパフォーマンスを強調している。
  論文  参考訳（メタデータ） (2022-10-09T03:41:02Z)
• A Theory of Label Propagation for Subpopulation Shift [61.408438422417326]
  ラベル伝搬に基づくドメイン適応のための有効なフレームワークを提案する。 アルゴリズム全体でエンドツーエンドの有限サンプル保証を得る。 理論的なフレームワークを、第3のラベルなしデータセットに基づいたソースからターゲットへの転送のより一般的な設定に拡張します。
  論文  参考訳（メタデータ） (2021-02-22T17:27:47Z)
• Learning Invariant Representations and Risks for Semi-supervised Domain Adaptation [109.73983088432364]
  半教師付きドメイン適応(Semi-DA)の設定の下で不変表現とリスクを同時に学習することを目的とした最初の手法を提案する。 共同で textbfLearning textbfInvariant textbfRepresentations と textbfRisks の LIRR アルゴリズムを導入する。
  論文  参考訳（メタデータ） (2020-10-09T15:42:35Z)
• Log-Likelihood Ratio Minimizing Flows: Towards Robust and Quantifiable Neural Distribution Alignment [52.02794488304448]
  そこで本研究では,対数様比統計量と正規化フローに基づく新しい分布アライメント手法を提案する。 入力領域の局所構造を保存する領域アライメントにおいて,結果の最小化を実験的に検証する。
  論文  参考訳（メタデータ） (2020-03-26T22:10:04Z)

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

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