論文の概要: Introducing Proof Tree Automata and Proof Tree Graphs
- arxiv url: http://arxiv.org/abs/2206.06294v1
- Date: Mon, 13 Jun 2022 16:24:33 GMT
- ステータス: 処理完了
- システム内更新日: 2022-06-14 16:25:39.460366
- Title: Introducing Proof Tree Automata and Proof Tree Graphs
- Title（参考訳）: Proof Tree AutomataとProof Tree Graphsの紹介
- Authors: Valentin D. Richard
- Abstract要約: 本稿では、グラフ理論とオートマトン理論のアプローチを用いて、計算の作業を支援する2つの新しいツールを紹介する。
第一のツールはProof Tree Automaton (PTA) であり、その言語が電卓の派生言語である木オートマトンである。
第2のツールは、Proof Tree Graph (PTG) と呼ばれる計算のグラフィカル表現である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In structural proof theory, designing and working on large calculi make it
difficult to get intuitions about each rule individually and as part of a whole
system. We introduce two novel tools to help working on calculi using the
approach of graph theory and automata theory. The first tool is a Proof Tree
Automaton (PTA): a tree automaton which language is the derivation language of
a calculus. The second tool is a graphical representation of a calculus called
Proof Tree Graph (PTG). In this directed hypergraph, vertices are sets of terms
(e.g. sequents) and hyperarcs are rules. We explore properties of PTA and PTGs
and how they relate to each other. We show that we can decompose a PTA as a
partial map from a calculus to a traditional tree automaton. We formulate that
statement in the theory of refinement systems. Finally, we compare our
framework to proof nets and string diagrams.
- Abstract（参考訳）: 構造証明理論では、大規模計算の設計と作業は、システム全体の一部として個々の規則について直観を得るのを難しくする。
グラフ理論とオートマトン理論のアプローチを用いて,計算作業を支援する2つの新しいツールを提案する。
第一のツールはProof Tree Automaton (PTA) であり、その言語が電卓の派生言語である木オートマトンである。
第2のツールは、Proof Tree Graph (PTG) と呼ばれる計算のグラフィカル表現である。
この有向ハイパーグラフでは、頂点は項(例えば列)の集合であり、ハイパーアークは規則である。
PTA と PTG の性質とそれらの相互関係について検討する。
計算値から従来の木オートマトンへの部分写像としてPTAを分解できることが示される。
我々はその文を精錬システム理論で定式化する。
最後に、フレームワークをネットと文字列ダイアグラムの証明と比較します。
関連論文リスト
- TreeFormer: Single-view Plant Skeleton Estimation via Tree-constrained Graph Generation [13.507708659476064]
木制約グラフ生成による植物骨格推定装置であるTreeFormerを提案する。
学習に基づくグラフ生成と従来のグラフアルゴリズムを組み合わせることで,学習ループの制約を課す。
実験の結果,本手法は複数領域の植物骨格構造を正確に推定できることがわかった。
論文 参考訳（メタデータ） (2024-11-25T06:43:20Z) - G-Retriever: Retrieval-Augmented Generation for Textual Graph Understanding and Question Answering [61.93058781222079]
現実のテキストグラフを対象とするフレキシブルな問合せフレームワークを開発した。
一般のテキストグラフに対する最初の検索拡張生成(RAG)手法を提案する。
G-Retrieverは、このタスクをSteiner Tree最適化問題として定式化し、グラフ上でRAGを実行する。
論文 参考訳（メタデータ） (2024-02-12T13:13:04Z) - Graph Generation with $K^2$-trees [13.281380233427287]
K2$-tree表現を利用した新しいグラフ生成手法を提案する。
また、プルーニング、フラットニング、トークン化プロセスを組み込んだシーケンシャルな$K2$-treerepresentationを提示する。
グラフ生成の優位性を確認するため,本アルゴリズムを4つの一般および2つの分子グラフデータセット上で広範囲に評価した。
論文 参考訳（メタデータ） (2023-05-30T15:36:37Z) - Structure-Unified M-Tree Coding Solver for MathWord Problem [57.825176412485504]
従来,数式表現の2次木構造を考慮に入れたモデルでは,性能が向上した。
本稿では、出力構造を統一するために、任意のM枝(M-tree)を持つ木を適用した構造統一M-Tree符号化(S-UMCr)を提案する。
広く使われているMAWPSとMath23Kデータセットの実験結果は、SUMC-rが複数の最先端モデルを上回るだけでなく、低リソース条件下でもはるかに優れた性能を発揮することを示した。
論文 参考訳（メタデータ） (2022-10-22T12:20:36Z) - A Prufer-Sequence Based Representation of Large Graphs for Structural
Encoding of Logic Networks [0.30458514384586405]
本稿では,グラフの構造が実生活システムの性質に影響を及ぼすという仮説を主に懸念する。
このような構造的影響のモデルは、VLSI回路のような複雑で大規模なシステムの有用な性質を推論するのに有用である。
論文 参考訳（メタデータ） (2022-09-04T11:24:19Z) - Explanation Graph Generation via Pre-trained Language Models: An
Empirical Study with Contrastive Learning [84.35102534158621]
エンドツーエンドで説明グラフを生成する事前学習言語モデルについて検討する。
本稿では,ノードとエッジの編集操作によるグラフ摂動の簡易かつ効果的な方法を提案する。
提案手法は,説明グラフの構造的精度と意味的精度を両立させる。
論文 参考訳（メタデータ） (2022-04-11T00:58:27Z) - Bayesian learning of forest and tree graphical models [0.0]
あるグラフから別のグラフへ繰り返し移動することによって、あるグラフのクラスや近似分布に注意することが一般的である。
非分解性グラフに対するアルゴリズムの2つの修正版を与え、特に事前分布としてランダム分布について議論する。
論文 参考訳（メタデータ） (2021-08-31T17:30:08Z) - Partition and Code: learning how to compress graphs [50.29024357495154]
まず、分割アルゴリズムがグラフを基本構造に分解し、これらを確率分布を学習する小さな辞書の要素にマッピングし、エントロピーエンコーダが表現をビットに変換する。
提案アルゴリズムは,非パラメトリックおよびパラメトリックグラフ圧縮器の異なるファミリーに対して,多種多様な実世界のネットワーク上で定量的に評価し,大幅な性能向上を実現している。
論文 参考訳（メタデータ） (2021-07-05T11:41:16Z) - Neural Trees for Learning on Graphs [19.05038106825347]
グラフニューラルネットワーク(GNN)は、グラフを学習するための柔軟で強力なアプローチとして登場した。
我々はニューラルツリーという新しいGNNアーキテクチャを提案する。
神経木アーキテクチャは無向グラフ上の任意の滑らかな確率分布関数を近似できることを示す。
論文 参考訳（メタデータ） (2021-05-15T17:08:20Z) - ExplaGraphs: An Explanation Graph Generation Task for Structured
Commonsense Reasoning [65.15423587105472]
スタンス予測のための説明グラフ生成の新しい生成および構造化コモンセンスリゾニングタスク(および関連するデータセット)を紹介します。
具体的には、信念と議論が与えられた場合、モデルは、議論が信念を支持しているかどうかを予測し、予測されたスタンスに対する非自明で完全で曖昧な説明として機能する常識強化グラフを生成する必要がある。
グラフの83%は、様々な構造と推論深度を持つ外部のコモンセンスノードを含んでいる。
論文 参考訳（メタデータ） (2021-04-15T17:51:36Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。