論文の概要: A Shallow Embedding of Datalog in Lean

• arxiv url: http://arxiv.org/abs/2605.02113v1
• Date: Mon, 04 May 2026 00:34:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-05 20:33:50.088682
• Title: A Shallow Embedding of Datalog in Lean
• Title（参考訳）: リーンにおけるデータログの浅層埋め込み
• Authors: Ramy Shahin,
• Abstract要約: 本稿では、リーン上にドメイン特化言語(DSL)としてのDatalogの浅い埋め込みの設計と実装について概説する。 Datalog DSLとLeanの双方向の相互運用性がこの設計の主要な目標です。
• 参考スコア（独自算出の注目度）: 1.421397337947365
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself. This paper outlines the design and implementation of a shallow embedding of Datalog as a Domain Specific Language (DSL) on top of Lean. Bidirectional interoperability between the Datalog DSL and Lean is a primary goal of this design. In addition to rules and facts, backward chaining queries are automatically translated into theorems with tactic-based proofs. The paper also includes three simple examples of how the DSL can be used.
• Abstract（参考訳）: Datalogは、Horn節の論理に基づく軽量論理プログラミング言語である。 一方、リーンは、インダクティブ・コンストラクションの計算(CIC)に基づく証明補助システムと言語である。 Datalogはリーンよりも制約があり、表現力は低いが、確立された推論アルゴリズムの長い歴史がある。 リーンのDatalogフラグメントで定義やクエリを記述するのは、リーン自体に記述するよりも簡潔で理解しやすいでしょう。 本稿では、リーン上にドメイン特化言語(DSL)としてのDatalogの浅い埋め込みの設計と実装について概説する。 Datalog DSLとLeanの双方向の相互運用性がこの設計の主要な目標です。 規則や事実に加えて、後方連鎖クエリは、戦術に基づく証明を伴う定理に自動的に変換される。 論文にはDSLの使い方に関する簡単な例が3つ含まれています。

関連論文リスト

• OrLog: Resolving Complex Queries with LLMs and Probabilistic Reasoning [51.58235452818926]
  そこで我々は,論理的推論から述語レベルの妥当性推定を分離するニューロシンボリック検索フレームワークOrLogを紹介する。 大規模言語モデル (LLM) は1つの復号のない前方通過において原子述語に対する可視性スコアを提供し、確率論的推論エンジンはクエリ満足度の後方確率を導出する。
  論文  参考訳（メタデータ） (2026-01-30T15:31:58Z)
• Last Layer Logits to Logic: Empowering LLMs with Logic-Consistent Structured Knowledge Reasoning [55.55968342644846]
  大規模言語モデル(LLM)は、膨大な非構造化テキストの事前学習を通じて、自然言語推論タスクにおいて優れた性能を達成する。 LLM出力の論理的欠陥を修正するために,ロジット強化とロジットフィルタリングをコアモジュールとして組み込んだ textitLogits-to-Logic フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-11-11T07:08:27Z)
• LUNAR: Unsupervised LLM-based Log Parsing [34.344687402936835]
  LUNARは,効率的かつ市販のログ解析のための教師なし手法である。 我々の重要な洞察は、LSMは直接ログ解析に苦労するかもしれないが、それらの性能は比較分析によって大幅に向上できるということである。 大規模な公開データセットの実験は、LUNARが精度と効率の点で最先端のログクラフトを著しく上回っていることを示している。
  論文  参考訳（メタデータ） (2024-06-11T11:32:01Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• 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)
• The Complexity of Why-Provenance for Datalog Queries [3.85203215318097]
  クエリ結果を説明する標準的な方法は、いわゆるwhy-provenanceであり、クエリ結果に証人に関する情報を、その結果を引き出すのに十分な入力データベースのサブセットの形式で提供します。 驚いたことに、なぜデータログクエリが実現したのかという概念は何十年にもわたって研究されてきたが、その計算複雑性はまだ解明されていない。 我々は、データログクエリとそのキーサブクラスに対して、なぜ保証されているのかというデータの複雑さを指摘します。
  論文  参考訳（メタデータ） (2023-03-22T17:37:39Z)
• Complexity of Arithmetic in Warded Datalog+- [1.5469452301122173]
  Warded Datalog+- ロジックベースの言語Datalogを拡張し、ルールヘッドに存在量化器を配置する。 我々はWarded Datalog+を算術演算で拡張し、P完全性を証明する新しい言語を定義する。 我々は,新たに定義された言語に対する効率的な推論アルゴリズムを提案し,最近導入された整数演算を用いたデータログフラグメントの記述的複雑性を証明した。
  論文  参考訳（メタデータ） (2022-02-10T15:14:03Z)

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

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