論文の概要: String Theories involving Regular Membership Predicates: From Practice
to Theory and Back
- arxiv url: http://arxiv.org/abs/2105.07220v1
- Date: Sat, 15 May 2021 13:13:50 GMT
- ステータス: 処理完了
- システム内更新日: 2021-05-18 14:52:22.617464
- Title: String Theories involving Regular Membership Predicates: From Practice
to Theory and Back
- Title(参考訳): 正規メンバーシップ述語を含む文字列理論:実践から理論へ
- Authors: Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin
Manea, Federico Mora, Dirk Nowotka
- Abstract要約: 文字列制約系に対する満足度問題に対するアルゴリズムは、対象ケースに存在する制約の構造を徹底的に理解する必要がある。
本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,決定不能性を証明する。
特に、現実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直結する。
- 参考スコア(独自算出の注目度): 12.98284167710378
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Widespread use of string solvers in formal analysis of string-heavy programs
has led to a growing demand for more efficient and reliable techniques which
can be applied in this context, especially for real-world cases. Designing an
algorithm for the (generally undecidable) satisfiability problem for systems of
string constraints requires a thorough understanding of the structure of
constraints present in the targeted cases. In this paper, we investigate
benchmarks presented in the literature containing regular expression membership
predicates, extract different first order logic theories, and prove their
decidability, resp. undecidability. Notably, the most common theories in
real-world benchmarks are PSPACE-complete and directly lead to the
implementation of a more efficient algorithm to solving string constraints.
- Abstract(参考訳): 文字列重み付けプログラムの形式解析における文字列ソルバの広範な使用は、特に実世界のケースにおいて、この文脈で適用可能なより効率的で信頼性の高い技術への需要が高まっている。
文字列制約系に対する(一般には決定不可能な)満足度問題に対するアルゴリズムの設計には、対象のケースに存在する制約の構造を十分に理解する必要がある。
本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,その決定可能性を証明する。
決定不能
実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直接繋がる。
関連論文リスト
- Multitask Kernel-based Learning with Logic Constraints [13.70920563542248]
本稿では,タスク関数の集合間の論理制約をカーネルマシンに組み込む枠組みを提案する。
特徴空間上の複数の一意述語をカーネルマシンで学習するマルチタスク学習方式を検討する。
一般的なアプローチでは、論理節を連続的な実装に変換し、カーネルベースの述語によって計算された出力を処理する。
論文 参考訳(メタデータ) (2024-02-16T12:11:34Z) - Optimised Storage for Datalog Reasoning [8.305527776204178]
物質化は、事実とルールのすべての結果を事前計算することで、データログの推論を促進する。
全ての実体化された事実を保管することは、実際には不可能かもしれない。特に規則が複雑で、与えられた事実の集合が大きい場合。
本稿では,このような最適化ストレージスキームを標準物質化アルゴリズムと統合可能な汎用フレームワークを提案する。
論文 参考訳(メタデータ) (2023-12-18T15:46:10Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳(メタデータ) (2023-12-08T09:32:26Z) - A Symbolic Language for Interpreting Decision Trees [7.143485463760098]
決定木を解釈するシンボリック言語であるExplainDTを提示する。
StratiFOILedは評価の表現性と複雑さをバランスさせる。
提案式としてStratiFOILedクエリを符号化するための最適化された実装を提供する。
論文 参考訳(メタデータ) (2023-10-18T00:07:38Z) - Query Structure Modeling for Inductive Logical Reasoning Over Knowledge
Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。
線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。
2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文 参考訳(メタデータ) (2023-05-23T01:25:29Z) - Synergies between Disentanglement and Sparsity: Generalization and
Identifiability in Multi-Task Learning [79.83792914684985]
我々は,最大スパース基底予測器が不整合表現をもたらす条件を提供する新しい識別可能性の結果を証明した。
この理論的な結果から,両レベル最適化問題に基づくアンタングル表現学習の実践的アプローチを提案する。
論文 参考訳(メタデータ) (2022-11-26T21:02:09Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Querying Inconsistent Prioritized Data with ORBITS: Algorithms,
Implementation, and Experiments [12.952483242045366]
優先順位付けされた知識ベース上で不整合耐性問合せ応答を行うための実用的なアルゴリズムについて検討する。
最適補修の2つの概念に基づく3つのよく知られた意味論(AR, IAR, 勇敢)を考える(パレート, 完成)。
論文 参考訳(メタデータ) (2022-02-16T10:44:39Z) - Modal Logic S5 Satisfiability in Answer Set Programming [8.89493507314525]
我々は、あらゆる世界に関係のある命題的原子の実装にAnswer Set Programmingを使うことを提案する。
提案したエンコーディングは、モーダル演算子によって根付いた部分形式間の包含関係などの他の特性を利用するように設計されている。
提案したエンコーディングの実証評価により, 到達性関係は非常に効果的であり, 最先端のS5ソルバに匹敵する性能を示した。
論文 参考訳(メタデータ) (2021-08-09T17:35:31Z) - Fractal Structure and Generalization Properties of Stochastic
Optimization Algorithms [71.62575565990502]
最適化アルゴリズムの一般化誤差は、その一般化尺度の根底にあるフラクタル構造の複雑性'にバウンドできることを示す。
さらに、特定の問題(リニア/ロジスティックレグレッション、隠れ/層ニューラルネットワークなど)とアルゴリズムに対して、結果をさらに専門化します。
論文 参考訳(メタデータ) (2021-06-09T08:05:36Z) - Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。
最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
論文 参考訳(メタデータ) (2020-10-23T19:08:46Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。