2019 | OriginalPaper | Buchkapitel Open Access

# The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains

## 1 Introduction

## 2 Preliminaries

## 3 Test Formulæ for \(\mathsf {SL}^{\!\scriptstyle {k}}\)

^{1}and we use the same symbol to denote both a set and the formula obtained by conjoining the elements of the set. The equivalence relation \(x \approx _T y\) is defined as \(T\,\models \,x \approx y\) and we write \(x \not \approx _T y\) for \(T\,\models \,\lnot x \approx y\). Observe that \(x \not \approx _T y\) is not the complement of \(x \approx _T y\). For a set X of variables, \({|{X}|}_T\) is the number of equivalence classes of \(\approx _T\) in X.

### 3.1 From Test Formulæ to \(\mathsf {FO}\)

^{2}. As a consequence, the transformation preserves sat-equivalence only if the formulæ \({|{h}|}\ge {|{U}|}-n\) occur only at negative polarity (see Lemma 1, Point 2). If the domain is infinite then this problem does not arise since the formulæ \({|{h}|} \ge {|{U}|} - n\) are always false.

## 4 From Quantifier-Free \(\mathsf {SL}^{\!\scriptstyle {k}}\) to Test formulæ

### 4.1 Minterms

^{3}. The domain closure of M is if either \(\mathrm {min}_M = n_1\) and \(\mathrm {max}_M = n_2\) for some \(n_1,n_2 \in \mathbf{\mathbb {Z}}\) such that \(n_1 \ge n_2\), or \(\mathrm {min}_M = {|{U}|} - n_1\) and \(\mathrm {max}_M = {|{U}|} - n_2\), where \(n_2 \ge n_1\); and otherwise:

^{4}if for all \(x,x' \in \mathsf {Var}\) and \(\mathbf y, \mathbf y' \in \mathsf {Var}^k\), such that \(x \approx _M x'\) and \(y_i \approx _M y'_i\) for all \(i \in [1,k]\), we have (1) if \(\mathsf {alloc}(x) \in M\) then \(\lnot \mathsf {alloc}(x') \not \in M\), and (2) if \(x \hookrightarrow \mathbf y \in M\) then \(\lnot \mathsf {alloc}(x'), \lnot x' \hookrightarrow \mathbf y' \not \in M\).

### 4.2 Translating Quantifier-Free \(\mathsf {SL}^{\!\scriptstyle {k}}\) into Minterms

## 5 Bernays-Schönfinkel-Ramsey \(\mathsf {SL}^{\!\scriptstyle {k}}\)

### 5.1 Undecidability of \(\mathsf {BSR}(\mathsf {SL}^{\!\scriptstyle {k}})\)

^{5}. It is easy to check that and are equisatisfiable. The undecidability result still holds for finite satisfiability if a single occurrence of is allowed, in a (ground) formula \({|{h}|} \ge {|{U}|} - 0\) (see the definition of above).