Fugu-MT 論文翻訳(概要): Faithful Logic Embeddings in HOL -- Deep and Shallow

論文の概要: Faithful Logic Embeddings in HOL -- Deep and Shallow

arxiv url: http://arxiv.org/abs/2502.19311v3
Date: Sun, 01 Jun 2025 11:17:37 GMT
ステータス: 翻訳完了
システム内更新日: 2025-06-03 13:48:29.937669
Title: Faithful Logic Embeddings in HOL -- Deep and Shallow
Title（参考訳）: HOLの忠実なロジック埋め込み -- 深くて浅く
Authors: Christoph Benzmüller,
Abstract要約: 本稿では,古典的高次論理学における深層・浅層埋め込みの同時展開法を提案する。この手法は論理学の教育、研究、応用に有用であり、ここでは単純な命題のモーダル論理を用いて説明される。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this 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)

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