論文の概要: Connecting Proof Theory and Knowledge Representation: Sequent Calculi
and the Chase with Existential Rules
- arxiv url: http://arxiv.org/abs/2306.02521v1
- Date: Mon, 5 Jun 2023 01:10:23 GMT
- ステータス: 処理完了
- システム内更新日: 2023-06-06 17:29:23.939179
- Title: Connecting Proof Theory and Knowledge Representation: Sequent Calculi
and the Chase with Existential Rules
- Title（参考訳）: 証明理論と知識表現をつなぐ--実存則によるシークエント計算とチェイス
- Authors: Tim S. Lyon and Piotr Ostropolski-Nalewaja
- Abstract要約: 実存則の文脈におけるチェイス機構は、本質的には、一階述語論理に対するゲンツェンの逐次計算の拡張における証明探索と同じであることを示す。
我々は、決定可能性の証明を理論的に確立するための中央ツールを、知識表現の文脈において、決定可能性の中央ツールと正式に結合する。
- 参考スコア（独自算出の注目度）: 1.8275108630751844
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Chase algorithms are indispensable in the domain of knowledge base querying,
which enable the extraction of implicit knowledge from a given database via
applications of rules from a given ontology. Such algorithms have proved
beneficial in identifying logical languages which admit decidable query
entailment. Within the discipline of proof theory, sequent calculi have been
used to write and design proof-search algorithms to identify decidable classes
of logics. In this paper, we show that the chase mechanism in the context of
existential rules is in essence the same as proof-search in an extension of
Gentzen's sequent calculus for first-order logic. Moreover, we show that
proof-search generates universal models of knowledge bases, a feature also
exhibited by the chase. Thus, we formally connect a central tool for
establishing decidability proof-theoretically with a central decidability tool
in the context of knowledge representation.
- Abstract（参考訳）: カオスアルゴリズムは知識ベースクエリの領域では不可欠であり、与えられたオントロジーからのルールの適用を通じて、あるデータベースから暗黙の知識を抽出することができる。
このようなアルゴリズムは、決定可能なクエリを包含する論理言語を特定するのに有用であることが証明されている。
証明論の分野において、シークエント計算は論理の識別可能なクラスを識別するために証明探索アルゴリズムを記述および設計するために用いられる。
本稿では,存在規則の文脈におけるチェイス機構が,一階述語論理に対するゲンツェンのシークエント計算の拡張における証明探索と本質的に同じであることを示す。
さらに,証明探索が知識基盤の普遍的モデルを生成することを示し,その特徴を追究した。
そこで,我々は知識表現の文脈において,決定可能性証明を理論的に中心決定可能性ツールと結びつける。
関連論文リスト
- TabVer: Tabular Fact Verification with Natural Logic [11.002475880349452]
本稿では,自然論理の文脈における数値と算術関数の集合論的解釈を提案する。
大規模言語モデルを用いて,テーブル上で関数を実行することで応答するクレームの健全な部分に関する質問を生成することにより,算術式を生成する。
FEVEROUS上の数ショット設定では、71.4の精度を達成し、完全な神経的および象徴的推論モデルの両方を3.4ポイント上回る。
論文 参考訳（メタデータ） (2024-11-02T00:36:34Z) - ChatRule: Mining Logical Rules with Large Language Models for Knowledge
Graph Reasoning [107.61997887260056]
そこで我々は,知識グラフ上の論理ルールをマイニングするための大規模言語モデルの力を解き放つ新しいフレームワークChatRuleを提案する。
具体的には、このフレームワークは、KGのセマンティック情報と構造情報の両方を活用するLLMベースのルールジェネレータで開始される。
生成されたルールを洗練させるために、ルールランキングモジュールは、既存のKGから事実を取り入れてルール品質を推定する。
論文 参考訳（メタデータ） (2023-09-04T11:38:02Z) - Modeling Hierarchical Reasoning Chains by Linking Discourse Units and
Key Phrases for Reading Comprehension [80.99865844249106]
本稿では,論理的推論の基盤として,対話レベルと単語レベルの両方の文脈を扱う総合グラフネットワーク(HGN)を提案する。
具体的には、ノードレベルの関係とタイプレベルの関係は、推論過程におけるブリッジと解釈できるが、階層的な相互作用機構によってモデル化される。
論文 参考訳（メタデータ） (2023-06-21T07:34:27Z) - Implementing Dynamic Programming in Computability Logic Web [0.0]
本稿では,アルゴリズムとその対応するアルゴリズム言語であるCoLwebについて述べる。
CoLwebは、非分散コンピューティングと分散コンピューティングの両方のためのアルゴリズム設計に対して、高レベルの、証明付き、分散スタイルのアプローチを強制します。
我々は,Hhorn節の定義を視覚的ユニバーサリー量子化(BUQ)と並列ユニバーサリー量子化(PUQ)の2種類に洗練する。
論文 参考訳（メタデータ） (2023-04-04T05:33:43Z) - Adversarial Learning to Reason in an Arbitrary Logic [5.076419064097733]
定理を証明するための既存のアプローチは、特定の論理とデータセットに焦点を当てている。
本稿では,任意の論理で動作可能な強化学習によって導かれるモンテカルロシミュレーションを提案する。
論文 参考訳（メタデータ） (2022-04-06T11:25:19Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳（メタデータ） (2021-11-23T17:49:00Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳（メタデータ） (2021-09-25T00:00:47Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳（メタデータ） (2021-07-30T08:27:15Z) - Fact-driven Logical Reasoning for Machine Reading Comprehension [82.58857437343974]
私たちは、常識と一時的な知識のヒントの両方を階層的にカバーする動機があります。
具体的には,文の背骨成分を抽出し,知識単位の一般的な定式化を提案する。
次に、事実単位の上にスーパーグラフを構築し、文レベル(事実群間の関係)と実体レベルの相互作用の利点を享受する。
論文 参考訳（メタデータ） (2021-05-21T13:11:13Z) - Logical Neural Networks [51.46602187496816]
ニューラルネットワーク(学習)と記号論理(知識と推論)の両方の重要な特性をシームレスに提供する新しいフレームワークを提案する。
すべてのニューロンは、重み付けされた実数値論理における公式の構成要素としての意味を持ち、非常に解釈不能な非絡み合い表現をもたらす。
推論は事前に定義されたターゲット変数ではなく、オムニであり、論理的推論に対応する。
論文 参考訳（メタデータ） (2020-06-23T16:55:45Z) - Extending Automated Deduction for Commonsense Reasoning [0.0]
本論文は,古典的な一階述語論理を自動推論する手法とアルゴリズムを,コモンセンス推論に拡張できると主張している。
提案された拡張は主に通常の証明木に依存しており、不整合、デフォルトルール、トピックの操作、関連性、信頼性、類似度などを含む常識知識ベースを扱うように設計されている。
機械学習はコモンセンスの知識ベースを構築するのに最適であり、拡張された論理ベースの手法はこれらの知識ベースからのクエリに実際に答えるのに適している、と我々は主張する。
論文 参考訳（メタデータ） (2020-03-29T23:17:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。