論文の概要: Intuitionistic Linear Temporal Logics
- arxiv url: http://arxiv.org/abs/1912.12893v1
- Date: Mon, 30 Dec 2019 11:49:31 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-17 03:00:37.347396
- Title: Intuitionistic Linear Temporal Logics
- Title(参考訳): 直観主義線形時間論理
- Authors: Philippe Balbiani and Joseph Boudou and Mart\'in Di\'eguez and David
Fern\'andez-Duque
- Abstract要約: 線形時相論理の直観的変種を次の', "to', and release" とみなす。
我々は $iltl$ が有効有限モデル特性を持ち、したがって決定可能であることを証明し、$itlb$ は有限モデル特性を持たない。
また、これらの論理に対する有界双変調の概念を導入し、それらを用いて、持続的なポーズのクラスでさえも、proto' と Release' の作用素が互いに定義できないことを示す。
- 参考スコア(独自算出の注目度): 0.7087237546722617
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We consider intuitionistic variants of linear temporal logic with `next',
`until' and `release' based on expanding posets: partial orders equipped with
an order-preserving transition function. This class of structures gives rise to
a logic which we denote $\iltl$, and by imposing additional constraints we
obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there
temporal logic, both of which have been considered in the literature. We prove
that $\iltl$ has the effective finite model property and hence is decidable,
while $\itlb$ does not have the finite model property. We also introduce
notions of bounded bisimulations for these logics and use them to show that the
`until' and `release' operators are not definable in terms of each other, even
over the class of persistent posets.
- Abstract(参考訳): 我々は,'next', 'until', `release' を含む線形時相論理の直観的変種を考える。
この構造のクラスは、我々が $\iltl$ と表現する論理を生み出し、追加の制約を課すことで、持続的なポーズの $\itlb$ と、ここで考える時相論理の $\itlht$ を得る。
我々は、$\iltl$ が有効有限モデル特性を持ち、したがって決定可能であることを証明し、$\itlb$ は有限モデル特性を持たない。
また、これらの論理に対する有界双シミュレーションの概念を導入し、それらを用いて、持続的なポーズのクラスでさえも 'until' と 'release' 作用素が互いに定義できないことを示す。
関連論文リスト
- Explaining k-Nearest Neighbors: Abductive and Counterfactual Explanations [48.13753926484667]
我々は、$barx$説明は高次元のアプリケーションでは非現実的であり、各ベクトルには数百から数千の特徴があると主張している。
我々は「最小の十分な理由」のような帰納的説明を、その分類を保証するのに十分である$barx$の一連の特徴に対応するものとして研究する。
本稿では, 実証的, 否定的複雑性の結果を, 事実的, 帰納的な説明に対して詳細に示す。
論文 参考訳(メタデータ) (2025-01-10T16:14:35Z) - Temporal Ensemble Logic [2.71467552808655]
線形時間時間的推論のためのモナディックな1次モーダル論理であるテンポラル・アンサンブル論理(TEL)を導入する。
TELは、臨床および人口健康研究における厳格化とコホート仕様と発見の要件から動機付けられている。
本稿では,その形式的意味論,証明システム,および$rm TEL_mathbbN+$の満足性の証明を行う。
論文 参考訳(メタデータ) (2024-08-26T17:36:25Z) - Neuro-Symbolic Temporal Point Processes [13.72758658973969]
本稿では,時間点プロセスモデルにニューラル・シンボリック・ルール誘導フレームワークを導入する。
負の対数類似性は学習を導く損失であり、説明論理則とその重みがエンドツーエンドで学習される。
提案手法は, 合成データセットおよび実データセット間で, 顕著な効率性と精度を示す。
論文 参考訳(メタデータ) (2024-06-06T09:52:56Z) - Reasoning about Intuitionistic Computation Tree Logic [8.512802769278245]
計算木論理の直観的バージョンを定義する。
我々は CTL の固定点公理が直観論的な CTL では有効でないことを示した。
論文 参考訳(メタデータ) (2023-10-03T18:30:39Z) - Description Logics Go Second-Order -- Extending EL with Universally
Quantified Concepts [0.0]
私たちは記述ロジックの拡張に$mathcalEL$をフォーカスします。
拡張の有用な断片について、異なる意味論による結論が一致することを示す。
わずかに小さいが、それでも有用である断片のために、私たちは拡張の決定可能性を示すことができました。
論文 参考訳(メタデータ) (2023-08-16T09:37:38Z) - Simulating Structural Plasticity of the Brain more Scalable than
Expected [69.39201743340747]
Rinkeらは、Barnes-Hutアルゴリズムの変種を用いて、現在のハードウェア上で最大10億のニューロンに対して構造的可塑性をシミュレートするスケーラブルなアルゴリズムを導入した。
アルゴリズムを慎重に検討すると、理論ランタイムは$O(n log2 n)$と分類できる。
論文 参考訳(メタデータ) (2022-10-11T09:02:43Z) - Logic-Driven Context Extension and Data Augmentation for Logical
Reasoning of Text [65.24325614642223]
論理的な記号や表現をテキストで理解し、答えにたどり着くよう提案します。
このような論理的情報に基づいて,文脈拡張フレームワークとデータ拡張アルゴリズムを提案する。
本手法は最先端の性能を実現し,論理駆動コンテキスト拡張フレームワークとデータ拡張アルゴリズムの両方が精度向上に寄与する。
論文 参考訳(メタデータ) (2021-05-08T10:09:36Z) - Superposition with Lambdas [59.87497175616048]
匿名関数を含むがブール関数を除いた拡張多型高階論理のクラスフラグメントに対する重ね合わせ計算を設計する。
推論ルールは$betaeta$-equivalence class of $lambda$-termsで動作し、難解な完全性を達成するために高階統一に依存する。
論文 参考訳(メタデータ) (2021-01-31T13:53:17Z) - Lexicographic Logic: a Many-valued Logic for Preference Representation [1.5484595752241122]
本稿では,様々な選好を表現できる古典命題論理の拡張である辞書論理を提案する。
ユーザの嗜好の満足度に応じてクエリ結果のランク付けを行う上で,新しい論理は有効な形式である,と我々は主張する。
論文 参考訳(メタデータ) (2020-12-20T14:42:04Z) - Thresholded Lasso Bandit [70.17389393497125]
Thresholded Lasso banditは、報酬関数を定義するベクトルとスパースサポートを推定するアルゴリズムである。
一般には $mathcalO( log d + sqrtT )$ や $mathcalO( log d + sqrtT )$ としてスケールする非漸近的後悔の上界を確立する。
論文 参考訳(メタデータ) (2020-10-22T19:14:37Z) - Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。
計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文 参考訳(メタデータ) (2020-05-05T12:10:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。