論文の概要: 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つの交替を持つ断片は決定不可能である。
さらに、論理の決定不能な断片と決定不能な断片の境界をプレネックス正規形式で検討する。
関連論文リスト
- Demonstration of 3 V Programmable Josephson Junction Arrays Using
Non-Integer-Multiple Logic [19.582439018570764]
本稿では、プログラマブルなジョセフソン電圧標準に使用できる整数表現のための新しい種類のプログラマブル論理を実証する。
これは、ほとんどのビットにおけるジャンクションの数を、通常のバイナリ論理や三項論理とは異なる可変整数値にすることができる。
超伝導短絡による短絡の欠落は、この論理の下で許容することができる。
論文 参考訳(メタデータ) (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) - A Divide-Align-Conquer Strategy for Program Synthesis [8.595181704811889]
本稿では,大規模プログラムの探索を複数の小さなプログラム合成問題に分割する例によって,構成セグメント化がプログラミングに応用可能であることを示す。
入力と出力における構成部品の構造的アライメントは、プログラム探索を導くのに使用されるペアワイズ対応に繋がる。
論文 参考訳(メタデータ) (2023-01-08T19:10:55Z) - 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) - Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
確率感性決定図は、解離ゲートの入力が確率値によってアノテートされる論理回路である。
我々は、局所確率を質量関数のクレーダル集合に置き換えることができる確率の一般化である、クレーダル感性決定図を開発する。
まず,ノイズの多い7セグメント表示画像に基づく簡単なアプリケーションについて検討する。
論文 参考訳(メタデータ) (2020-08-19T16:04:34Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。