論文の概要: Finite Model Theory of the Triguarded Fragment and Related Logics
- arxiv url: http://arxiv.org/abs/2101.08377v2
- Date: Sat, 23 Jan 2021 08:56:14 GMT
- ステータス: 処理完了
- システム内更新日: 2021-03-21 07:49:32.462593
- Title: Finite Model Theory of the Triguarded Fragment and Related Logics
- Title(参考訳): 三ガードフラグメントの有限モデル理論と関連する論理
- Authors: Emanuel Kiero\'nski and Sebastian Rudolph
- Abstract要約: Triguarded Fragment (TGF)は第一次論理の最も表現力のある決定可能な断片の1つである。
そこで, TGF は有限モデル特性を持ち, 有限満足度は N2ExpTime-complete として知られる満足度と一致することを示した。
- 参考スコア(独自算出の注目度): 3.883460584034766
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: The Triguarded Fragment (TGF) is among the most expressive decidable
fragments of first-order logic, subsuming both its two-variable and guarded
fragments without equality. We show that the TGF has the finite model property
(providing a tight doubly exponential bound on the model size) and hence finite
satisfiability coincides with satisfiability known to be N2ExpTime-complete.
Using similar constructions, we also establish 2ExpTime-completeness for finite
satisfiability of the constant-free (tri)guarded fragment with transitive
guards.
- Abstract(参考訳): Triguarded Fragment (TGF) は、一階述語論理の最も表現力に富んだ断片であり、その2変数とガードされた断片の両方を等しく仮定している。
TGF は有限モデル特性(モデルサイズに厳密な2倍指数境界を与える)を持ち、したがって有限満足度は N2ExpTime 完全であることが知られている満足度と一致することを示す。
同様の構成を用いると、遷移ガード付き固定自由(tri)ガードフラグメントの有限充足性に対する2ExpTime完全性も確立する。
関連論文リスト
- Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Provable Adversarial Robustness for Fractional Lp Threat Models [136.79415677706612]
分数L_pの「ノルム」で区切られた攻撃はまだ十分に検討されていない。
いくつかの望ましい性質を持つ防衛法を提案する。
証明可能な(認証された)堅牢性を提供し、ImageNetにスケールし、(高い確率ではなく)決定論的保証を得る。
論文 参考訳(メタデータ) (2022-03-16T21:11:41Z) - Controlling the Complexity and Lipschitz Constant improves polynomial
nets [55.121200972539114]
多項式ネットの結合CP分解(CCP)モデルとNested Coupled CP分解(NCP)モデルに対する新しい複雑性境界を導出する。
本研究では、6つのデータセットで実験的に評価し、モデルが逆摂動に対して頑健であるとともに精度も向上することを示す。
論文 参考訳(メタデータ) (2022-02-10T14:54:29Z) - Recursive Bayesian Networks: Generalising and Unifying Probabilistic
Context-Free Grammars and Dynamic Bayesian Networks [0.0]
確率的文脈自由文法 (PCFGs) と動的ベイズネットワーク (DBNs) は相補的な強みと制約を持つシーケンスモデルとして広く使われている。
本稿では,PCFGとDBNを一般化・統合するRecursive Bayesian Networks(RBNs)について述べる。
論文 参考訳(メタデータ) (2021-11-02T19:21:15Z) - Temporal Inference with Finite Factored Sets [0.07614628596146598]
有限因子集合は時間的関係を推定するための強力なツールであることを示す。
因子集合に対するd-分離の類似性、条件性を導入する。
論文 参考訳(メタデータ) (2021-09-23T17:33:30Z) - Lifting the Convex Conjugate in Lagrangian Relaxations: A Tractable
Approach for Continuous Markov Random Fields [53.31927549039624]
断片的な離散化は既存の離散化問題と矛盾しないことを示す。
この理論を2つの画像のマッチング問題に適用する。
論文 参考訳(メタデータ) (2021-07-13T12:31:06Z) - Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model
for Protein Design [70.27706384570723]
Fold2Seqは特定の標的に条件付きタンパク質配列を設計するための新しいフレームワークである。
Fold2Seqの性能は, シーケンス設計の速度, カバレッジ, 信頼性において向上したか, 同等であったかを示す。
フォールドベースのFold2Seqの独特な利点は、構造ベースのディープモデルやRosettaDesignと比較して、3つの現実世界の課題においてより明確になる。
論文 参考訳(メタデータ) (2021-06-24T14:34:24Z) - Interpretable Time-series Representation Learning With Multi-Level
Disentanglement [56.38489708031278]
Disentangle Time Series (DTS)は、シーケンシャルデータのための新しいDisentanglement Enhanceingフレームワークである。
DTSは時系列の解釈可能な表現として階層的意味概念を生成する。
DTSは、セマンティック概念の解釈性が高く、下流アプリケーションで優れたパフォーマンスを実現します。
論文 参考訳(メタデータ) (2021-05-17T22:02:24Z) - Trakhtenbrot's Theorem in Coq: Finite Model Theory through the
Constructive Lens [0.7614628596146599]
依存型理論の構成的設定において有限一階満足度(FSAT)を研究する。
非論理的記号の1階署名に応じて、FSATの完全な分類を行います。
全ての結果は, 合成不決定性の増大するCoqライブラリの枠組みで機械化されている。
論文 参考訳(メタデータ) (2021-04-29T16:05:31Z) - Reducing Discontinuous to Continuous Parsing with Pointer Network
Reordering [0.7412445894287709]
不連続木はトークンを並べ替えることで連続変種に変換することができる。
我々は与えられた入力文の連続トークン配置を正確に生成できるポインタネットワークを開発した。
論文 参考訳(メタデータ) (2021-04-13T14:32:59Z) - On the Oracle Complexity of Higher-Order Smooth Non-Convex Finite-Sum
Optimization [1.6973426830397942]
平滑な非有限和最適化における高階法の下限を証明する。
pth-order regularized method は有限和の目的から利益を得ることができないことを示す。
新たな二階平滑性仮定は一階平均二乗平滑性に類似していると考えられる。
論文 参考訳(メタデータ) (2021-03-08T23:33:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。