論文の概要: Faithful Logic Embeddings in HOL -- A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level

• arxiv url: http://arxiv.org/abs/2502.19311v1
• Date: Wed, 26 Feb 2025 17:08:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-27 14:56:24.093171
• Title: Faithful Logic Embeddings in HOL -- A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level
• Title（参考訳）: Fithful Logic Embeddings in HOL -- 深くて浅い、自動化され、インタラクティブで、重くて軽い、証明と反例、メタとオブジェクトのレベル。
• Authors: Christoph Benzmüller,
• Abstract要約: 本稿では,古典的高階論理における深層・浅層埋め込みの同時配置法を提案する。 このアプローチは論理学の教育、研究、応用に役立ちます。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various automated reasoning tools in recent years. This paper presents a recipe for the simultaneous deployment of different forms of deep and shallow embeddings in classical higher-order logic, enabling not only flexible interactive and automated theorem proving and counterexample finding at meta and object level, but also automated faithfulness proofs between the logic embeddings. The approach, which is fruitful for logic education, research and application, is deliberately illustrated here using simple propositional modal logic. However, the work presented is conceptual in nature and not limited to such a simple logic context.
• Abstract（参考訳）: 古典的高階論理における非古典論理の深部および浅部埋め込みは、近年、様々な自動推論ツールで研究され、実装され、使用されてきた。 本稿では,古典的高階論理における深層埋め込みと浅部埋め込みを同時に展開するためのレシピを提案し,メタレベルとオブジェクトレベルでのフレキシブルな対話的かつ自動的な定理の証明と反例を実現するとともに,論理埋め込み間での自動忠実性証明を可能にする。 この手法は論理学の教育、研究、応用に役立ち、単純な命題論理を用いて意図的に説明されている。 しかし、提示された作品は本質的に概念的であり、そのような単純な論理的文脈に限らない。

関連論文リスト

• Logical Modalities within the European AI Act: An Analysis [0.0]
  本稿では,その論理的モダリティの観点から,欧州AI法を包括的に分析する。 論理・多元的知識工学フレームワークと方法論の形式的な表現を準備することを目的としている。 LogiKEyは形式的手法に基づく規範的推論のための計算ツールを開発する。
  論文  参考訳（メタデータ） (2025-01-31T13:15:33Z)
• Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework [93.59256448185954]
  本稿では論理完全推論フレームワークであるAristotleについて,論理解法,論理解法,論理解法,論理解法の3つの主要なコンポーネントを提案する。 本フレームワークでは,記号表現と論理規則を総合的に推論プロセスに統合する。 いくつかのデータセットの実験結果は、Aristotleが最先端の推論フレームワークを精度と効率の両方で一貫して上回っていることを示している。
  論文  参考訳（メタデータ） (2024-12-22T10:14:09Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。 応用例としては、メタ理論的性質の形式的解析と検証がある。
  論文  参考訳（メタデータ） (2023-12-08T09:32:26Z)
• LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and Reasoning [73.98142349171552]
  LOGICSEGは、神経誘導学習と論理推論をリッチデータとシンボリック知識の両方に統合する、全体論的視覚意味論である。 ファジィ論理に基づく連続的な緩和の間、論理式はデータとニューラルな計算グラフに基礎を置いており、論理によるネットワークトレーニングを可能にする。 これらの設計によりLOGICSEGは、既存のセグメンテーションモデルに容易に統合できる汎用的でコンパクトなニューラル論理マシンとなる。
  論文  参考訳（メタデータ） (2023-09-24T05:43:19Z)
• Towards Invertible Semantic-Preserving Embeddings of Logical Formulae [1.0152838128195467]
  論理的要件とルールの学習と最適化は、人工知能において常に重要な問題である。 現在のメソッドは、カーネルメソッドを介して効果的なセマンティック保存の埋め込みを構築することができるが、それらが定義するマップは可逆ではない。 本稿では,グラフ変分オートエンコーダフレームワークに基づく深層アーキテクチャを応用した埋め込みの逆変換法について述べる。
  論文  参考訳（メタデータ） (2023-05-03T10:49:01Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文) 論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。 ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
  論文  参考訳（メタデータ） (2022-07-04T14:38:49Z)
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning [91.3755431537592]
  論理埋め込みツールは、古典的でない推論問題を古典的な高階論理にプロシージャエンコーディングする。 推論ターゲットとして、多くの非古典論理をサポートすることができる。
  論文  参考訳（メタデータ） (2022-03-23T12:08:51Z)
• Automated Reasoning in Non-classical Logics in the TPTP World [58.720142291102135]
  TPTP Worldは現在、古典論理のみをサポートしている。 非古典論理推論の同様の標準は存在しない。 本稿では,非古典論理学における推論のための言語と基盤を提供するTPTP Worldの最新の拡張について述べる。
  論文  参考訳（メタデータ） (2022-02-20T15:29:30Z)
• Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
  本稿では,関連する共通知識を用いた発表ロジックのセマンティックな埋め込みについて述べる。 これにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。 この研究は、複数派のLogiKEy知識工学方法論に重要な追加となる。
  論文  参考訳（メタデータ） (2021-11-02T15:14:52Z)
• Public Announcement Logic in HOL [0.0]
  関連する共通知識を持つ公開告知論理のための浅層セマンティック埋め込みについて述べる。 この埋め込みにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
  論文  参考訳（メタデータ） (2020-10-02T06:46:02Z)
• Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis [0.0]
  本稿では,議論的言説の深い多元論的論理解析へのアプローチを提案する。 我々は古典的な高階論理に最先端の自動推論技術を用いる。
  論文  参考訳（メタデータ） (2020-07-02T11:07:53Z)

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

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