English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper investigates the satisfiability problem for Separation Logic, withunrestricted nesting of separating conjunctions and implications, for prenexformulae with quantifier prefix in the language $\exists^*\forall^*$, in thecases where the universe of possible locations is either countably infinite orfinite. In analogy with first-order logic with uninterpreted predicates andequality, we call this fragment Bernays-Sch\"onfinkel-Ramsey Separation Logic[BSR(SLk)]. We show that, unlike in first-order logic, the (in)finitesatisfiability problem is undecidable for BSR(SLk) and we define twonon-trivial subsets thereof, that are decidable for finite and infinitesatisfiability, respectively, by controlling the occurrences of universallyquantified variables within the scope of separating implications, as well asthe polarity of the occurrences of the latter. The decidability results areobtained by a controlled elimination of separating connectives, described as(i) an effective translation of a prenex form Separation Logic formula into acombination of a small number of \emph{test formulae}, using only first-orderconnectives, followed by (ii) a translation of the latter into anequisatisfiable first-order formula.

On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic