論文の概要: A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
- arxiv url: http://arxiv.org/abs/2206.05973v1
- Date: Mon, 13 Jun 2022 08:36:13 GMT
- ステータス: 処理完了
- システム内更新日: 2022-06-15 00:06:18.208101
- Title: A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
- Title（参考訳）: 線形時間時相論理に対するsahlqvist型対応定理
- Authors: Rui Li, Francesco Belardinelli
- Abstract要約: 線形時間時間時間論理(LTL)のためのShlqvist型対応定理を開発する。
モーダル作用素 F, G, X, U を用いて構築されたサルクヴィスト公式の有意なクラスを同定する。
本論文の主な成果は、一階言語で定義可能なフレーム条件に対するソルクヴィスト公式の対応性を証明することである。
- 参考スコア（独自算出の注目度）: 10.029813712651471
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The language of modal logic is capable of expressing first-order conditions
on Kripke frames. The classic result by Henrik Sahlqvist identifies a
significant class of modal formulas for which first-order conditions -- or
Sahlqvist correspondents -- can be find in an effective, algorithmic way.
Recent works have successfully extended this classic result to more complex
modal languages. In this paper, we pursue a similar line and develop a
Sahlqvist-style correspondence theorem for Linear-time Temporal Logic (LTL),
which is one of the most widely used formal languages for temporal
specification. LTL extends the syntax of basic modal logic with dedicated
temporal operators Next X and Until U . As a result, the complexity of the
class of formulas that have first-order correspondents also increases
accordingly. In this paper, we identify a significant class of LTL Sahlqvist
formulas built by using modal operators F , G, X, and U . The main result of
this paper is to prove the correspondence of LTL Sahlqvist formulas to frame
conditions that are definable in first-order language.
- Abstract（参考訳）: モーダル論理の言語はクリプキフレーム上の一階条件を表現することができる。
Henrik Sahlqvist による古典的な結果は、一階条件 (あるいは Sahlqvist 対応式) が効果的でアルゴリズム的な方法で発見できる、重要なモーダル公式のクラスを特定できる。
最近の作品は、この古典的な結果をより複雑なモーダル言語に拡張することに成功している。
本稿では,線形時時時論理 (LTL) に対する類似の行を追求し,時相仕様のための最も広く使われている形式言語の一つである Sahlqvist 形式の対応定理を開発する。
LTLは、基本的なモーダル論理の構文を拡張し、専用のテンポラル演算子Next X と until U を持つ。
その結果、一階の対応式を持つ公式のクラスの複雑さも、それに応じて増加する。
本稿では, モーダル作用素 F , G, X, U を用いて構築した LTL Sahlqvist 公式の有意なクラスを同定する。
本論文の主な結果は、一階言語で定義可能なフレーム条件に対するltl sahlqvist公式の対応を証明することである。
関連論文リスト
- Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
形式言語理論は、特に認識者に関するものである。
代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。
ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
論文 参考訳（メタデータ） (2024-11-11T16:33:25Z) - SymBa: Symbolic Backward Chaining for Structured Natural Language Reasoning [5.893124686141782]
我々はシンボリック・ソルバとLLMを統合した新しい後方連鎖システムSymBaを提案する。
SymBa では、解法が証明過程を制御し、解法が証明を完成させるために新しい情報を必要とする場合にのみ LLM が呼び出される。
完全性を活用して、SymBaは、ベースラインと比較して、導出性、リレーショナル、および算術的推論ベンチマークの大幅な改善を実現している。
論文 参考訳（メタデータ） (2024-02-20T08:27:05Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z) - Advancing Regular Language Reasoning in Linear Recurrent Neural Networks [56.11830645258106]
本稿では,リニアリカレントニューラルネットワーク(LRNN)がトレーニングシーケンスに隠された規則を学習できるかを検討する。
ブロック対角および入力依存遷移行列を備えた新しいLRNNを提案する。
実験結果から,提案モデルが正規言語タスクに対して長さ外挿を行うことができる唯一のLRNNであることが示唆された。
論文 参考訳（メタデータ） (2023-09-14T03:36:01Z) - Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。
有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
論文 参考訳（メタデータ） (2023-07-31T17:02:23Z) - The Alternating-Time \mu-Calculus With Disjunctive Explicit Strategies [1.7725414095035827]
同時ゲーム構造におけるエージェントの連立の戦略能力について検討する。
論理の重要な要素は、あるエージェントの連立が与えられた目標を強制するための共同戦略を持つことを示す経路定量化器である。
我々は, ATLES を固定点演算子と戦略解離で拡張し, 明示的な戦略で時相の $mu$-calculus に到達する。
論文 参考訳（メタデータ） (2023-05-30T07:16:59Z) - Lexinvariant Language Models [84.2829117441298]
離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある
我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。
十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
論文 参考訳（メタデータ） (2023-05-24T19:10:46Z) - Structural generalization is hard for sequence-to-sequence models [85.0087839979613]
シーケンス・ツー・シーケンス(seq2seq)モデルは、多くのNLPタスクで成功している。
構成一般化に関する最近の研究は、セq2seqモデルは訓練で見られなかった言語構造への一般化において非常に低い精度を達成することを示した。
論文 参考訳（メタデータ） (2022-10-24T09:03:03Z) - Temporal Answer Set Programming [3.263632801414296]
本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。
本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。
第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
論文 参考訳（メタデータ） (2020-09-14T16:13:36Z) - A Formal Language Approach to Explaining RNNs [6.624726878647541]
本稿では、線形時間論理(LTL)と呼ばれる形式記述言語を用いて、リカレントニューラルネットワーク(RNN)の意思決定を説明するためのフレームワークであるLEXRを提案する。
LEXRの説明は、RNNから決定論的有限オートマトンを抽出する最近のアルゴリズムで生成されるものよりも正確で理解しやすい。
論文 参考訳（メタデータ） (2020-06-12T16:17:53Z) - Learning Concepts Definable in First-Order Logic with Counting [0.0]
次数構造のクラス上の FOCN は、線形時間で一貫した学習が可能であることを示す。
任意の定数$c$に対して少なくとも$(log log n)c$の次数の構造のクラスについて、ほぼ正しい(PAC)学習に拡張する。
論文 参考訳（メタデータ） (2019-09-09T12:57:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。