A separation logic for sequences in pointer programs and its decidability

• URL: http://arxiv.org/abs/2301.06237v1
• Date: Mon, 16 Jan 2023 02:52:06 GMT
• Title: A separation logic for sequences in pointer programs and its decidability
• Authors: Tianyue Cao, Bowen Zhang, Zhao Jin, Yongzhi Cao, Hanpin Wang
• Abstract summary: 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 are new members in our logic. 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.
• Score: 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.

Related papers

• Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning [28.111458981621105]
  Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. We propose a Compositional First-Order Logic Translation to capture logical semantics hidden in the natural language during translation. We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches.
  arXiv  Detail & Related papers  (2024-10-10T15:42:39Z)
• Demonstration of 3 V Programmable Josephson Junction Arrays Using Non-Integer-Multiple Logic [19.016449462249156]
  This article demonstrates a new kind of programmable logic for the representation of an integer that can be used for the programmable Josephson voltage standard. It can enable the numbers of junctions in most bits to be variable integer values, which is different from normal binary logic or ternary logic. Missing junctions due to superconducting short circuits can be tolerated under this logic.
  arXiv  Detail & Related papers  (2024-02-25T11:49:48Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts [0.0]
  We focus on the extension of description logic $mathcalEL$. We show that for a useful fragment of the extension, the conclusions entailed by the different semantics coincide. For a slightly smaller, but still useful, fragment, we were also able to show decidability of the extension.
  arXiv  Detail & Related papers  (2023-08-16T09:37:38Z)
• The Transformation Logics [58.35574640378678]
  We introduce a new family of temporal logics designed to balance the trade-off between expressivity and complexity. Key feature is the possibility of defining operators of a new kind that we call transformation operators. We show them to yield logics capable of creating hierarchies of increasing expressivity and complexity.
  arXiv  Detail & Related papers  (2023-04-19T13:24:04Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  Passage-level logical relations represent entailment or contradiction between propositional units (e.g., a concluding sentence) We propose logic structural-constraint modeling to solve the logical reasoning QA and introduce discourse-aware graph networks (DAGNs) The networks first construct logic graphs leveraging in-line discourse connectives and generic logic theories, then learn logic representations by end-to-end evolving the logic relations with an edge-reasoning mechanism and updating the graph features.
  arXiv  Detail & Related papers  (2022-07-04T14:38:49Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  Two programs are equivalent if there exists a sequence of application of rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
  arXiv  Detail & Related papers  (2021-09-22T01:37:08Z)
• Structured Reordering for Modeling Latent Alignments in Sequence Transduction [86.94309120789396]
  We present an efficient dynamic programming algorithm performing exact marginal inference of separable permutations. The resulting seq2seq model exhibits better systematic generalization than standard models on synthetic problems and NLP tasks.
  arXiv  Detail & Related papers  (2021-06-06T21:53:54Z)
• Differentiable Inductive Logic Programming for Structured Examples [6.8774606688738995]
  We propose a new framework to learn logic programs from noisy and structured examples. We show that our new framework can learn logic programs from noisy and structured examples, such as sequences or trees. Our framework can be scaled to deal with complex programs that consist of several clauses with function symbols.
  arXiv  Detail & Related papers  (2021-03-02T13:47:33Z)
• LogicalFactChecker: Leveraging Logical Operations for Fact Checking with Graph Module Network [111.24773949467567]
  We propose LogicalFactChecker, a neural network approach capable of leveraging logical operations for fact checking. It achieves the state-of-the-art performance on TABFACT, a large-scale, benchmark dataset.
  arXiv  Detail & Related papers  (2020-04-28T17:04:19Z)
• Multi-level Head-wise Match and Aggregation in Transformer for Textual Sequence Matching [87.97265483696613]
  We propose a new approach to sequence pair matching with Transformer, by learning head-wise matching representations on multiple levels. Experiments show that our proposed approach can achieve new state-of-the-art performance on multiple tasks.
  arXiv  Detail & Related papers  (2020-01-20T20:02:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.