論文の概要: SHACL2FOL: An FOL Toolkit for SHACL Decision Problems
- arxiv url: http://arxiv.org/abs/2406.08018v1
- Date: Wed, 12 Jun 2024 09:20:25 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-13 17:45:58.573564
- Title: SHACL2FOL: An FOL Toolkit for SHACL Decision Problems
- Title（参考訳）: SHACL2FOL: SHACL決定問題のためのFOLツールキット
- Authors: Paolo Pareti,
- Abstract要約: 我々は、SHACL文書をFOL文に変換する最初の自動ツールであるSHACL2FOLを紹介する。
このツールは、満足度と包含性の2つの静的解析問題に対する解を計算する。
また、一連の制約に関してグラフの有効性をテストすることもできる。
- 参考スコア（独自算出の注目度）: 0.4895118383237099
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Recent studies on the Shapes Constraint Language (SHACL), a W3C specification for validating RDF graphs, rely on translating the language into first-order logic in order to provide formally-grounded solutions to the validation, containment and satisfiability decision problems. Continuing on this line of research, we introduce SHACL2FOL, the first automatic tool that (i) translates SHACL documents into FOL sentences and (ii) computes the answer to the two static analysis problems of satisfiability and containment; it also allow to test the validity of a graph with respect to a set of constraints. By integrating with existing theorem provers, such as E and Vampire, the tool computes the answer to the aforementioned decision problems and outputs the corresponding first-order logic theories in the standard TPTP format. We believe this tool can contribute to further theoretical studies of SHACL, by providing an automatic first-order logic interpretation of its semantics, while also benefiting SHACL practitioners, by supplying static analysis capabilities to help the creation and management of SHACL constraints.
- Abstract（参考訳）: RDFグラフを検証するためのW3C仕様であるShapes Constraint Language (SHACL)に関する最近の研究は、検証、封じ込め、満足度決定問題に対する公式な解を提供するために、言語を一階述語論理に翻訳することに依存している。
SHACL2FOL(SHACL2FOL)は、最初の自動ツールである。
i) SHACL 文書を FOL 文に変換して
i) 満足度と包含性の2つの静的解析問題に対する解を計算し、また、制約の集合に関してグラフの有効性をテストすることもできる。
E や Vampire のような既存の定理証明と統合することにより、上記の決定問題に対する解を計算し、標準 TPTP フォーマットで対応する一階述語論理理論を出力する。
このツールは、SHACLのセマンティクスの自動一階述語論理解釈を提供することによって、SHACLのさらなる理論的研究に寄与し、また、SHACLの制約の作成と管理を支援する静的解析機能を提供することで、SHACL実践者の利益を享受できると考えている。
関連論文リスト
- Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z) - Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。
我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。
我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
論文 参考訳（メタデータ） (2024-09-13T22:25:58Z) - H-STAR: LLM-driven Hybrid SQL-Text Adaptive Reasoning on Tables [56.73919743039263]
本稿では,2段階のプロセスにシンボル的アプローチと意味的アプローチ(テキスト的アプローチ)を統合し,制約に対処する新しいアルゴリズムを提案する。
実験の結果,H-STARは3つの質問応答(QA)と事実検証データセットにおいて,最先端の手法を大幅に上回っていることがわかった。
論文 参考訳（メタデータ） (2024-06-29T21:24:19Z) - Evaluating and Improving Tool-Augmented Computation-Intensive Math
Reasoning [75.74103236299477]
CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。
ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。
CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
論文 参考訳（メタデータ） (2023-06-04T17:02:59Z) - Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
このような問題に対する一般的なフレームワークとして,第2レベル代数モデルカウント (2AMC) を導入している。
KC(Knowledge Compilation)に基づく第1レベルのテクニックは、変数順序制約を課すことで、特定の2AMCインスタンスに適応している。
2AMC問題の論理構造を利用して、これらの制約の一部を省略し、負の効果を制限できることが示される。
論文 参考訳（メタデータ） (2022-05-16T08:10:40Z) - Exploring Viable Algorithmic Options for Learning from Demonstration
(LfD): A Parameterized Complexity Approach [0.0]
本稿では,パラメータ化複雑性解析を用いて,アルゴリズムの選択肢を体系的に探索する方法を示す。
環境、実演、ポリシーに対する多くの(しばしば同時に)制限に対して、我々の問題は、一般的にも、あるいは相対的に、効率的に解決できないことを示す。
論文 参考訳（メタデータ） (2022-05-10T15:54:06Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Satisfiability and Containment of Recursive SHACL [4.8986598953553555]
シェープ制約言語(Shapes Constraint Language, SHACL)は、グラフ上の特定の形状を検証することでRDFデータを検証するための最近のW3C勧告言語である。
これまでの研究は、バリデーション問題と、満足度と封じ込めの標準決定問題に主に焦点を合わせてきた。
我々は、SHACLのセマンティクスを正確に把握するSCLと呼ばれる新しい一階言語への翻訳を提供することにより、SHACLの異なる特徴を包括的に研究する。
また、SCLの2階拡張であるMSCLを提示し、単一の形式論理フレームワーク、メインで定義できるようにしました。
論文 参考訳（メタデータ） (2021-08-30T08:51:03Z) - AR-LSAT: Investigating Analytical Reasoning of Text [57.1542673852013]
テキストの分析的推論の課題を研究し、1991年から2016年までのロースクール入学試験からの質問からなる新しいデータセットを紹介します。
我々は,この課題をうまくこなすために必要な知識理解と推論能力を分析する。
論文 参考訳（メタデータ） (2021-04-14T02:53:32Z) - SHACL Satisfiability and Containment (Extended Paper) [6.308539010172308]
Shapes Constraint Language (SHACL)は、RDFデータを検証するための最近のW3C勧告言語である。
本稿では、SCLと呼ばれる新しい一階述語言語への翻訳を提供することにより、再帰的でないSHACLの異なる特徴を徹底的に研究する。
この論理学におけるSHACLの特徴の相互作用について検討し、上記のSHACLサブ言語に対する決定問題の決定可能性と複雑性の詳細なマップを提供する。
論文 参考訳（メタデータ） (2020-08-31T14:52:03Z) - The empirical duality gap of constrained statistical learning [115.23598260228587]
本研究では,制約付き統計学習問題(制約なし版)について,ほぼ全ての現代情報処理のコアとなる研究を行った。
本稿では, 有限次元パラメータ化, サンプル平均, 双対性理論を利用して, 無限次元, 未知分布, 制約を克服する制約付き統計問題に取り組むことを提案する。
フェアラーニングアプリケーションにおいて,この制約付き定式化の有効性と有用性を示す。
論文 参考訳（メタデータ） (2020-02-12T19:12:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。