論文の概要: A separation logic for sequences in pointer programs and its decidability

• arxiv url: http://arxiv.org/abs/2301.06237v1
• Date: Mon, 16 Jan 2023 02:52:06 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-18 16:45:54.576791
• Title: A separation logic for sequences in pointer programs and its decidability
• Title（参考訳）: ポインタプログラムにおけるシーケンスの分離論理とその決定可能性
• Authors: Tianyue Cao, Bowen Zhang, Zhao Jin, Yongzhi Cao, Hanpin Wang
• Abstract要約: ヒープ制御プログラムの論理的推論にシーケンスを組み込んだシーケンスヒープ分離論理を提案する。 シーケンス変数とシングルトンヒープ格納シーケンスの量子化は、私たちの論理における新しいメンバーである。 シーケンス-ヒープ分離論理の命題的断片は決定可能であり、プログラム変数が2回、シーケンス変数が1回変更される断片は決定不可能である。
• 参考スコア（独自算出の注目度）: 5.229882716833972
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequences and multilevel data structures, we propose sequence-heap separation logic which integrates sequences into logical reasoning on heap-manipulated programs. Quantifiers over sequence variables and singleton heap storing sequence (sequence singleton heap) are new members in our logic. Further, we study the satisfiability problem of two fragments. The propositional fragment of sequence-heap separation logic is decidable, and the fragment with 2 alternations on program variables and 1 alternation on sequence variables is undecidable. In addition, we explore boundaries between decidable and undecidable fragments of the logic with prenex normal form.
• Abstract（参考訳）: 分離論理とその変種はポインタプログラムで様々な特性を記述することができる。 しかし、列上の性質に関しては、形式化が難しい場合がある。 可変長シーケンスと多レベルデータ構造のプロパティを扱うために,ヒープ操作プログラムの論理推論にシーケンスを統合するシーケンスヒープ分離論理を提案する。 シーケンス変数とシングルトンヒープ格納シーケンス(シーケンスシングルトンヒープ)の定量化は、私たちのロジックの新しいメンバーです。 さらに,2つのフラグメントの満足度問題について検討した。 シーケンス-ヒープ分離論理の命題的断片は決定可能であり、プログラム変数に2つの交替とシーケンス変数に1つの交替を持つ断片は決定不可能である。 さらに、論理の決定不能な断片と決定不能な断片の境界をプレネックス正規形式で検討する。

関連論文リスト

• Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning [28.111458981621105]
  複雑な論理的推論タスクは、長い推論を必要とするが、それは、チェーン・オブ・シークレットのプロンプトを持つ大きな言語モデル(LLM)が依然として不足している。 本稿では,翻訳中に自然言語に隠された論理的意味を抽出する合成一階論理翻訳を提案する。 提案手法は,CLOVERと呼ばれる7つの論理的推論ベンチマークを用いて評価し,従来のニューロシンボリックアプローチよりも優れていたことを示す。
  論文  参考訳（メタデータ） (2024-10-10T15:42:39Z)
• Demonstration of 3 V Programmable Josephson Junction Arrays Using Non-Integer-Multiple Logic [19.016449462249156]
  本稿では、プログラマブルなジョセフソン電圧標準に使用できる整数表現のための新しい種類のプログラマブル論理を実証する。 これは、ほとんどのビットにおけるジャンクションの数を、通常のバイナリ論理や三項論理とは異なる可変整数値にすることができる。 超伝導短絡による短絡の欠落は、この論理の下で許容することができる。
  論文  参考訳（メタデータ） (2024-02-25T11:49:48Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts [0.0]
  私たちは記述ロジックの拡張に$mathcalEL$をフォーカスします。 拡張の有用な断片について、異なる意味論による結論が一致することを示す。 わずかに小さいが、それでも有用である断片のために、私たちは拡張の決定可能性を示すことができました。
  論文  参考訳（メタデータ） (2023-08-16T09:37:38Z)
• The Transformation Logics [58.35574640378678]
  表現性と複雑性のトレードオフのバランスをとるために設計された、時間論理の新しいファミリーを導入する。 重要な特徴は、変換演算子と呼ばれる新しい種類の演算子を定義する可能性である。 表現力と複雑性を増大させる階層を創り出すことができる論理を提示する。
  論文  参考訳（メタデータ） (2023-04-19T13:24:04Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文) 論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。 ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
  論文  参考訳（メタデータ） (2022-07-04T14:38:49Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。 本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
  論文  参考訳（メタデータ） (2021-09-22T01:37:08Z)
• Structured Reordering for Modeling Latent Alignments in Sequence Transduction [86.94309120789396]
  本稿では,分離可能な置換の辺りを正確に推定する効率的な動的プログラミングアルゴリズムを提案する。 結果のSeq2seqモデルは、合成問題やNLPタスクの標準モデルよりも体系的な一般化が優れている。
  論文  参考訳（メタデータ） (2021-06-06T21:53:54Z)
• Differentiable Inductive Logic Programming for Structured Examples [6.8774606688738995]
  雑音や構造化例から論理プログラムを学ぶための新しいフレームワークを提案する。 我々の新しいフレームワークは、シーケンスやツリーなど、ノイズや構造化された例から論理プログラムを学習できることを示します。 我々のフレームワークは、関数記号を持つ複数の節からなる複雑なプログラムを扱うためにスケールできる。
  論文  参考訳（メタデータ） (2021-03-02T13:47:33Z)
• LogicalFactChecker: Leveraging Logical Operations for Fact Checking with Graph Module Network [111.24773949467567]
  ファクトチェックに論理演算を活用するニューラルネットワークアプローチであるLogicalFactCheckerを提案する。 大規模なベンチマークデータセットであるTABFACT上での最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2020-04-28T17:04:19Z)
• Multi-level Head-wise Match and Aggregation in Transformer for Textual Sequence Matching [87.97265483696613]
  そこで本研究では,複数のレベルにおける頭部のマッチング表現を学習することで,Transformerとのシーケンスペアマッチングを新たに提案する。 実験の結果,提案手法は複数のタスクにおいて新しい最先端性能を実現することができることがわかった。
  論文  参考訳（メタデータ） (2020-01-20T20:02:02Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。