# Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates

Mnacho Echenim, Nicolas Peltier

► To cite this version:

Mnacho Echenim, Nicolas Peltier. Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. Fundamenta Informaticae, 2025, 194 (1), pp.11318. 10.46298/fi.11318 . hal-05168028

HAL Id: hal-05168028

https://hal.science/hal-05168028v1

Submitted on 17 Jul 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates

Mnacho Echenim*

Nicolas Peltier*

Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, 38000 Grenoble, France

**Abstract.** We establish various complexity results for the entailment problem between formulas in Separation Logic (SL) with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on the inductive rules that define the semantics of the predicates. We focus on so-called *P-rules*, which are similar to (but simpler than) the so-called *bounded treewidth fragment* of SL studied by Iosif et al. in 2013. In particular, for a specific fragment where predicates are defined by so-called *loc-deterministic* inductive rules, we devise a sound and complete cyclic proof procedure running in polynomial time. Several complexity lower bounds are provided, showing that any relaxing of the provided conditions makes the problem intractable.

**Keywords:** Separation logic, Inductive reasoning, Decision procedures, Cyclic proofs

**ACM Computing Classification System:** —Theory of computation, Logic, Automated reasoning;
—Theory of computation, Logic, Separation logic

## 1. Introduction

Separation Logic [15, 20] (SL) is widely used in verification to reason on programs manipulating pointer-based data structures. It forms the basis of several automated static program analyzers such as Smallfoot [1], Infer [3] (Facebook) or SLAyer [2] (Microsoft Research) and several correctness proofs were carried out by embedding SL in interactive theorem provers such as Coq [21], see for instance

<footnote>*This work has been partially funded by the French National Research Agency (ANR-21-CE48-0011).</footnote>
[16]. SL uses a special connective $*$, called separating conjunction, modeling heap compositions and allowing for concise and natural specifications. More precisely, atoms in SL are expressions of the forms $x \mapsto (y_1, \dots, y_n)$, where $x, y_1, \dots, y_n$ are variables denoting locations (i.e., memory addresses), asserting that location $x$ is allocated and refers to the tuple (record) $(y_1, \dots, y_n)$. The special connective $\phi * \psi$ asserts that formulas $\phi$ and $\psi$ hold on disjoint parts of the memory. Recursive data structures may then be described by considering predicates associated with inductive rules, such as:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
\texttt{ls}(x, y) & \leftarrow & x \mapsto y & \texttt{tree}(x) & \leftarrow x \mapsto () \\
\texttt{ls}(x, y) & \leftarrow & x \mapsto z * \texttt{ls}(z, y) & \texttt{tree}(x) & \leftarrow x \mapsto (y, z) * \texttt{tree}(y) * \texttt{tree}(z)
\end{array}
$$

where $\texttt{ls}(x, y)$ denotes a nonempty list segment and $\texttt{tree}(x)$ denotes a tree. For the sake of gener-
icity, such rules are not built-in but may be provided by the user. Due to the expressive power of
such inductive definitions, the input language is usually restricted in this context to so-called *symbolic
heaps*. These are existentially quantified conjunctions and separating conjunctions of atoms, including
inductively defined predicates and equational atoms but dismissing for instance universal quantifica-
tions, negations and separating implications. Many problems in verification require to solve entailment
problems between such SL formulas, for instance when these formulas denote pre- or post-conditions
of programs. Unfortunately, the entailment problem between symbolic heaps is undecidable in general
[19], but it is decidable if the considered inductive rules satisfy the so-called *PCE conditions* (standing
for *Progress, Connectivity and Establishment*) [13]. However even for the PCE fragment the complex-
ity of the entailment problem is still very high; more precisely, this problem is 2-EXPTIME-complete
[8, 9, 17]. Less expressive fragments have thus been considered, for which more efficient algorithms
were developed. In [14] a strict subclass of PCE entailments is identified with an EXPTIME complex-
ity based on a reduction to the language inclusion problem for tree automata [6]. In [11], an algorithm
is developed to handle various kinds of (possibly nested) singly-linked lists based on a reduction to the
membership problem for tree automata. The complexity of the procedure is dominated by the boolean
satisfiability and unsatisfiability tests, that are NP and co-NP complete, respectively. A polynomial
proof procedure has been devised for the specific case of singly-linked lists [7]. In [5], the tractabil-
ity result is extended to more expressive fragments, with formulas defined on some unique nonlinear
compositional inductive predicate with distinguished source, destination, and static parameters. The
compositional properties satisfied by the considered predicate (as originally introduced in [12]) ensure
that the entailment problem can be solved efficiently. Recently [18] introduced a polynomial-time
cyclic proof system to solve entailment problem efficiently, under some conditions on the inductive
rules.

In the present paper, we study the complexity of the entailment problem for a specific fragment
that is similar to the PCE fragment, but simpler. The fragment inherits most of the conditions given in
[13] and admits an additional restriction that is meant to ensure that entailment problems can be solved
in a more efficient way<fnref n="1" />: every predicate is bound to allocate *exactly* one of its parameters (forbidding
for instance predicates denoting doubly-linked list segments from $x$ to $y$, as both $x$ and $y$ would be
allocated). This means that the rules do not allow for multiple pointers *into* a data structure (whereas
multiple pointers *out* of the structure are allowed). We first show that this additional restriction is actu-

<footnote n="1">¹At the cost, of course, of a loss of expressivity.</footnote>
ally not sufficient to ensure tractability. More precisely, we establish several lower-bound complexity results for the entailment problem under various additional hypotheses. Second, we define a new class of inductive definitions for which the entailment problem can be solved in polynomial time, based mainly on the two following additional restrictions: (i) the arity of the predicates is bounded; and (ii) the rules defining the same predicate do not overlap, in a sense that will be formally defined below. Both conditions are rather natural restrictions in the context of programming. Indeed, the number of parameters is usually small in this context. Also, data structures are typically defined using a finite set of free constructors, which yields inductive definitions that are trivially non-overlapping.

If Condition (i) is not satisfied, then the complexity is simply exponential. In contrast with other polynomial-time algorithms, the formulas we consider may contain several inductive predicates, and these predicates are possibly non-compositional (in the sense of [11]). The algorithm for testing entailment is defined as a sequent-like cyclic proof procedure, with standard unfolding and decomposition rules, together with a specific strategy ensuring efficiency and additional syntactic criteria to detect and dismiss non-provable sequents. Our approach is close to that of [18], in the sense that the two procedures use cyclic proof procedures with non-disjunctive consequents. However, the conditions on the rules are completely different: our definition allows for multiple inductive rules with mutually recursive definitions, yielding richer recursive data structures. On the other hand, the SHLIDe rules in [18] support ordering and equality relations on non-addressable values, whereas the predicate we consider are purely spatial. Moreover, the base cases of the rules in [18] correspond to empty heaps, which are forbidden in our approach.

To provide some intuition on what can and cannot be expressed in the fragment we consider, we provide some examples (formal definitions will be given later); consider the predicate P defined by the following rules, which encode a combination of lists and trees, possibly looping on an initial element y, and ending with an empty tuple:

$$P(x, y) \Leftarrow x \mapsto (\mathit{list}, u) * P(u, y)$$

$$P(x, y) \Leftarrow x \mapsto (\mathit{tree}, u_1, u_2) * P(u_1, y) * P(u_2, y)$$

$$P(x, y) \Leftarrow x \mapsto (\mathit{loop}, y)$$

$$P(x, y) \Leftarrow x \mapsto ()$$

All variables are implicitly universally quantified at the root level in every rule<fnref n="2" />. The constants list, tree and loop may be viewed as constructors for the data structure. This predicate does not fall in the scope of the fragment considered in [18] since it involves a definition with several inductive rules, but it falls in the scope of the fragment considered in the present paper. Our restrictions require that the definition must be deterministic, in the sense that there can be no overlap between distinct rules. This is the case here, as the tuples (list, u), (tree, u₁, u₂) and (loop, y) are pairwise distinct (not unifiable), but replacing for instance the constant loop by list in the third rule would not be possible, as the resulting rule would overlap with the first one (both rules could allocate the same heap cell). As explained above, a key limitation of our fragment (compared to that of [13]) is that it does not allow predicates allocating several parameters, such as the following predicate *dllseg(x, y, z, u)*

<footnote n="2">²Alternatively, the variables *u*, *u*₁, *u*₂, which do not occur in the left-hand side of the rules, may be viewed as being quantified existentially on the right-hand side of *<*.</footnote>
defining a doubly-linked list segment from $x$ to $z$ (each cell points to a pair containing the previous and next element and $y$ and $u$ denote the previous and next element in the list, respectively):

$$ \mathrm{dllseg}(x, y, z, u) \leftarrow (x \mapsto (y, x') * \mathrm{dllseg}(x', x, z, u)) \wedge x \not\approx z $$

$$ \mathrm{dllseg}(x, y, z, u) \leftarrow x \mapsto (y, u) \wedge x \approx z $$

Other definitions of `dllseg` are possible, but none would fit in with our restrictions: in every case, both $x$ (the beginning of the list) and $z$ (its end) must be eventually allocated, which is not permitted in the fragment we consider. On the other hand, the following predicate, defining a doubly-linked list, ending with `()`, can be defined ($y$ denotes the previous element in the list):

$$ \mathrm{dll}(x, y) \leftarrow x \mapsto (y, z) * \mathrm{dll}(z, x) $$

$$ \mathrm{dll}(x, y) \leftarrow x \mapsto () $$

The rest of the paper is organised as follows. In Section 2, the syntax and semantics of the logic are defined. The definitions are mostly standard, although we consider a multisorted framework, with a special sort `loc` denoting memory locations and additional sorts for data or constructors. We then introduce a class of inductive definitions called P-rules. In Section 3, various lower bounds on the complexity of the entailment problem for SL formulas with P-rules are established which allow one to motivate additional restrictions on the inductive rules. These lower bounds show that all the restrictions are necessary to ensure that the entailment problem is tractable. This leads to the definition of the notion of a loc-deterministic set of rules, that is a subset of P-rules for which entailment can be decided in polynomial time. The proof procedure is defined in Section 4. For the sake of readability and generality we first define generic inference rules and establish their correctness, before introducing a specific strategy to further restrict the application of the rules that is both complete and efficient. Section 5 contains all soundness, completeness and complexity results and Section 6 concludes the paper.

# 2. Definitions

## 2.1. Syntax

We use a multisorted framework, which is essentially useful to distinguish locations from data. Let $\mathfrak{S}$ be a set of sorts, containing a special sort `loc`, denoting memory locations. Let $\mathcal{V}_{s \in \mathfrak{S}}$ be a family of countably infinite disjoint sets of variables of sort $s$, with $\mathcal{V} \stackrel{\mathrm{def}}{=} \bigcup_{s \in \mathfrak{S}} \mathcal{V}_s$. Let $\mathcal{C}_{s \in \mathfrak{S}}$ be a family of disjoint sets of constant symbols of sort $s$, also disjoint from $\mathcal{V}$, with $\mathcal{C} \stackrel{\mathrm{def}}{=} \bigcup_{s \in \mathfrak{S}} \mathcal{C}_s$. The set of terms of sort $s$ is $\mathcal{T}_s \stackrel{\mathrm{def}}{=} \mathcal{V}_s \cup \mathcal{C}_s$, and we let $\mathcal{T} \stackrel{\mathrm{def}}{=} \bigcup_{s \in \mathfrak{S}} \mathcal{T}_s$. Constants are especially useful in our framework to denote constructors in data structures. To simplify technicalities, we assume that there is no constant of sort `loc`, i.e., $\mathcal{C}_{\mathrm{loc}} = \emptyset$.

An equation (resp. a disequation) is an expression of the form $t \approx s$ (resp. $t \not\approx s$) where $t, s \in \mathcal{T}_s$ for some $s \in \mathfrak{S}$. The set of pure formulas $\mathcal{F}_P$ is the set of formulas of the form $e_1 \wedge \cdots \wedge e_n$, where every expression $e_i$ is either an equation or a disequation. Such formulas are considered modulo
contraction, e.g., a pure formula $\xi \wedge \xi$ is considered identical to $\xi$, and also modulo associativity and commutativity of conjunction. We denote by $\perp$ (false) any formula of the form $t \not\approx t$. If $n = 0$, then $\bigwedge_{i=1}^n e_i$ may be denoted by $\top$ (true). If $(t_1, \dots, t_n)$ and $(s_1, \dots, s_m)$ are vectors of terms, then $(t_1, \dots, t_n) \approx (s_1, \dots, s_m)$ denotes the formula $\perp$ if either $n \neq m$ or $n = m$ and there exists $i \in \{1, \dots, n\}$ such that $s_i$ and $t_i$ are of different sorts; and denotes $\bigwedge_{i=1}^n t_i \approx s_i$ otherwise.

Let $\mathcal{P}$ be a set of predicate symbols. Each symbol in $\mathcal{P}$ is associated with a unique profile of the form $(s_1, \dots, s_n)$ with $n \ge 1$, $s_1 = \text{loc}$ and $s_i \in \mathfrak{S}$, for all $i \in \{2, \dots, n\}$. We write $p : s_1, \dots, s_n$ to denote a symbol with profile $(s_1, \dots, s_n)$ and we write $p : s_1, \dots, s_n \in \mathcal{P}$ to state that $p$ is a predicate symbol of profile $s_1, \dots, s_n$ in $\mathcal{P}$. A spatial atom $\alpha$ is either a points-to atom $x \mapsto (t_1, \dots, t_n)$ with $x \in \mathcal{V}_{\text{loc}}$ and $t_1, \dots, t_n \in \mathcal{T}$, or a predicate atom of the form $p(x, t_1, \dots, t_n)$, where $p$ is a predicate of profile loc, $s_1, \dots, s_n$ in $\mathcal{P}$, the term $x$ is a variable in $\mathcal{V}_{\text{loc}}$ and $t_i \in \mathcal{T}_{s_i}$ for all $i \in \{1, \dots, n\}$. In both cases, the variable $x$ is called the root of $\alpha$ and is denoted by $\text{root}(\alpha)$.

The set of spatial formulas $\mathcal{F}_S$ is the set of formulas of the form $\beta_1 * \dots * \beta_n$, where every expression $\beta_i$ is a spatial atom. If $n = 0$ then $\beta_1 * \dots * \beta_n$ is denoted by $\text{emp}$. The number $n$ of occurrences of spatial atoms in a spatial formula $\phi = \beta_1 * \dots * \beta_n$ is denoted by $\text{len}(\phi)$. We write $\phi \sqsubseteq \psi$ if $\psi$ is of the form $\phi * \phi'$, modulo associativity and commutativity of $*$. The set of (non quantified) symbolic heaps $\mathcal{F}_H$ is the set of expressions of the form $\phi \lambda \xi$, where $\phi \in \mathcal{F}_S$ and $\xi \in \mathcal{F}_P$. Note that for clarity we use $\lambda$ to denote conjunctions between spatial and pure formulas and $\wedge$ to denote conjunctions occurring within pure formulas. If $\xi = \top$, then $\phi \lambda \xi$ may be written $\phi$ (i.e., any spatial formula may be viewed as a symbolic heap). For any formula $\lambda$, $|\lambda|$ denotes the size of $\lambda$ (which is defined inductively as usual). Note that $\top$ is not a symbolic heap (but $\text{emp} \lambda \top$ is a symbolic heap).

We denote by $\mathcal{V}(\beta)$ (resp. $\mathcal{V}_s(\beta)$) the set of variables (resp. of variables of sort $s$) occurring in a variable or formula $\beta$. A substitution is a sort-preserving total mapping from $\mathcal{V}$ to $\mathcal{T}$. We denote by $\text{dom}(\sigma)$ the set of variables such that $\sigma(x) \neq x$, and by $\text{codom}(x)$ the set $\{\sigma(x) \mid x \in \text{dom}(\sigma)\}$. The substitution $\sigma$ such that $\sigma(x_i) = y_i$ for all $i = 1, \dots, n$ and $\text{dom}(\sigma) \subseteq \{x_1, \dots, x_n\}$ is denoted by $\{x_i \leftarrow y_i \mid i = 1, \dots, n\}$. For any expression $\beta$ and substitution $\sigma$, we denote by $\beta\sigma$ the expression obtained from $\beta$ by replacing every variable $x$ by $\sigma(x)$. A unifier of two expressions or tuples of expressions $\beta$ and $\beta'$ is a substitution $\sigma$ such that $\beta\sigma = \beta'\sigma$.

An inductive rule is an expression of the form $p(x_1, \dots, x_n) \Leftarrow \lambda$, where $p : s_1, \dots, s_n \in \mathcal{P}$, $x_1, \dots, x_n$ are pairwise distinct variables of sorts $s_1, \dots, s_n$ respectively and $\lambda \in \mathcal{F}_H$. The set of variables in $\mathcal{V}(\lambda) \setminus \{x_1, \dots, x_n\}$ are the existential variables of the rule. Let $\mathfrak{R}$ be a set of inductive rules. We write $p(t_1, \dots, t_n) \Leftarrow_{\mathfrak{R}} \lambda$ iff $\mathfrak{R}$ contains (up to a renaming, and modulo AC) a rule of the form $p(y_1, \dots, y_n) \Leftarrow \gamma$ and $\lambda = \gamma\{y_i \leftarrow t_i \mid i = 1, \dots, n\}$. We assume by renaming that $\gamma$ contains no variable in $\{t_1, \dots, t_n\}$. We write $p(t_1, \dots, t_n) \rightsquigarrow_{\mathfrak{R}} E$ if $E$ is the set of symbolic heaps $\lambda$ such that $p(t_1, \dots, t_n) \Leftarrow_{\mathfrak{R}} \lambda$. Note that if $\mathfrak{R}$ is finite then $E$ is finite up to a renaming of variables not occurring in $\{t_1, \dots, t_n\}$. Note also that the considered logic does not allow for negations (hence entailment is not reducible to satisfiability) or separating implications, as this would make satisfiability undecidable (see for instance [19]).

The symbol $\subseteq_m$ denotes the inclusion relation between multisets. With a slight abuse of notations, we will sometimes identify sequences with sets when the order and number of repetitions is not important, for instance we may write $x \subseteq y$ to state that every element of $x$ occurs in $y$.
In the present paper, we shall consider entailment problems between symbolic heaps.

## 2.2. Semantics

We assume for technical convenience that formulas are interpreted over a fixed universe and that constants are interpreted as pairwise distinct elements. Let $\mathfrak{U}_{s \in \mathcal{G}}$ be pairwise disjoint countably infinite sets and let $\mathfrak{U} \stackrel{\text{def}}{=} \bigcup_{s \in \mathcal{G}} \mathfrak{U}_s$. We assume that an injective function is given, mapping every constant $c \in C_s$ to an element of $\mathfrak{U}_s$, denoted by $\dot{c}$.

A heap is a partial finite function from $\mathfrak{U}_{\text{loc}}$ to $\mathfrak{U}^*$, where $\mathfrak{U}^*$ denotes as usual the set of finite sequences of elements of $\mathfrak{U}$. An element $\ell \in \mathfrak{U}_{\text{loc}}$ is allocated in a heap $\mathfrak{h}$ if $\ell \in \text{dom}(\mathfrak{h})$. Two heaps $\mathfrak{h}$ and $\mathfrak{h}'$ are disjoint if $\text{dom}(\mathfrak{h}) \cap \text{dom}(\mathfrak{h}') = \emptyset$, in which case $\mathfrak{h} \uplus \mathfrak{h}'$ denotes their disjoint union. We write $\mathfrak{h} \subseteq \mathfrak{h}'$ if there is a heap $\mathfrak{h}''$ such that $\mathfrak{h}' = \mathfrak{h} \uplus \mathfrak{h}''$. For every heap $\mathfrak{h}$, we denote by $\text{ref}(\mathfrak{h})$ the set of elements $\ell \in \mathfrak{U}_{\text{loc}}$ such that there exists $\ell_0, \dots, \ell_n$ with $\ell_0 \in \text{dom}(\mathfrak{h})$, $\mathfrak{h}(\ell_0) = (\ell_1, \dots, \ell_n)$ and $\ell = \ell_i$ for some $i = 0, \dots, n$. We write $\ell \to_{\mathfrak{h}} \ell'$ if $(\ell, \ell') \in \mathfrak{U}_{\text{loc}}^2$, $\ell \in \text{dom}(\mathfrak{h})$, $\mathfrak{h}(\ell) = (\ell_1, \dots, \ell_n)$ and $\ell' = \ell_i$, for some $i = 1, \dots, n$.

**Proposition 2.1.** Let $\mathfrak{h}, \mathfrak{h}'$ be two heaps such that $\mathfrak{h} \subseteq \mathfrak{h}'$. For all $\ell, \ell' \in \mathfrak{U}_{\text{loc}}$, if $\ell \to_{\mathfrak{h}}^* \ell'$ then $\ell \to_{\mathfrak{h}', 1}^* \ell'$.

**Proof:**

By definition of the relation $\to_{\mathfrak{h}}$ we have $\to_{\mathfrak{h}} \subseteq \to_{\mathfrak{h}', 1}$, thus $\to_{\mathfrak{h}}^* \subseteq \to_{\mathfrak{h}', 1}^*$

<figure><img src="image_2.png" /></figure>

A store $\mathfrak{s}$ is a total function mapping every term in $T_s$ to an element in $\mathfrak{U}_s$ such that $\mathfrak{s}(c) = \dot{c}$, for all $c \in C$ (note that this entails that $\mathfrak{s}$ is injective on $C$). A store $\mathfrak{s}$ is *injective on a multiset of variables* $V$ if $\{x, y\} \subseteq_m V \implies \mathfrak{s}(x) \neq \mathfrak{s}(y)$. When a store is injective on a multiset of variables, this entails that the latter is a set, i.e., that contains at most one occurrence of each variable. For any $V \subseteq V$, and for any store $\mathfrak{s}$, a store $\mathfrak{s}'$ is an *associate of s w.r.t.* $V$ if $\mathfrak{s}(x) = \mathfrak{s}'(x)$ holds for all $x \notin V$.

**Definition 2.2.** An SL-structure is a pair $(\mathfrak{s}, \mathfrak{h})$, where $\mathfrak{s}$ is a store and $\mathfrak{h}$ is a heap.

The satisfiability relation on SL-formulas is defined inductively as follows:

**Definition 2.3.** An SL-structure $(\mathfrak{s}, \mathfrak{h})$ validates a formula (pure formula, spatial formula, or symbolic heap) $\lambda$ modulo a set of inductive rules $\mathfrak{R}$, written $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \lambda$, if one of the following conditions holds:

* $\lambda = \text{emp}$ and $\mathfrak{h} = \emptyset$;

* $\lambda = (t \approx s)$ and $\mathfrak{s}(t) = \mathfrak{s}(s)$;

* $\lambda = (t \not\approx s)$ and $\mathfrak{s}(t) \neq \mathfrak{s}(s)$;

* $\lambda = x \mapsto (t_1, \dots, t_k)$ and $\mathfrak{h} = \{(\mathfrak{s}(x), \mathfrak{s}(t_1), \dots, \mathfrak{s}(t_k))\}$;

* either $\lambda = \lambda_1 \wedge \lambda_2$ or $\lambda = \lambda_1 \wedge \lambda_2$, and $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \lambda_i$ for all $i = 1, 2$;
* $\lambda = \lambda_1 * \lambda_2$ and there exist disjoint heaps $h_1$ and $h_2$ such that $h = h_1 \uplus h_2$ and $(s, h_i) \models_{\mathfrak{R}} \lambda_i$ for all $i = 1, 2$;

* $\lambda = p(t_1, \dots, t_n)$ and $p(t_1, \dots, t_n) \Leftarrow_{\mathfrak{R}} \gamma$, where there exists an associate $s'$ of $s$ w.r.t. the set $V(\gamma) \setminus V(\lambda)$ such that $(s', h) \models_{\mathfrak{R}} \gamma$.

An $\mathfrak{R}$-model of a formula $\lambda$ is a structure $(s, h)$ such that $(s, h) \models_{\mathfrak{R}} \lambda$. A formula is satisfiable (w.r.t. $\mathfrak{R}$) if it admits at least one $\mathfrak{R}$-model.

**Remark 2.4.** Note that a formula $x \mapsto (t_1, \dots, t_k)$ asserts not only that $x$ refers to $(t_1, \dots, t_k)$ but also that $x$ is the only allocated location. This fits with usual definitions (see, e.g., [15]). The assertions are meant to describe elementary heaps, which can be combined afterwards using the connective $*$. Simply asserting that $x$ refers to $(t_1, \dots, t_k)$ could be done in full SL using the following formula: $x \mapsto (t_1, \dots, t_k) * \top$, but such a formula is not a symbolic heap and is thus outside of the fragment we consider in the present paper.

We write $(s, h) \models_{\mathfrak{R}} \lambda$ instead of $(s, h) \models_{\mathfrak{R}} \lambda$ if $\lambda$ contains no predicate symbol, since the relation is independent of $\mathfrak{R}$ in this case. Similarly, if $\lambda$ is a pure formula then the relation does not depend on the heap, thus we may simply write $s \models_{\mathfrak{R}} \lambda$.

**Remark 2.5.** Note that there is no symbolic heap that is true in every structure. For instance $emp \triangleleft \top$ is true only in structures with an empty heap.

**Proposition 2.6.** Let $(s, h)$ be a structure and let $\sigma$ be a substitution. If $(s, h) \models_{\mathfrak{R}} \lambda \sigma$ then we have $(s \circ \sigma, h) \models_{\mathfrak{R}} \lambda$.

**Proof:**

By an immediate induction on the satisfiability relation. $\square$

In the present paper, we shall consider inductive rules of a particular form, defined below.

**Definition 2.7.** An inductive rule is a P-rule if it is of the form

$$p(x_1, \dots, x_n) \Leftarrow x_1 \mapsto (y_1, \dots, y_k) * q_1(z_1, u_1) * \dots * q_m(z_m, u_m) \triangleleft \xi$$

possibly with $m = 0$, where:

1. $\xi$ is a conjunction of disequations of the form $u \not\approx v$, where $u \in \{x_1, \dots, x_n, y_1, \dots, y_k\}$ and $v \in \{y_1, \dots, y_k\} \setminus \{x_1, \dots, x_n\}$;

2. $\{z_1, \dots, z_m\} = (\{y_1, \dots, y_k\} \setminus \{x_1, \dots, x_n\}) \cap V_{\text{loc}}$, and $z_1, \dots, z_m$ are pairwise distinct;

3. All the elements of $u_i$ occur in $\{x_1, \dots, x_n\} \cup \{y_1, \dots, y_k\} \cup C$.

The predicate symbol $p$ is called the head of the rule.
<figure><img src="image_3.png" /><figcaption>Figure 1. Doubly-linked list ending with () ($\ell_{n+1}$ is allocated but has no successor)</figcaption></figure>

**Example 2.8.** The rules associated with `ls` and `tree` in the introduction are P-rules, as well as the following rules. Intuitively `als(x, y) ∧ x ≠ y` denotes an acyclic list (`als(x, y)` is thus “quasi-acyclic”, in the sense that it may loop only on the first element). Note that the constraint `x ≠ y` cannot be added to the right-hand side of the rules because the obtained rule would not be a P-rule, hence it must be added in the formula. The atom `dll(x, y)` denotes a doubly-linked list starting at `x`, with the convention that each element of the list points to a pair containing the previous and next elements. The parameter `y` denotes the element before `x` (if any) and the last element points to the empty tuple `()`. The structures validating `dll(x, y)` are of the form (see Figure 1) `(s_n, h_n)` with `n ≥ 0`, `dom(h) = {l_1, ..., l_{n+1}}`, `h(l_i) = (l_{i-1}, l_{i+1})` for all `i ∈ {1, ..., n}`, `h(l_{n+1}) = ()`, `s(x) = l_1` and `s(y) = l_0`. Locations `l_1, ..., l_{n+1}` must be pairwise distinct and `l_0` is arbitrary. The atom `tptr(x, y, z)` denotes a binary tree in which every node refers to its two successors and to its parent and sibling nodes. The parameters `y` and `z` denote the sibling and parent nodes, respectively. Leaves point to `()`. See Figure 2 for an example with 5 allocated locations.

<table><tr><td>als(x, y)</td><td>⇔ (x ↦ (z) * als(z, y)) ∧ y ≠ z</td><td>% (quasi-)acyclic list</td></tr><tr><td>als(x, y)</td><td>⇔ x ↦ (y)</td><td></td></tr><tr><td>tll(x, y)</td><td>⇔ x ↦ (y, z) * tree(z)</td><td>% binary trees with</td></tr><tr><td>tll(x, y)</td><td>⇔ (x ↦ (z, u) * tll(z, y) * tree(u))</td><td>% leftmost leaf y</td></tr><tr><td>dll(x, y)</td><td>⇔ x ↦ (y, z) * dll(z, x)</td><td>% doubly-linked lists</td></tr><tr><td>dll(x, y)</td><td>⇔ x ↦ ()</td><td></td></tr><tr><td>tptr(x, y, z)</td><td>⇔ x ↦ (u, v, y, z) * tptr(u, v, x)</td><td>% binary trees with</td></tr><tr><td>tptr(x, y, z)</td><td>*tptr(v, u, x)</td><td>% pointers to brother</td></tr><tr><td>tptr(x, y, z)</td><td>⇔ x ↦ ()</td><td>% and parent nodes</td></tr></table>

The following rules are not P-rules (if all variables are of sort `loc`):

<table><tr><td>p(x)</td><td>⇔ x ↦ (z)</td><td>Condition 2 violated</td></tr><tr><td>p(x)</td><td>⇔ ls(x, z) * p(z)</td><td>No points-to atom</td></tr><tr><td>q(x, y)</td><td>⇔ x ↦ (z) ∧ y ≈ z</td><td>Condition 2 violated</td></tr><tr><td>q(x, y)</td><td>⇔ ls(x, y)</td><td>No points-to atom</td></tr><tr><td>als(x, y)</td><td>⇔ (x ↦ (z) * als(z, y)) ∧ x ≠ y</td><td>Condition 1 violated</td></tr><tr><td>als(x, y)</td><td>⇔ x ↦ (y) ∧ x ≠ y</td><td>Condition 1 violated</td></tr></table>
<figure><img src="image_4.png" /><figcaption>Figure 2. Binary tree with pointers to parent and sibling ($l_2, l_3, l_4$ are allocated but have no successor)</figcaption></figure>

**Remark 2.9.** As evidenced by the rules in Example 2.8, the tuple () is frequently used as a base case, to end a data structure. This departs from standard conventions in SL in which a non-allocated constant nil is frequently used instead. We avoid considering constants of sort loc in our framework because this would complicate definitions: one would have to keep track of allocated and non-allocated constants and/or to add syntactic conditions on the formulas and rules to ensure that such constants are never allocated. Note that this convention introduces an asymmetry in the structure. For instance, in doubly-linked lists, the “next” field of the last element points to () while the “previous” field of the first element contains an arbitrary location y. To achieve symmetry in the structure, one could introduce an atom $y \mapsto ()$. For example, the formula $y \mapsto () * dll(x, y)$ represents a doubly-linked list ending with () in both directions.

Note that P-rules are progressing and connected (in the sense of [13]): every rule allocates exactly one location –the first parameter of the predicate– and the first parameter of every predicate in the body of the rule occurs in the right-hand side of the (necessarily unique) points-to atom of the rule. They are not necessarily established (again in the sense of [13]) as non-allocated existential variables are allowed provided they are not of sort loc.

**Example 2.10.** The following (non established, in the sense of [13]) rules, denoting list segments with unallocated elements are P-rules iff $u \notin V_{loc}$:

$$ \mathbf{ls}(x, y) \Leftarrow x \mapsto (u, y) \qquad \mathbf{ls}(x, y) \Leftarrow x \mapsto (u, z) * \mathbf{ls}(z, y) $$

The heap of any model of $\mathbf{ls}(x, y)$ is of the form $\{l_i \mapsto (u_i, l_{i+1}) | i \in \{1, \dots, n\}\}$, where $u_1, \dots, u_n$ denote arbitrary elements (of a sort distinct from loc).

P-Rules containing no variable of a sort distinct from loc are established. P-Rules also differ from PCE rules in that every predicate allocates exactly one of its parameters, namely the first one (the other allocated locations are associated with existential variables). In other words, there may be only
one “entry point” to the structure allocated by a predicate, namely its root. For instance the rule $p(x, y) \leftarrow x \mapsto (y) * q(y)$ (along with another rule for symbol $q$, e.g., $q(y) \leftarrow y \mapsto (\quad)$) is PCE but it is not a P-rule, whereas $p(x) \leftarrow x \mapsto (y) * q(y)$ is a P-rule. Such a restriction makes the entailment problem easier to solve because it rules out data structures that can be constructed in different orders (for instance doubly-linked lists with a reference to the end of the list).

We introduce some useful notations and measures on sets of P-rules. For every set of P-rules $\mathfrak{R}$, we denote by $\mathcal{P}(\mathfrak{R})$ the set of predicate symbols occurring in a rule in $\mathfrak{R}$. We define:

$$ar_{max}(\mathfrak{R}) = \max\{n \mid p : s_1, \dots, s_n \in \mathcal{P}(\mathfrak{R})\}$$

and

$$record_{max}(\mathfrak{R}) = \max\{k \mid p(x_1, \dots, x_n) \leftarrow (x \mapsto (t_1, \dots, t_k) * \phi) \wedge \xi \in \mathfrak{R}\}$$

The numbers $ar_{max}(\mathfrak{R})$ and $record_{max}(\mathfrak{R})$ respectively denote the maximum arity of the predicate symbols in $\mathfrak{R}$ and the maximum number of record fields in a points-to atom occurring in $\mathfrak{R}$. The width of $\mathfrak{R}$ is defined as follows: $width(\mathfrak{R}) \stackrel{\text{def}}{=} \max(ar_{max}(\mathfrak{R}), record_{max}(\mathfrak{R}))$.

We make two additional assumptions about the considered set of rules: we assume that every predicate is productive (Assumption 2.12) and that no parameter is useless (Assumption 2.15). More precisely, the set of productive predicate symbols is inductively defined as follows: $p \in \mathcal{P}$ is productive w.r.t. a set of inductive rules $\mathfrak{R}$ if $\mathfrak{R}$ contains a rule $p(x) \leftarrow \lambda$ such that all the predicate symbols occurring in $\lambda$ are productive. In particular, a rule with no predicate in its right-hand side is always productive (base case). Productive rules can easily be computed using a straightforward least fixpoint algorithm.

**Example 2.11.** Let $\mathfrak{R} = \{p(x) \leftarrow q(x), q(x) \leftarrow p(x), r(x) \leftarrow x \mapsto (y) * p(y)\}$. The predicates $p, q, r$ are not productive.

It is easy to check that every formula containing at least one non-productive predicate symbol is unsatisfiable. Indeed, if a predicate symbol $p$ is non-productive, then an atom $p(x)$ cannot be unfolded into a formula containing no predicate symbol. This justifies the following:

**Assumption 2.12.** For all sets of P-rules $\mathfrak{R}$, we assume that all the predicate symbols are productive w.r.t. $\mathfrak{R}$.

For all predicates $p : s_1, \dots, s_n$, the set $out_{\mathfrak{R}}(p)$ denotes the least set of indices $i$ in $\{1, \dots, n\}$ such that $s_i = \text{loc}$ and there exists a rule $p(x_1, \dots, x_n) \leftarrow \lambda$ in $\mathfrak{R}$ such that $\lambda$ contains either a points-to atom $x_1 \mapsto (t_1, \dots, t_k)$ where $x_i \in \{t_1, \dots, t_k\}$ or a predicate atom $q(t_1, \dots, t_m)$ with $t_j = x_i$, for some $j \in out_{\mathfrak{R}}(q)$. Intuitively, $out_{\mathfrak{R}}(p)$ denote the set of “out-going” nodes of the structures corresponding to $p$, i.e., the set of parameters corresponding to locations that can be referred to but not necessarily allocated.

**Example 2.13.** Consider the following rules:

$$p(x, y, z) \leftarrow x \mapsto (x, y) \quad p(x, y, z) \leftarrow x \mapsto (x, u) * q(u, z, z) \quad q(x, y, z) \leftarrow x \mapsto (y)$$

Then $out_{\mathfrak{R}}(p) = \{1, 2\}$ and $out_{\mathfrak{R}}(q) = \{2\}$.
### 3. Lower Bounds

We establish various lower bounds for the validity problems for sequents $\lambda \vdash_{\mathfrak{R}} \gamma$, where $\mathfrak{R}$ satisfies some additional conditions. These lower bounds will motivate the additional restrictions that are imposed to devise a polynomial-time proof procedure.

Checking the validity of sequents $\lambda \vdash_{\mathfrak{R}} \gamma$ where $\mathfrak{R}$ is a set of P-rules is actually undecidable in general. This result can be established by an argument similar to the one used in [10] to prove the undecidability of PCE entailments modulo theories; it is not given here for the sake of conciseness, and because the goal of this paper is to investigate tractable cases. The undecidability proof relies on the existence of variables of a sort distinct from loc. If such variables are forbidden, then the rules are PCE hence entailment is decidable [13], but we still get an EXPTIME lower bound:

**Proposition 3.1.** Checking the validity of sequents $\lambda \vdash_{\mathfrak{R}} \gamma$ is EXPTIME-hard, even if $\mathfrak{R}$ is a set of P-rules and all the variables occurring in $\lambda \vdash_{\mathfrak{R}} \gamma$ are of sort loc.

**Proof:**

The proof is by a straightforward reduction from the inclusion problem for languages accepted by tree automata (see [6]). Indeed, a tree automaton $(Q, V, \{q_0\}, R)$ can be straightforwardly encoded as a set of P-rules, where each rule $q \to f(q_1, \dots, q_n)$ in $R$ is encoded by an inductive rule of the form $q(x) \Leftarrow x \mapsto (f, x_1, \dots, x_n) * \mathbf{*}_{i=1}^n q_i(x_i)$. Each function symbol $f$ is considered as a constant of a sort $\mathfrak{s} \neq \text{loc}$, and a term $f(t_1, \dots, t_n)$ is represented as a heap $\mathfrak{h}_1 \uplus \dots \uplus \mathfrak{h}_n \uplus \{(\ell_0, \ell_1, \dots, \ell_n)\}$, where $\ell_0, \dots, \ell_n$ are pairwise distinct locations and $\mathfrak{h}_1, \dots, \mathfrak{h}_n$ are disjoint representations of $t_i$ with $\ell_0 \notin \text{dom}(\mathfrak{h}_i)$, for $i = 1, \dots, n$. It is straightforward to verify that the language accepted by $(Q, V, \{q_0\}, R)$ is included in that of $(Q', V, \{q'_0\}, R')$ iff the sequent $q_0(x) \vdash_{\mathfrak{R}} q'_0(x)$ is valid. $\square$

Since the inclusion problem is polynomial for top-down deterministic tree automata [6], it is natural to further restrict the considered rules to make them deterministic, in the following sense:

**Definition 3.2.** A set of P-rules $\mathfrak{R}$ is *deterministic* if for all pairs of distinct rules of the form $p(x_i) \Leftarrow (y_i \mapsto t_i * \phi_i) \wedge \xi_i$ (where $i = 1, 2$) occurring in $\mathfrak{R}$, the formula $x_1 \approx x_2 \wedge t_1 \approx t_2 \wedge \xi_1 \wedge \xi_2$ is unsatisfiable (we assume by renaming that the rules share no variable).

For instance the rules associated with the predicate `ls` in the introduction are not deterministic, whereas the rules associated with `tree` are deterministic, as well as all those in Example 2.8. For the predicate `ls`, the formula $x \approx x' \wedge y \approx z$ is satisfiable, whereas for the predicate `tree`, the formula $x \approx x' \wedge () \approx (y, z)$ is unsatisfiable (in both cases the variable $x$ is renamed by $x'$ in the second rule).

The following proposition shows that the restriction to deterministic sets of P-rules is still not sufficient to obtain a tractable validity problem:

**Proposition 3.3.** Checking the validity of sequents $\lambda \vdash_{\mathfrak{R}} \gamma$ is PSPACE-hard, even if $\mathfrak{R}$ is a deterministic set of P-rules and all variables in $\lambda \vdash_{\mathfrak{R}} \gamma$ are of sort loc.
**Proof:**

Let “$w \in E$” be any problem in PSPACE. By definition, there exists a Turing machine $M = (Q, \Sigma, B, \Gamma, \delta, q_0, F)$ accepting exactly the words in $E$ and a polynomial $R$ such that $M$ runs in space $R(n)$ on all words $w \in \Sigma^n$. The set $Q$ denotes the set of states of $M$, $\Sigma$ is the input alphabet, $B$ is the blank sumbol, $\Gamma$ is the tape alphabet, $\delta$ is the transition function, $q_0$ is the initial state and $F$ is the set of final states. We shall reduce the problem “$w \in E$” to the entailment problem, for a sequent fulfilling the conditions above. Consider a word $w$ of length $n$, and let $N = R(n)$. Assume that $C$ contains all the elements in $\Gamma$. We consider $card(Q) \cdot N$ predicates $q^i$ of arity $N + 3$, for all $q \in Q$ and $i \in \{1, \dots, N\}$, associated with the following rules:

$$ 
\begin{array}{l}
q^i(x, y_1, \dots, y_N, u, v) \Leftarrow x \mapsto (x', u, v, a) * p^{i+\mu}(x', y_1, \dots, y_{i-1}, b, y_{i+1}, \dots, y_N, y_i, a) \\
\phantom{q^i(x, y_1, \dots, y_N, u, v) \Leftarrow} \text{if } q \notin F \text{ and } \delta \text{ contains a rule } (q, a) \to (p, b, \mu) \\
\phantom{q^i(x, y_1, \dots, y_N, u, v) \Leftarrow} \text{with } i + \mu \in \{1, \dots, N\}
\end{array}
$$

$$ q^i(x, y_1, \dots, y_N, u, v) \Leftarrow x \mapsto (x, u, v, B), \text{ if } q \in F. $$

Intuitively, $q$ is the state of the machine, the arguments $y_1, \dots, y_N$ denote the tape (that is of length $N$ by hypothesis) and $i$ denotes the position of the head on the tape. The constants $a, b$ denote the symbols read and written on the tape, respectively, $p$ is the final state of the transition rule and the integer $\mu$ denotes the move, i.e., an element of $\{-1, 0, +1\}$, so that $i + \mu$ is the final position of the head on the tape. Note that at this point the inductive rule does not test whether the symbol $a$ is indeed identical to the symbol at position $i$, namely $y_i$. Instead, it merely stores both $y_i$ and $a$ within the next tuple of the heap, by passing them as parameters to $p^{i+\mu}$. The arguments $u$ and $v$ are used to encode respectively the symbol read on the tape at the previous state and the symbol that was expected. By definition of the above rules, it is clear that $q^i(x, y_1, \dots, y_N, B, B)$ holds if the heap is a list of tuples $(x_j, u_j, v_j, a_j)$, for $j = 1, \dots, k$, linked on the first argument (the last element loops on itself). The heap encodes a “candidate run” of length $k$ of $M$, i.e., a run for which one does not check, when applying a transition $(p, a) \to (q, b, \mu)$, that the symbol read on the tape is identical to the expected symbol $a$. The symbols $u_i, v_i, a_i$ stored at each node are precisely the symbols that are read $(u_i)$ and expected $(v_i)$ at the previous step, respectively, along with the symbol $(a_i)$ that is expected at the current step (this last symbol is added to ensure that the rules are deterministic). Note that for $i = 1$ there is no previous step and for $i = k$ no symbol is read since the state is final; thus by convention, $a_k$ is set to $B$ (see the last rule of $q^i$). Furthermore, $u_1, v_1$ will also be set to $B$ by invoking the initial state predicate with $B$ as the last two arguments (see the definition of the sequent below). To check that the list corresponds to an actual run of $M$, it thus suffices to check that $u_i = v_i$ holds for all $i = 1, \dots, k$.

The right-hand side of the sequent will allocate all structures not satisfying this condition. To this purpose, we associate with each state $r \in Q$ two predicate symbols $r_0$ and $r_1$ defined by the following rules (where $i, j \in \{0, 1\}$):

$$ 
\begin{array}{l}
r_i(x) \Leftarrow x \mapsto (x', a, b, c) * r_j(x') \\
\phantom{r_i(x) \Leftarrow} \text{for all } r \notin F, a, b, c \in \Gamma, \text{ where } j = 1 \text{ iff either } i = 1 \text{ or } a \neq b; \\
r_i(x) \Leftarrow x \mapsto (x, a, b, B) \quad \text{if } a, b \in \Gamma, r \in F \text{ and either } i = 1 \text{ or } a \neq b.
\end{array}
$$
Intuitively, the index $i$ in predicate $r_i$ is equal to 1 iff a faulty location has been encountered (i.e., a tuple $(x', a, b)$ with $a \neq b$).

Note that the number of rules is polynomial w.r.t. $N$, since the machine $M$ is fixed. Also, the obtained set of rules is deterministic, because $M$ is deterministic and the expected symbol is referred to by the location allocated by each predicate symbol $q^i$, thus the tuples $(x', u, v, a)$ corresponding to distinct rules associated with the same symbol $q^i$ cannot be unifiable.

Let $w_1, \dots, w_N = w.B^{N-n}$ be the initial tape (where $w$ is completed by blank symbols $B$ to obtain a word of length $N$). It is clear that the sequent $q_0^1(x, w_1, \dots, w_N, B, B) \vdash_{\mathfrak{R}} r_0(x)$ is valid iff all the “candidate runs” of $M$ fulfill the conditions of the right-hand side, i.e., falsify at least one equality between read and expected symbols. Thus $q_0^1(x, w_1, \dots, w_N, B, B) \vdash_{\mathfrak{R}} r_0(x)$ is valid iff $M$ does not accept $w$. $\square$

In view of this result, it is natural to investigate the complexity of the entailment problem when the maximal arity of the predicates is bounded. However, this is still insufficient to get a tractable problem, as the following lemma shows.

**Lemma 3.4.** Checking the validity of sequents $\lambda \vdash_{\mathfrak{R}} \gamma$ is co-NP-hard, even if $width(\mathfrak{R}) \le 4$ (i.e., if the symbols and tuples are of arity at most 4) and $\mathfrak{R}$ is a deterministic set of P-rules.

**Proof:**

The proof is by a reduction from the complement of the 3-coloring problem, that is well-known to be NP-complete. Let $G = (V, E)$ be a graph, where $V = \{v_1, \dots, v_n\}$ is a finite set of vertices and $E$ is a set of undirected edges, i.e., a set of unordered pairs of vertices. Let $\text{Colors} = \{a, b, c\}$ be a set of colors, with $\text{card}(\text{Colors}) = 3$. We recall that a solution of the 3-coloring problem is a function $f: V \to \text{Colors}$ such that $(x, y) \in E \implies f(x) \neq f(y)$. We assume, w.l.o.g., that all vertices occur in at least one edge. We consider two distinct sorts loc and s. We assume, w.l.o.g., that $V \cup \text{Colors} \subseteq V_s$ (i.e., $a, b, c$, as well as the set of vertices in $G$, are variables) and $V \cap \text{Colors} = \emptyset$.

Let $E = \{(x_i, y_i) \mid i = 1, \dots, m\}$ (where the edges are ordered arbitrarily) and let $u_1, \dots, u_{m+1}$ be pairwise distinct variables of sort loc. Let $\phi$ be the formula: $*_{i=1}^m u_i \mapsto (x_i, y_i, u_{i+1}) * u_{m+1} \mapsto ()$. Let $p$ and $q$ be predicate symbols associated with the following rules:

$$p(u, a, b, c) \Leftarrow u \mapsto (v, v, u') * q(u')$$

$$p(u, a, b, c) \Leftarrow u \mapsto (v_1, v_2, u') * v_1 \not\approx v_2 * v_1 \not\approx a * v_1 \not\approx b * v_1 \not\approx c * q(u')$$

$$p(u, a, b, c) \Leftarrow u \mapsto (d, v_2, u') * v_2 \not\approx a * v_2 \not\approx b * v_2 \not\approx c * q(u')$$
for all $d \in \{a, b, c\}$

$$p(u, a, b, c) \Leftarrow u \mapsto (d_1, d_2, u') * p(u', a, b, c)$$

for all $d_1, d_2 \in \{a, b, c\}$ where $d_1 \neq d_2$

$$q(u) \Leftarrow u \mapsto (v_1, v_2, u') * q(u')$$

$$q(u) \Leftarrow u \mapsto ()$$

Intuitively, any model $(\mathfrak{s}, \mathfrak{h})$ of $\phi$ encodes a candidate solution of the 3-coloring problem, where each variable $z \in \{x_1, \dots, x_m\} \cup \{y_1, \dots, y_m\}$ is mapped to an element $\mathfrak{s}(z)$ in $\mathfrak{U}_s$. The heap $\mathfrak{h}$ is
a list of tuples linked on the last element and containing a tuple $(\mathfrak{s}(u_i), \mathfrak{s}(x_i), \mathfrak{s}(y_i), \mathfrak{s}(u_{i+1}))$ for all $(x_i, y_i) \in E$. To check that this candidate solution indeed fulfills the required properties, one has to verify that all the pairs $(\mathfrak{s}(x_i), \mathfrak{s}(y_i))$ are composed of distinct elements in $\{a, b, c\}$.

By definition of the rules for predicate $p$, $(\mathfrak{s}, \mathfrak{h})$ is a model of $p(u_1, a, b, c)$ iff the list contains a pair $(\mathfrak{s}(x), \mathfrak{s}(y))$ such that one of the following holds:

* $\mathfrak{s}(x) = \mathfrak{s}(y)$ (first rule of $p$),

* $\mathfrak{s}(x) \neq \mathfrak{s}(y)$ and $\mathfrak{s}(x) \notin \{\mathfrak{s}(a), \mathfrak{s}(b), \mathfrak{s}(c)\}$ (second rule of $p$),

* $\mathfrak{s}(x) \in \{\mathfrak{s}(a), \mathfrak{s}(b), \mathfrak{s}(c)\}$ and $\mathfrak{s}(y) \notin \{\mathfrak{s}(a), \mathfrak{s}(b), \mathfrak{s}(c)\}$ (third rule of $p$).

After the cell corresponding to this faulty pair is allocated, $q$ is invoked to allocate the remaining part of the list. Thus $p(u_1, a, b, c)$ holds iff the model does not encode a solution of the 3-coloring problem, either because $\mathfrak{s}(x_i) = \mathfrak{s}(y_i)$ for some $(x_i, y_i) \in E$ or because one of the variables is mapped to an element distinct from $a, b, c$ – note that by the above assumption, each of these variables occurs in the list. Consequently $\mathfrak{h} \vdash \mathfrak{p}(u_1, a, b, c)$ admits a counter-model iff there exists a model of $\mathfrak{h}$ that does not satisfy $p(u_1, a, b, c)$, i.e., iff the 3-coloring problem admits a solution (thus the entailment is valid iff the 3-coloring problem admits no solution). $\square$

The results above motivate the following definition, that strengthens the notion of a deterministic set of rules.

**Definition 3.5.** A set of P-rules $\mathfrak{R}$ is loc-deterministic if it is deterministic and all the disequations occurring in the rules in $\mathfrak{R}$ are of the form $x \not\approx y$ with $x, y \in \mathcal{V}_{\text{loc}}$.

The intuition behind loc-deterministic rules is that, to get an efficient proof procedure, we have to restrict the amount of equational reasoning needed to establish the validity of the sequents. Disequations between locations are relatively easy to handle because (by definition of P-rules) all existential variables of sort loc must be pairwise distinct (as they are allocated in distinct atoms). However, dealing with disequations between data is much more difficult, as evidenced by the proof of Lemma 3.4. Thus we restrict such disequations to those occurring in the initial sequent.

The rules associated with `als`, `tree`, `tll`, `tptr` or `dll` in the introduction and in Example 2.8 are loc-deterministic. In contrast, the following rules are deterministic, but not loc-deterministic (where $u, v$ denote variables of some sort distinct from loc):

$$p(x, u) \leftarrow x \mapsto (v) \land v \not\approx u \qquad p(x, u) \leftarrow x \mapsto (u)$$

Rules that are loc-deterministic are well-suited to model constructor-based data structures used in standard programming languages; for instance, lists could be represented as follows (where `cons` is a constant symbol denoting a constructor and $y$ is a variable of some sort distinct from loc, denoting data stored in the list):

$$\mathit{ls}(x) \leftarrow x \mapsto (\mathit{cons}, y, z) * \mathit{ls}(z) \qquad \mathit{ls}(x) \leftarrow x \mapsto (\mathit{ })$$

We end this section by establishing a key property of deterministic set of rules, namely the fact that every spatial formula $\mathfrak{h}$ is *precise*, in the sense of [4]: it is fulfilled on at most one subheap within a given structure.
**Lemma 3.6.** Let $\mathfrak{R}$ be a deterministic set of rules. For every spatial formula $\phi$, for every store $s$ and for every heap $h$ there exists at most one heap $h'$ such that $h' \subseteq h$ and $(s, h') \models_{\mathfrak{R}} \phi$.

**Proof:**

The proof is by induction on the satisfiability relation $\models_{\mathfrak{R}}$. Note that by hypothesis $\phi$ is a spatial formula, hence contains no occurrences of $\approx$, $\not\approx$, $\wedge$ or $\wedge$. Assume that there exist two heaps $h'_1, h'_2$ such that $h'_i \subseteq h$ and $(s, h'_i) \models_{\mathfrak{R}} \phi$ (for $i = 1, 2$). We show that $h'_1 = h'_2$.

* If $\phi = \text{emp}$ then necessarily $h_i = \emptyset$ for $i = 1, 2$ thus $h'_1 = h'_2$.

* If $\phi = y_0 \mapsto (y_1, \dots, y_n)$ then by Definition 2.3 we have $h'_i = \{(s(y_0), \dots, s(y_n))\}$ for $i = 1, 2$ thus $h'_1 = h'_2$.

* If $\phi = \phi_1 * \phi_2$ then for all $i = 1, 2$ there exist two disjoint heaps $h_i^j$ (for $j = 1, 2$) such that $h'_i = h_i^1 \uplus h_i^2$ for $i = 1, 2$ and $(s, h_i^j) \models_{\mathfrak{R}} \phi_j$, for $i, j \in \{1, 2\}$. Since $h_i^j \subseteq h'_i \subseteq h$ we get by the induction hypothesis $h_1^j = h_2^j$ for $j = 1, 2$. Therefore $h_1^1 \uplus h_1^2 = h_2^1 \uplus h_2^2$, i.e., $h'_1 = h'_2$.

* If $\phi$ is a predicate atom of root $x$, then for $i = 1, 2$ we have $\phi \Leftarrow_{\mathfrak{R}} \lambda_i$, and there exists an associate $s_i$ of $s$ w.r.t. $V(\psi_i) \setminus V(\phi)$ such that $(s_i, h'_i) \models_{\mathfrak{R}} \lambda_i$. Since $\mathfrak{R}$ is a set of P-rules, $\lambda_i$ is of the form $(x_i \mapsto y_i * \phi_i) \wedge \xi_i$ and there exist disjoint heaps $h_i^j$ (for $j = 1, 2$) such that the following conditions are satisfied: (i) $h'_i = h_i^1 \uplus h_i^2$; (ii) $(s_i, h_i^1) \models_{\mathfrak{R}} x_i \mapsto (y_i)$; (iii) $(s_i, h_i^2) \models_{\mathfrak{R}} \phi_i$; (iv) and $s_i \models \xi_i$. Furthermore, $x_i$ must be the root of $\phi$, thus $x_1 = x_2 = x$. For $i = 1, 2$ we have $h_i^1 = \{(s(x_i), s_i(y_i))\}$, and since $h_i^1 \subseteq h$, necessarily $s_1(y_1) = s_2(y_2)$ and $h_1^1 = h_2^1$. The heap $h_i^2$ is the restriction of $h'_i$ to the locations distinct from $s(x)$. We distinguish two cases.

- Assume that the inductive rules applied on $\phi$ to respectively derive $\lambda_1$ and $\lambda_2$ are different. We may assume by $\alpha$-renaming that $(V(\lambda_1) \setminus V(\phi)) \cap (V(\lambda_2) \setminus V(\phi)) = \emptyset$, which entails that there exists a store $s'$ that coincides with $s_i$ on $V(\lambda_i)$ (since $s_1$ and $s_2$ coincide on the variables in $V(\phi)$). Then we have $s' \models y_1 \approx y_2$ (since $s_1(y_1) = s_2(y_2)$) and $s' \models \xi_i$ (since $s_i \models \xi_i$), which entails that the formula $y_1 \approx y_2 \wedge \xi_1 \wedge \xi_2$ is satisfiable, contradicting the fact that $\mathfrak{R}$ is deterministic.

- Assume that the same rule is used to derive both $\lambda_1$ and $\lambda_2$. We may assume in this case (again by $\alpha$-renaming) that the vector of variables occurring in $\lambda_1$ and $\lambda_2$ are the same, so that $y_1 = y_2$ and $\phi_1 = \phi_2$. Since $\mathfrak{R}$ is a set of P-rules, all variables $z$ in $V(\phi_i) \setminus V(\phi)$ occur in $y_i$. As $s_1(y_1) = s_2(y_2)$, this entails that $s_1(z) = s_2(z)$ holds for all such variables, thus $s_1 = s_2$. Consequently, $(s_1, h_i^2) \models_{\mathfrak{R}} \phi_1$, for all $i = 1, 2$ with $h_i^2 \subseteq h'_i \subseteq h$. By the induction hypothesis this entails that $h_1^2 = h_2^2$, thus $h'_1 = h'_2$.

□

**Example 3.7.** Lemma 3.6 does not hold if the rules are not deterministic. For instance, the formula $\text{ls}(x, y)$ (with the rules given in the introduction) has two models $(s, h)$ and $(s, h')$ where $h'$ is a strict subheap of $h$: $s(x) = \ell_1$, $s(y) = \ell_2$, $h = \{\ell_1 \mapsto (\ell_2), \ell_2 \mapsto (\ell_2)\}$ and $h' = \{\ell_1 \mapsto (\ell_2)\}$. Intuitively, the formula $\text{ls}(y, y)$ (which is useful to derive $\text{ls}(x, y)$) can be derived by any of the two rules of $\text{ls}$, yielding two different models. In contrast $\text{als}(x, y)$ (with the rules of Example 2.8) has only one model with the store $s$ and a heap included in $h$, namely $(s, h')$.
# 4. Proof Procedure

From now on, we consider a fixed loc-deterministic set of P-rules $\mathfrak{R}$, satisfying Assumptions 2.12 and 2.15. For technical convenience, we also assume that $\mathfrak{R}$ is nonempty and that every constant in $C$ occurs in a rule in $\mathfrak{R}$.

## 4.1. Some Basic Properties of P-Rules

We begin by introducing some definitions and deriving straightforward consequences of the definition of P-rules. We shall denote by $alloc(\lambda)$ the multiset of variables allocated by a formula $\lambda$:

**Definition 4.1.** For every formula $\lambda$, we denote by $alloc(\lambda)$ the multiset of variables $x$ such that $\lambda$ contains a spatial atom with root $x$.

Lemma 4.2 states that the variables in $alloc(\lambda)$ are necessarily allocated in every model of $\lambda$, which entails (Corollary 4.3) that they must be associated with pairwise distinct locations. Moreover, a formula distinct from *emp* has at least one root, hence allocates at least one variable (Corollary 4.4).

**Lemma 4.2.** Let $\lambda$ be a formula. If $(s, h) \models_{\mathfrak{R}} \lambda$ and $x \in alloc(\lambda)$ then $s(x) \in dom(h)$.

**Proof:**

By hypothesis, $\lambda$ is of the form $(\alpha * \phi) \wedge \xi$ where $\alpha$ is a spatial atom with root $x$. Thus $(s, h) \models_{\mathfrak{R}} \alpha * \phi$ and there exist disjoint heaps $h_1, h_2$ such that $(s, h_1) \models_{\mathfrak{R}} \alpha$, $(s, h_2) \models_{\mathfrak{R}} \phi$, and $h = h_1 \uplus h_2$. Since the root of $\alpha$ is $x$, $\alpha$ is either of the form $x \mapsto y$ or of the form $p(x, y)$ where $p \in \mathcal{P}$. In the former case, it is clear that $s(x) \in dom(h_1) \subseteq dom(h)$ since $(s, h_1) \models_{\mathfrak{R}} \alpha$. In the latter case, we have $\alpha \Leftarrow_{\mathfrak{R}} \lambda'$ and $(s', h) \models_{\mathfrak{R}} \lambda'$, where $s'$ is an associate of $s$ w.r.t. $\mathcal{V}(\lambda') \setminus \mathcal{V}(\alpha)$. Since $\mathfrak{R}$ is a set of P-rules, necessarily $\lambda'$ contains a points-to atom of the form $x \mapsto z$, which entails that $s'(x) \in dom(h_1)$, hence $s(x) \in dom(h)$. $\square$

**Corollary 4.3.** Let $\lambda$ be a formula and let $(s, h)$ be an $\mathfrak{R}$-model of $\lambda$. If $\{x, y\} \subseteq_m alloc(\lambda)$ then $s(x) \neq s(y)$. In particular, if $alloc(\lambda)$ contains two occurrences of the same variable $x$ then $\lambda$ is unsatisfiable.

**Proof:**

By definition, $\lambda$ is of the form $(\alpha_1 * \alpha_2 * \phi) \wedge \xi$, where $\alpha_1$ and $\alpha_2$ are spatial atoms of roots $x$ and $y$, respectively, with $alloc(\alpha_1) = \{x\}$ and $alloc(\alpha_2) = \{y\}$. If $\lambda$ admits a model $(s, h)$, then there exists disjoint heaps $h_1, h_2, h'$ such that $h = h_1 \uplus h_2 \uplus h'$, $(s, h_i) \models_{\mathfrak{R}} \alpha_i$ (for $i = 1, 2$) and $(s, h') \models_{\mathfrak{R}} \phi$. By Lemma 4.2 we have $s(x) \in dom(h_1)$ and $s(y) \in dom(h_2)$, thus $s(x) \neq s(y)$ since $h_1$ and $h_2$ are disjoint. $\square$

**Corollary 4.4.** Let $\phi$ be a spatial formula and let $(s, h)$ be an $\mathfrak{R}$-model of $\phi$. If $\phi \neq emp$ then $h \neq \emptyset$.

**Proof:**

Since $\phi \neq emp$, necessarily $\phi$ contains at least one atom $\alpha$, thus $\mathrm{root}(\alpha) \in alloc(\phi)$. Then the result follows immediately from Lemma 4.2. $\square$
Corollary 4.3 motivates the following definition, which provides a simple syntactic criterion to identify some formulas that cannot be satisfiable, due to the fact that the same variable is allocated twice.

**Definition 4.5.** A formula $\lambda$ is heap-unsatisfiable if $alloc(\lambda)$ contains two occurrences of the same variable. Otherwise, it is heap-satisfiable.

The next proposition states that every location that is referred to in the heap of some model of $\lambda$ must be reachable from one of the roots of $\lambda$. This follows from the fact that, by definition of P-rules, the set of allocated locations has a tree-shaped structure: the root of each atom invoked in an inductive rule must be connected to the location allocated by the rule (see Condition 2 in Definition 2.7).

**Proposition 4.6.** Let $\lambda$ be a symbolic heap and let $(s, h)$ be an $\mathfrak{R}$-model of $\lambda$. For every $\ell \in \text{ref}(h)$, there exists $x \in \text{alloc}(\lambda)$ such that $s(x) \xrightarrow{h}^* \ell$.

**Proof:**

The proof is by induction on the satisfiability relation. We establish the result also for spatial formulas and pure formulas.

* If $\lambda = \text{emp}$ or is $\lambda$ is a pure formula then $\text{ref}(\lambda) = \emptyset$ hence the proof is immediate.

* If $\lambda = y_0 \mapsto (y_1, \dots, y_n)$, then $h = \{(s(y_0), \dots, s(y_n))\}$, by Definition 2.3, thus $\text{ref}(h) = \{s(y_i) \mid i = 0, \dots, n, \text{ and } y_i \text{ is of sort loc}\}$ and $s(y_0) \xrightarrow{h} s(y_i)$, for all $i = 1, \dots, n$ such that $y_i$ is of sort loc. By Definition 4.1 $\text{alloc}(\lambda) = \{y_0\}$, thus the proof is completed.

* If $\lambda = \phi \lambda \xi$, where $\phi$ is a spatial formula and $\xi$ is a pure formula distinct from $\top$, then we have $(s, h) \models_{\mathfrak{R}} \phi$ and $\text{alloc}(\lambda) = \text{alloc}(\phi)$, hence the result follows immediately from the induction hypothesis.

* If $\lambda = \phi_1 * \phi_2$, then there exist two disjoint heaps $h_1, h_2$ such that $h = h_1 \uplus h_2$ and $(s, h_i) \models_{\mathfrak{R}} \phi_i$, for all $i = 1, 2$. If $\ell \in \text{ref}(h)$ then necessarily $\ell \in \text{ref}(h_i)$ for some $i = 1, 2$. By the induction hypothesis, we deduce that there exists $x \in \text{alloc}(\phi_i)$ such that $s(x) \xrightarrow{h_i}^* \ell$. Since $\text{alloc}(\phi_i) \subseteq_m \text{alloc}(\phi)$ and $\xrightarrow{h_i}^* \subseteq \xrightarrow{h}^*$ by Proposition 2.1, we obtain the result.

* If $\lambda$ is a predicate atom, then $\lambda \Leftarrow_{\mathfrak{R}} \gamma$ and $(s', h) \models_{\mathfrak{R}} \gamma$ for some formula $\gamma$ and some associate $s'$ of $s$ w.r.t. $\mathcal{V}(\gamma) \setminus \mathcal{V}(\lambda)$. Let $\ell \in \text{ref}(h)$. By the induction hypothesis, there exists $x \in \text{alloc}(\gamma)$ such that $s(x) \xrightarrow{h}^* \ell$. By definition, $x$ is the root of some atom $\alpha$ in $\gamma$. If $\alpha$ is a points-to atom, then since $\lambda \Leftarrow_{\mathfrak{R}} \gamma$ is an instance of a rule in $\mathfrak{R}$ and all rules are P-rules, $x$ must be the root of $\lambda$; in this case $x \in \text{alloc}(\lambda)$ and the proof is completed. Otherwise, $x$ is the root of a spatial atom in $\gamma$, and, because all rules are P-rules, $\gamma$ must contain an atom of the form $y_0 \mapsto (y_1, \dots, y_n)$, such that $y_0 = \text{root}(\lambda)$ and $y_i = x$, for some $i = 1, \dots, n$. Since $(s', h) \models_{\mathfrak{R}} \gamma$, we have $(s(y_0), \dots, s(y_n)) \in h$, hence $s(y_0) \xrightarrow{h} s(x)$. Using the fact that $s(x) \xrightarrow{h}^* \ell$, we deduce that $s(y_0) \xrightarrow{h}^* \ell$, hence the proof is completed since $\text{alloc}(\lambda) = \{y_0\}$.

□
The next lemma asserts a key property of the considered formulas: all the locations occurring in the heap of a model of some formula $\phi$ are either allocated or associated with a variable that is free in $\phi$. This follows from the definition of P-rules: all variables of sort $\text{loc}$ that are existentially quantified in an inductive rule must be allocated (at the next recursive call). Recall that spatial formulas contain no quantifiers.

**Lemma 4.7.** Let $\phi$ be a spatial formula and let $(s, h)$ be an $\mathfrak{R}$-model of $\phi$. Then the following inclusion holds: $\text{ref}(h) \subseteq \text{dom}(h) \cup s(\mathcal{V}(\phi))$.

**Proof:**

The proof is by induction on the relation $\models\mathfrak{R}$. Note that as $\phi$ is spatial, it contains no occurrence of $\approx$, $\not\approx$, $\wedge$ and $\wedge$.

* If $\phi$ is of the form $y_0 \mapsto (y_1, \dots, y_n)$ then by definition $h = \{(s(y_0), \dots, s(y_n))\}$ and $\text{ref}(h) = \{s(y_0), \dots, s(y_n)\} = s(\mathcal{V}(\phi))$.

* If $\phi = \text{emp}$ then $h = \emptyset$ thus $\text{ref}(h) = \emptyset$ and the proof is immediate.

* If $\phi$ is a predicate atom then we have $\phi \Leftarrow \mathfrak{R} \psi \wedge \xi$, and $(s', h) \models\mathfrak{R} \psi$, for some associate $s'$ of $s$ w.r.t. $\mathcal{V}(\psi \wedge \xi) \setminus \mathcal{V}(\phi)$. Let $\ell \in \text{ref}(h) \setminus \text{dom}(h)$. By the induction hypothesis, $\ell = s'(x)$ for some variable $x \in \mathcal{V}(\psi)$. If $x \in \mathcal{V}(\phi)$ then necessarily $s'(x) = s(x)$, thus $\ell \in s(\mathcal{V}(\phi))$ and the proof is completed. Otherwise, by Definition 2.7, since all the rules in $\mathfrak{R}$ are P-rules; $x$ occurs as the root of some predicate atom in $\psi$, i.e., $x \in \text{alloc}(\psi)$. By Lemma 4.2 we deduce that $s'(x) \in \text{dom}(h)$, i.e., $\ell \in \text{dom}(h)$ which contradicts our assumption.

* If $\phi$ is of the form $\phi_1 * \phi_2$ then there exist disjoint heaps $h_1, h_2$ such that $(s, h_i) \models\mathfrak{R} \phi_i$ (for $i = 1, 2$) and $h = h_1 \uplus h_2$. Let $\ell \in \text{ref}(h) \setminus \text{dom}(h)$. Necessarily we have $\ell \in \text{ref}(h_i)$, for some $i = 1, 2$ and $\ell \notin \text{dom}(h_i)$, hence by the induction hypothesis we deduce that $\ell = s(x)$, for some $x \in \mathcal{V}(\phi_i)$. Since $\mathcal{V}(\phi_i) \subseteq \mathcal{V}(\phi)$, the proof is completed.

□

## 4.2. A Restricted Entailment Relation

We introduce a simple syntactic criterion, used in the inference rules of Section 4.3, that is sufficient to ensure that a given pure formula $\xi$ holds in every counter-model of a sequent with left-hand side $\lambda$ and multiset of variables $V$. The idea is to test that $\xi$ either occurs in $\lambda$, is trivial, or is a disequation entailed by the fact that the considered store must be injective on $\text{alloc}(\lambda) \cup V$ (using Definition 2.17 and Corollary 4.3). Lemma 4.10 states that the relation satisfies the expected property.

**Definition 4.8.** Let $\lambda$ be a symbolic heap, $\xi$ be a pure formula and let $V$ be a multiset of variables. We write $\lambda \triangleright_V \xi$ if for every atom $\zeta$ occurring in $\xi$, one of the following conditions holds:

1. $\zeta$ occurs in $\lambda$;

2. either $\zeta = (t \approx t)$ for some variable $t$, or $\zeta = (t_1 \not\approx t_2)$ and $t_1, t_2$ are distinct constants;
3. $\zeta = (x_1 \not\approx x_2)$ modulo commutativity, and one of the following holds: $\{x_1, x_2\} \subseteq_m \text{alloc}(\lambda)$, $(x_1 \in \text{alloc}(\lambda)$ and $x_2 \in V)$ or $\{x_1, x_2\} \subseteq_m V$. This is equivalent to stating that $\{x_1, x_2\} \subseteq_m \text{alloc}(\lambda) + V$ where $\text{alloc}(\lambda) + V$ denotes as usual the union of the multisets $\text{alloc}(\lambda)$ and $V$.

**Example 4.9.** Consider the symbolic heap $\lambda = (p(x, y) * q(z)) \wedge x \not\approx y$, and let $V = \{u\}$. We have $\lambda \triangleright_V x \not\approx y \wedge x \not\approx z \wedge x \not\approx u$. Indeed, $x$ and $z$ are necessarily distinct since they are allocated by distinct atoms $p(x, y)$ and $q(z)$ (as, by definition of the P-rules, every predicate allocates it first parameter) $x$ cannot be equal to $u$ as $u \in V$ and $V$ is intended to denote a set of non-allocated variables (see Definition 2.17) and $x$ is allocated, and $x$ cannot be equal to $y$ as the disequation $x \not\approx y$ occurs in $\lambda$.

**Lemma 4.10.** Let $\lambda$ be a symbolic heap and let $\xi$ be a pure formula such that $\lambda \triangleright_V \xi$. For every structure $(\mathfrak{s}, \mathfrak{h})$, if $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \lambda$, $\mathfrak{s}(V) \cap \text{dom}(\mathfrak{h}) = \emptyset$ and $\mathfrak{s}$ is injective on $V$ then $\mathfrak{s} \models_{\mathfrak{R}} \xi$.

**Proof:**

We show that $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \zeta$, for all atoms $\zeta$ in $\xi$. We consider each case in Definition 4.8 separately:

1. If $\zeta$ occurs in $\lambda$ then since $(\mathfrak{s}, \mathfrak{h}) \models \gamma$, necessarily $\mathfrak{s} \models_{\mathfrak{R}} \zeta$.

2. If $\zeta = (t \approx t)$ then it is clear that $\mathfrak{s} \models \zeta$. If $\zeta = (t_1 \not\approx t_2)$ and $t_1, t_2$ are distinct constants then $\mathfrak{s}(t_1) \neq \mathfrak{s}(t_2)$ since all stores are injective on constants by definition.

3. If $\zeta = x_1 \not\approx x_2$ and $\{x_1, x_2\} \subseteq_m \text{alloc}(\lambda)$ then by Corollary 4.3, we get $\mathfrak{s}(x_1) \neq \mathfrak{s}(x_2)$ since $\mathfrak{s}(x_1)$ and $\mathfrak{s}(x_2)$ must be allocated in disjoint heaps. Thus $\mathfrak{s} \models_{\mathfrak{R}} \zeta$. If $x_1 \in \text{alloc}(\phi)$ and $x_2 \in V$ then we have $\mathfrak{s}(x_1) \in \text{dom}(\mathfrak{h})$ by Lemma 4.2, and since $\mathfrak{s}(V) \cap \text{dom}(\mathfrak{h}) = \emptyset$, we deduce that $\mathfrak{s} \models_{\mathfrak{R}} \zeta$. Finally, if $\{x_1, x_2\} \subseteq_m V$ then $\mathfrak{s}(x_1) \neq \mathfrak{s}(x_2)$, because $\mathfrak{s}$ is injective on $V$ by hypothesis.

□

## 4.3. Inference Rules

We consider the rules represented in Figure 3. The rules apply modulo AC, they are intended to be applied bottom-up: a rule is *applicable* on a sequent $\lambda \vdash_V \gamma$ if there exists an instance of the rule the conclusion of which is $\lambda \vdash_{\mathfrak{R}} \gamma$. We recall that an inference rule is *sound* if the validity of the premises entails the validity of the conclusion, and *invertible* if the converse holds.

**Remark 4.11.** The application conditions given in Figure 3 are the most general ones ensuring that the rules are sound. Additional application conditions will be provided afterwards (see Definition 4.31) to obtain a proof procedure that runs in polynomial time. The latter conditions are rather complex, and in our opinion introducing them at this point could hinder the understanding of the rules.

We provide some examples and explanations concerning the inference rules.

**Example 4.12.** Rules R (replacement) and E (elimination) handle equational reasoning. For instance, given the sequent $(p(x, u) * p(y, u)) \wedge (u \approx v) \vdash_{\mathfrak{R}} (p(x, u) * p(y, v)) \wedge (x \not\approx y)$, one may first apply R, yielding: $p(x, u) * p(y, u) \vdash_{\mathfrak{R}} (p(x, u) * p(y, u)) \wedge (x \not\approx y)$. As $\{x, y\} \subseteq_m \text{alloc}(p(x, u) * p(y, u))$, E applies, which yields the trivially valid sequent $p(x, u) * p(y, u) \vdash_{\mathfrak{R}} p(x, u) * p(y, u)$.
$$
\text{R: } \frac{\phi\{x \leftarrow t\} \wedge \xi\{x \leftarrow t\} \vdash_{\mathfrak{R}}^{V\{x \leftarrow t\}} \gamma\{x \leftarrow t\}}{\phi \wedge (x \approx t \wedge \xi) \vdash_{\mathfrak{R}}^{V} \gamma} \quad \text{if } x \in \mathcal{V}
$$

$$
E: \frac{\lambda \vdash_{\mathfrak{R}}^{V} \psi \wedge \zeta}{\lambda \vdash_{\mathfrak{R}}^{V} \psi \wedge (\zeta \wedge \zeta')} \quad \text{if } \lambda \triangleright V \zeta'
$$

$$
S: \frac{\phi_1 \wedge \xi_1 \vdash_{\mathfrak{R}}^{V \cup \text{alloc}(\phi_2)} \psi_1 \wedge \zeta_1 \qquad \phi_2 \wedge \xi_2 \vdash_{\mathfrak{R}}^{V \cup \text{alloc}(\phi_1)} \psi_2 \wedge \zeta_2}{(\phi_1 * \phi_2) \wedge (\xi_1 \wedge \xi_2) \vdash_{\mathfrak{R}}^{V} (\psi_1 * \psi_2) \wedge (\zeta_1 \wedge \zeta_2)} \quad \text{if } \phi_1 \neq \text{emp} \text{ and } \phi_2 \neq \text{emp}
$$

$$
U: \frac{(\phi'_1 * \phi) \wedge (\xi'_1 \wedge \xi) \vdash_{\mathfrak{R}}^{V} \gamma \quad \dots \quad (\phi'_n * \phi) \wedge (\xi'_n \wedge \xi) \vdash_{\mathfrak{R}}^{V} \gamma}{(p(\mathbf{t}) * \phi) \wedge \xi \vdash_{\mathfrak{R}}^{V} \gamma} \quad \text{if } p(\mathbf{t}) \rightsquigarrow_{\mathfrak{R}} \{\phi'_i \wedge \xi'_i \mid i = 1, \dots, n\}
$$

$$
I: \frac{(x \mapsto (y_1, \dots, y_k) * \phi) \wedge \xi \vdash_{\mathfrak{R}}^{V} (x \mapsto (y_1, \dots, y_k) * \psi' \sigma * \psi) \wedge \zeta}{(x \mapsto (y_1, \dots, y_k) * \phi) \wedge \xi \vdash_{\mathfrak{R}}^{V} (p(x, z) * \psi) \wedge \zeta} \quad \text{if all the conditions below hold}
$$

(i) $p(x, z) \Leftarrow_{\mathfrak{R}} (x \mapsto (u_1, \dots, u_k) * \psi') \wedge \zeta'$; (ii) $\sigma$ is a substitution whose domain is included in $\{u_1, \dots, u_k\} \setminus (\{x\} \cup z)$; (iii) $\sigma(u_i) = y_i$, for all $i \in \{1, \dots, k\}$; and (iv) $(x \mapsto (y_1, \dots, y_k) * \phi) \wedge \xi \triangleright_V \zeta' \sigma$

$$
W: \frac{\phi \wedge \xi \vdash_{\mathfrak{R}}^{V} \gamma}{\phi \wedge (\xi \wedge \xi') \vdash_{\mathfrak{R}}^{V} \gamma} \quad \text{if one of the conditions below holds:}
$$

$$
(i) \xi' = x \not\approx y \text{ and } \phi \triangleright_V x \not\approx y; \text{ or (ii) } \xi' = \bigwedge_{i=1}^n x \not\approx y_i \text{ and } x \notin \mathcal{V}(\phi) \cup \mathcal{V}(\xi) \cup \mathcal{V}(\gamma) \cup \{y_1, \dots, y_n\}
$$

$$
C: \frac{\phi\{x \leftarrow y\} \wedge \xi\{x \leftarrow y\} \vdash_{\mathfrak{R}}^{V\{x \leftarrow y\}} \gamma\{x \leftarrow y\} \qquad \phi \wedge (\xi \wedge x \not\approx y) \vdash_{\mathfrak{R}}^{V} \gamma}{\phi \wedge \xi \vdash_{\mathfrak{R}}^{V} \gamma} \quad \text{if } x, y \in \mathcal{V}_{\text{loc}}
$$

$$
V: \frac{\lambda \vdash_{\mathfrak{R}}^{V} \gamma}{\lambda \vdash_{\mathfrak{R}}^{V \cup \{x\}} \gamma} \quad \text{if } x \notin \mathcal{V}(\lambda) \cup \mathcal{V}(\gamma)
$$

<caption>Figure 3. The Inference rules</caption>
**Example 4.13.** Rule S (separation) applies on the sequent $p(x) * p(y) \vdash_{\mathfrak{R}}^0 q(x) * r(y)$, yielding $p(x) \vdash_{\mathfrak{R}}^{\{y\}} q(x)$ and $p(y) \vdash_{\mathfrak{R}}^{\{x\}} r(y)$ (as $\{x\} = \text{alloc}(p(x))$ and $\{y\} = \text{alloc}(p(y))$). The addition of $y$ (resp. $x$) to the variables associated with the sequent allows us to keep track of the fact that these variables cannot be allocated in $p(x)$ (resp. $p(y)$) as they are already allocated in the other part of the heap. Note that the rule also yields $p(x) \vdash_{\mathfrak{R}}^{\{y\}} r(y)$ and $p(y) \vdash_{\mathfrak{R}}^{\{x\}} q(x)$, however as we shall see later (see Definition 4.24) the latter premises cannot be valid and this application can be dismissed.

**Example 4.14.** Rules U (unfolding) and I (imitation) both unfold inductively defined predicate symbols. U unfolds predicates occurring on the left-hand side of a sequent, yielding one premise for each inductive rule. In contrast, I applies on the right-hand side and selects one rule in a non-deterministic way (provided it fulfills the rule application condition), yielding exactly one premise. Let $\mathfrak{R}$ be the following set of rules, where a, b are constant symbols and $z, z_1, z_2$ are variables of the same sort as a and b:

$$ 
\begin{array}{lcl}
p(x) & \Leftarrow & x \mapsto (a, x) \\
p(x) & \Leftarrow & x \mapsto (b, x) \\
q(x) & \Leftarrow & x \mapsto (z, y) \\
q(x) & \Leftarrow & x \mapsto (z_1, z_2, x)
\end{array}
$$

Rule U applies on $p(x, y) \vdash_{\mathfrak{R}}^0 q(x)$, yielding $x \mapsto (a, x) \vdash_{\mathfrak{R}}^0 q(x)$ and $x \mapsto (b, x) \vdash_{\mathfrak{R}}^0 q(x)$. Then I applies on both sequents, with the respective substitutions $\{y \leftarrow x, z \leftarrow a\}$ and $\{y \leftarrow x, z \leftarrow b\}$, yielding $x \mapsto (a, x) \vdash_{\mathfrak{R}}^0 x \mapsto (a, x)$ and $x \mapsto (b, x) \vdash_{\mathfrak{R}}^0 x \mapsto (b, x)$. Note that I cannot be applied with the inductive rule $q(x) \Leftarrow x \mapsto (z_1, z_2, x)$, as $(a, x)$ and $(b, x)$ are not instances of $(z_1, z_2, x)$.

**Example 4.15.** Rules W (weakening) and V (variable weakening) allow to get rid of irrelevant information, which is essential for termination. For instance one may deduce $p(x) \vdash_{\mathfrak{R}}^0 q(x)$ from $p(x) \wedge (u \not\approx v \wedge u \not\approx w) \vdash_{\mathfrak{R}}^0 q(x)$. Indeed, if the former sequent admits a counter-model, then one gets a counter-model of the latter one by associating $u, v, w$ with pairwise distinct elements.

**Example 4.16.** Rule C performs a case analysis on $x \approx y$. It is essential to allow further applications of Rule I in some cases. Consider the sequent $u \mapsto (x, x) * p(x) \vdash_{\mathfrak{R}}^0 q(u, y)$, with the rules $q(u, y) \Leftarrow u \mapsto (y, z) * p(z)$, and $q(u, y) \Leftarrow (u \mapsto (z, z) * p(z)) \wedge z \not\approx y$. Rule I does not apply because there is no substitution $\sigma$ with domain $\{z\}$ such that $(x, x) = (y, z)\sigma$, and $u \mapsto (x, x) * p(x) \not\vdash_V x \not\approx y$. The rule C yields $u \mapsto (y, y) * p(y) \vdash_{\mathfrak{R}}^0 q(u, y)$ and $(u \mapsto (x, x) * p(x)) \wedge x \not\approx y \vdash_{\mathfrak{R}}^0 q(u, y)$. Then the rule I applies on both sequents, yielding the premises $u \mapsto (y, y) * p(y) \vdash_{\mathfrak{R}}^0 u \mapsto (y, y) * p(y)$ and $(u \mapsto (x, x) * p(x)) \wedge x \not\approx y \vdash_{\mathfrak{R}}^0 u \mapsto (x, x) * p(x)$.

We have the following facts, which can be verified by an inspection of the inference rules:

**Proposition 4.17.** Consider an equality-free sequent $\lambda \vdash_{\mathfrak{R}}^V \gamma$ that is the conclusion of an inference rule, of which $\lambda' \vdash_{\mathfrak{R}}^{V'} \gamma'$ is a premise.

1. No rule can introduce any equality to $\lambda' \vdash_{\mathfrak{R}}^{V'} \gamma'$.

2. If $x \in V' \setminus V$, then the inference rule is either V or C.
3. If $alloc(\gamma') \subsetneq alloc(\gamma)$ then the inference rule is either S or C.

4. The only inference rules that can introduce new variables to $\gamma'$ are I and C.

5. No rule introduces a disequation between terms of a sort distinct from loc.

6. The only rule that introduces a predicate atom to the right-hand side of a premise is I.

7. If $v \in (alloc(\gamma) \cup V) \setminus (alloc(\gamma') \cup V')$, then the inference rule must be C.

**Proof:**

The first six facts are straightforward to verify. Fact 7 holds because Rule R cannot apply if no equality occurs; if rule S is applied then the variables in $alloc(\gamma) \setminus alloc(\gamma')$ must occur in $V'$; Rule I deletes a predicate atom but introduces a points-to atom with the same root and rule V cannot be applied on variables occurring in $V\gamma$. $\square$

We establish additional basic properties of the inference rules. All the rules are sound and invertible, except for rule S that is only sound. The results follow easily from the semantics, except for the invertibility of I, which crucially depends on the fact that rules are deterministic. Indeed, I unfolds one atom on the right-hand side by selecting one specific inductive rule. In our case, at most one rule can be applied, which ensures that equivalence is preserved. This is a crucial point because otherwise one would need to consider disjunctions of formulas on the right-hand side of the sequent (one disjunct for each possible rule), which would make the procedure much less efficient.

**Example 4.18.** Consider the sequent $x \mapsto (y) * y \mapsto (z) \vdash_{\mathfrak{R}}^{\emptyset} p(x, z)$, with the rules

$$ \begin{array}{lclcl} p(x, z) & \Leftarrow & x \mapsto (y) * q(y, z) & p(x, z) & \Leftarrow & x \mapsto (y) * q'(y, y) \\ q(y, z) & \Leftarrow & y \mapsto (z) \wedge y \not\approx z & q'(y, z) & \Leftarrow & y \mapsto (z) \end{array} $$

It is clear that the rules are not deterministic, as there is an overlap between the two rules associated with $p$. Applying rule I on the above sequent yields either $x \mapsto (y) * y \mapsto (z) \vdash_{\mathfrak{R}}^{\emptyset} x \mapsto (y) * q(y, z)$ or $x \mapsto (y) * y \mapsto (z) \vdash_{\mathfrak{R}}^{\emptyset} x \mapsto (y) * q'(y, y)$. None of these two possible premises is valid, although the initial sequent is valid. This shows that I is not invertible (although it is still sound) when $\mathfrak{R}$ is not deterministic. The intuition is that it is not possible to decide which rule must be applied on $p$ before deciding whether $z$ is equal to $y$ or not.

**Lemma 4.19.** The rules R, E, U, W, V and C and I are sound and invertible. More specifically, for all heaps $h$, the conclusion of the rule admits a counter-model ($\mathfrak{s}, h$) iff one of the premises admits a counter-model ($\mathfrak{s}', h$).

**Proof:**

We consider each rule separately (we refer to the definitions of the rules for notations) and establish the equivalence of the lemma. We recall (Definition 2.17) that a counter-model of a sequent is a structure $(\mathfrak{s}, h)$ that validates the antecedent, falsifies the conclusion, and is such that the store is injective on $V$ and no variable in $V$ is allocated.
(s, h₂) |=ₘ ψ'σ, hence (s, h₁ ⊔ h₂) |=ₘ λσ. By Proposition 2.6, we get (s', h₁ ⊔ h₂) |=ₘ λ. Since p(x, z) ←ₘ λ, we deduce that (s, h₁ ⊔ h₂) |=ₘ p(x, z), hence (s, h) |=ₘ p(x, z) * ψ. Thus (s, h) |=ₘ (p(x, z) * ψ) ∧ ζ, which contradicts our hypothesis.

Conversely, assume that (x ↦ (y₁, ..., yₖ) * φ) ∧ ξ ⊢ₘ^V (p(x, z) * ψ) ∧ ζ is valid, and let (s, h) be an ℜ-model of (x ↦ (y₁, ..., yₖ) * φ) ∧ ξ such that s(V) ∩ dom(h) = ∅ and s is injective on V. We deduce that (s, h) |=ₘ (p(x, z) * ψ) ∧ ζ, thus s |= ζ, and there exist disjoint heaps h₁, h₂ such that (s, h₁) |=ₘ (p(x, z) and (s, h₂) |=ₘ ψ. This entails that there exists a symbolic heap λ and a associate s' of s w.r.t. V(λ) \ V(p(x, z)) such that p(x, z) ←ₘ λ, and (s', h₁) |=ₘ λ. Since the rules in ℜ are P-rules, λ is of the form (x ↦ (v₁, ..., v_m) * ψ'') ∧ ζ''. Moreover, it is clear that h(s(x)) = (s(y₁), ..., s(yₖ)), so that m = k and s'(vᵢ) = s(yᵢ), for all i = 1, ..., k. Let σ' be the substitution mapping every variable in {v₁, ..., vₖ} not occurring in x, z to the first variable yⱼ such that s'(vᵢ) = s(yⱼ). By definition, we have s' = s ○ σ', thus by Proposition 2.6, we get (s, h₁) |=ₘ λσ'.

Assume for the sake of contradiction that the inductive rule used to derive λ is distinct from the one used to derive the formula λ' = (x ↦ (u₁, ..., uₖ) * ψ') ∧ ζ' in the application condition of the rule. We may assume by renaming that V(λ') ∩ V(λ) ⊆ V(p(x, z)). Let s'' be a store coinciding with s' on all constants and on all variables in V(λ), and such that, for all variables y ∈ V(λ') \ V(p(x, z)), s''(y) = s(σ(y)). Since s' |= ζ'' we have s'' |= ζ''. By the application condition of the rule σ(uᵢ) = yᵢ, thus s'' |= uᵢ ≈ yᵢ, for all i = 1, ..., k. Since s |= ξ and ξ |= ζ'σ (still by the application condition of the rule), we get s |= ζ'σ, and by Proposition 2.6 we deduce that s |= ζ'. Thus (u₁, ..., uₖ) ≈ (v₁, ..., vₖ) ∧ ζ' ∧ ζ'' is satisfiable, which contradicts the fact that ℜ is deterministic.

This entails that the rules applied to derive λ and λ' are the same, and by renaming we may assume in this case that (u₁, ..., uₖ) = (v₁, ..., vₖ) (which entails that (x ↦ (v₁, ..., vₖ))σ = x ↦ (y₁, ..., yₖ)), with ψ' = ψ'' and ζ' = ζ''. Using the fact that σ(uᵢ) = yᵢ and s'(vᵢ) = s(yᵢ), for all i = 1, ..., k, it is easy to check that s'(y) = s(σ(y)), for all variables y. Since (s', h₂) |=ₘ λ we get by Proposition 2.6, (s, h₂) |=ₘ λσ, i.e., (s, h₂) |=ₘ (x ↦ (y₁, ..., yₖ) * ψ'σ). Therefore (s, h) |=ₘ (x ↦ (y₁, ..., yₖ) * ψ'σ * ψ) ∧ ζ.

□

Rule S is sound but in contrast with the other rules, it is not invertible in general (intuitively, there is no guarantee that the decomposition of the left-hand side of the sequent corresponds to that of the right-hand side).

**Example 4.20.** Consider the (valid) sequent $x \mapsto (y) * y \mapsto (x) \vdash_{\mathfrak{M}}^0 p(x, y) * p(y, x)$ with the rule $p(u, v) \Leftarrow u \mapsto (v)$. Rule S applies, yielding the valid premises $x \mapsto (y) \vdash_{\mathfrak{M}}^0 p(x, y)$ and $y \mapsto (x) \vdash_{\mathfrak{M}}^0 p(y, x)$. However, since the rules apply modulo commutativity of * we may also get the premises: $x \mapsto (y) \vdash_{\mathfrak{M}}^0 p(y, x)$ and $y \mapsto (x) \vdash_{\mathfrak{M}}^0 p(x, y)$ which are not valid.

**Lemma 4.21.** Rule S is sound. More specifically, if (s, h) is a counter-model of the conclusion, then one of the premises admits a counter-model (s, h'), where h' is a proper subheap of h.
**Proof:**

Let $(\mathfrak{s}, \mathfrak{h})$ be an $\mathfrak{R}$-model of $(\phi_1 * \phi_2) \wedge (\xi_1 \wedge \xi_2)$, where $\mathfrak{s}(V) \cap \text{dom}(\mathfrak{h}) = \emptyset$ and $\mathfrak{s}$ is injective on $V$. Assume that the premises admit no counter-model of the form $(\mathfrak{s}, \mathfrak{h}')$ with $\mathfrak{h}' \subset \mathfrak{h}$. By definition, there exist disjoint heaps $\mathfrak{h}_1, \mathfrak{h}_2$ such that $\mathfrak{h} = \mathfrak{h}_1 \uplus \mathfrak{h}_2$, and $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \phi_i$, for $i = 1, 2$. Since $\phi_i \neq \text{emp}$, $\phi_i$ contains at least one predicate atom, with a root $x_i$. By Lemma 4.2, necessarily $\mathfrak{s}(x_i) \in \text{dom}(\mathfrak{h}_i)$, so $\mathfrak{h}_i$ is not empty and $\mathfrak{h}_i \subset \mathfrak{h}$ for $i = 1, 2$. Still by Lemma 4.2, $\mathfrak{s}(\text{alloc}(\phi_i)) \subseteq \text{dom}(\mathfrak{h}_i)$, and since $\mathfrak{h}_1$ and $\mathfrak{h}_2$ are disjoint, we deduce that $\mathfrak{s}(\text{alloc}(\phi_{3-i})) \cap \text{dom}(\mathfrak{h}_i) = \emptyset$ for $i = 1, 2$. Thus $\mathfrak{s}(V \cup \text{alloc}(\phi_{3-i})) \cap \text{dom}(\mathfrak{h}_i) = \emptyset$. By Corollary 4.3 $\mathfrak{s}$ is injective on $\text{alloc}(\phi_1 * \phi_2)$, hence since $\mathfrak{s}$ is injective on $V$, we deduce that $\mathfrak{s}$ is injective on $V \cup \text{alloc}(\phi_{3-i})$. Since $(\mathfrak{s}, \mathfrak{h}_i)$ cannot be a counter-model of the premises because $\mathfrak{h}_i \subset \mathfrak{h}$, this entails that $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \psi_i \wedge \zeta_i$ for $i = 1, 2$, thus $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} (\psi_1 * \psi_2) \wedge (\zeta_1 \wedge \zeta_2)$. $\square$

**4.4. Axioms and Anti-Axioms**

We define two sets of syntactic criteria on sequents that allow to quickly conclude that such sequents are respectively valid or non-valid. This will be useful to block the application of the inference rules in these cases. Axioms (i.e., necessarily valid sequents) are defined as follows.

**Definition 4.22.** An axiom is a sequent that is of one of the following forms modulo AC:

1. $\phi \lambda (\xi \wedge \xi') \vdash_{\mathfrak{R}}^{V} \phi \lambda \xi$;

2. $\phi \lambda (\xi \wedge x \not\approx x) \vdash_{\mathfrak{R}}^{V} \gamma$;

3. $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \gamma$ where $\phi$ is heap-unsatisfiable;

4. $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \gamma$ where either $\text{alloc}(\phi) \cap V \neq \emptyset$ or $V$ contains two occurrences of the same variable.

Intuitively, a sequent is valid if the right-hand side is a trivial consequence of the left-hand side, if the left-hand side is (trivially) unsatisfiable, or if $V$ contains a variable that is allocated by the left-hand side or two occurrences of the same variable (since by hypothesis counter-models must be injective on $V$).

**Lemma 4.23.** All axioms are valid.

**Proof:**

We consider each case separately (using the same notations as in Definition 4.22):

1. It is clear that every model of $\phi \lambda (\xi \wedge \xi')$ is a model of $\phi \lambda \xi$.

2. By definition, $\phi \lambda (\xi \wedge x \not\approx x) \vdash_{\mathfrak{R}}^{V} \gamma$ has no counter-model.

3. If $\phi$ is heap-unsatisfiable then $\text{alloc}(\phi)$ contains two occurrences of the same variable, which by Corollary 4.3, entails that $\phi$ has no model. Thus $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \gamma$ has no counter-model.
4. Let $(\mathfrak{s}, \mathfrak{h})$ be a counter-model of $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \gamma$. By definition $\mathfrak{s}$ is injective on $V$ hence we cannot have $\{x, x\} \subseteq_m V$. Also, by definition, if $x \in V$ then we cannot have $\mathfrak{s}(x) \in \text{dom}(\mathfrak{h})$, and if $x \in \text{alloc}(\phi)$ then if $x \in \text{alloc}(\phi) \cap V$ then $\mathfrak{s}(x) \in \text{dom}(\mathfrak{h})$ by Lemma 4.2. We conclude that it is impossible to have $x \in \text{alloc}(\phi) \cap V$ either.

□

We also introduce the notion of an anti-axiom, which is a sequent satisfying some syntactic conditions that prevent it from being valid.

**Definition 4.24.** A sequent $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$ is an *anti-axiom* if it is not an axiom, $\xi$ contains no equality, $\zeta = \top$ and one of the following conditions holds:

1. $\text{alloc}(\psi) \not\subseteq \text{alloc}(\phi)$;

2. $\psi = \text{emp}$ and $\phi \neq \text{emp}$.

3. There exists a variable $x \in \text{alloc}(\phi) \setminus \text{alloc}(\psi)$, such that $y \not\to_{\phi}^* x$ holds, for all $y \in \text{alloc}(\psi)$;

4. $V \cap (\mathcal{V}(\phi) \setminus \mathcal{V}(\psi))$ is not empty.

5. $\mathcal{V}_{\text{loc}}(\phi) \setminus (\mathcal{V}(\psi) \cup \text{alloc}(\phi))$ is not empty.

We provide examples illustrating every case in Definition 4.24:

**Example 4.25.** The following sequents (where $p$ is some arbitrary predicate) are anti-axioms:

1 : $p(x, y) \qquad \vdash_{\mathfrak{R}}^{\emptyset} p(y, x)$

3 : $p(x, y) * p(z, y) \qquad \vdash_{\mathfrak{R}}^{\emptyset} q(x, y)$

5 : $p(x, y) \qquad \vdash_{\mathfrak{R}}^{\emptyset} r(x)$

2 : $p(x, y) \qquad \vdash_{\mathfrak{R}}^{\emptyset} \text{emp}$

4 : $p(x, y) \qquad \vdash_{\mathfrak{R}}^{\{y\}} r(x)$

Intuitively, 1 cannot be valid because there exist models of $p(x, y)$ in which $y$ is not allocated whereas $y$ is allocated in all models of $p(y, x)$. Note that by Assumption 2.12, all predicates are productive, hence $p(x, y)$ admits at least one model. Furthermore, a predicate cannot allocate any of its arguments other than the root, for instance rules of the form $p(x, y) \Leftarrow x \mapsto (y) * p(y, x)$, indirectly allocating $y$, are not allowed. 2 cannot be valid because the models of $p(x, y)$ allocate at least $x$. For 3, assuming that all variables are associated with distinct locations, one can construct a model of $p(x, y) * p(z, y)$ in which there is no path from $x$ to $z$ and by Proposition 4.6 all locations occurring in the heap of any model of $q(x, y)$ must be reachable from $x$. For 4 and 5, we can construct a counter-model by considering any structure in which $y$ occurs in the heap but is not allocated, and by Lemma 4.7, all the locations occurring in the heap of any model of $r(x)$ must be allocated.

To show that all anti-axioms admit counter-models, we use the following lemma, which will also play a key rôle in the completeness proof. It states that all the formulas that are heap-satisfiable admit a model satisfying some particular properties:
**Lemma 4.26.** Let $\phi$ be a spatial formula, containing a variable $x$ of sort $\mathbf{loc}$. Let $\mathfrak{s}$ be a store that is injective on $\mathrm{alloc}(\phi)$. Let $U$ be an infinite subset of $\mathfrak{U}_{\mathbf{loc}}$ such that $U \cap \mathfrak{s}(\mathcal{V}_{\mathbf{loc}}) = \emptyset$. If $\phi$ is heap-satisfiable, then it admits an $\mathfrak{R}$-model of the form $(\mathfrak{s}, \mathfrak{h})$, where $\mathfrak{s}(x) \in \mathrm{ref}(\mathfrak{h})$, the set $\mathrm{dom}(\mathfrak{h})$ is a subset of $U \cup \mathfrak{s}(\mathrm{alloc}(\phi))$ and $\mathrm{ref}(\mathfrak{h}) \subseteq U \cup \mathfrak{s}(\mathcal{V}(\phi))$. Moreover, if $\mathfrak{s}$ is injective then $(\mathfrak{s}, \mathfrak{h})$ is a $\to$-compatible model of $\phi$.

**Proof:**

The proof is by induction on the formulas. Note that we cannot have $\phi = \mathrm{emp}$ since $x \in \mathcal{V}(\phi)$.

* If $\phi = y_0 \mapsto (y_1, \dots, y_n)$ then we set: $\mathfrak{h} \stackrel{\mathrm{def}}{=} \{(\mathfrak{s}(y_0), \dots, \mathfrak{s}(y_n))\}$. By definition, $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi$. Moreover, $x \in \{y_0, \dots, y_n\}$, and $\mathrm{ref}(\mathfrak{h}) = \{\mathfrak{s}(y_i) \mid i = 0, \dots, n \text{ and } y_i \in \mathcal{V}_{\mathbf{loc}}\}$, hence $\mathfrak{s}(x) \in \mathrm{ref}(\mathfrak{h})$ and $\mathrm{ref}(\mathfrak{h}) \subseteq \mathfrak{s}(\mathcal{V}(\phi))$. Furthermore, $\mathrm{dom}(\mathfrak{h}) = \{\mathfrak{s}(y_0)\}$ and $\mathrm{alloc}(\phi) = \{y_0\}$ thus $\mathrm{dom}(\mathfrak{h}) \subseteq \mathfrak{s}(\mathrm{alloc}(\phi))$. Finally, assume that $\mathfrak{s}$ is injective. We have by definition $\to_{\mathfrak{h}} = \{(\mathfrak{s}(y_0), \mathfrak{s}(y_i)) \mid i = 1, \dots, n\}$, thus if $\mathfrak{s}(u) \to_{\mathfrak{h}}^* \mathfrak{s}(v)$ for $u, v \in \mathcal{V}(\lambda)$ then we must have either $\mathfrak{s}(u) = \mathfrak{s}(v)$, so that $u = v$ because $\mathfrak{s}$ is injective, in which case it is clear that $u \to_{\phi}^* v$; or $\mathfrak{s}(u) = \mathfrak{s}(y_0)$ and $\mathfrak{s}(v) = \mathfrak{s}(y_i)$ for some $i = 1, \dots, n$. Since $\mathfrak{s}$ is injective this entails that $u = y_0, v = y_i$, thus $u \to_{\phi} v$ by definition of $\to_{\phi}$.

* Assume that $\phi = p(y_0, \dots, y_n)$ is a predicate atom. Then, since by Assumption 2.12 every predicate symbol is productive, there exists a symbolic heap $\gamma$ such that $\phi \Leftarrow_{\mathfrak{R}} \gamma$. If $x = y_0$ then since the rules in $\mathfrak{R}$ are P-rules, $\gamma$ contains a points-to-atom with root $x$. Otherwise, by Assumption 2.15, $x = y_i$ for some $i \in \mathrm{out}_{\mathfrak{R}}(p)$, hence there exists a rule application $\phi \Leftarrow_{\mathfrak{R}} \gamma$ such that $x$ occurs in some predicate atom in $\gamma$. Thus in both cases we may assume that $x$ occurs in a spatial atom in $\gamma$. Note that $\gamma$ must be heap-satisfiable, since all considered rules are P-rules and by Definition 2.7 the roots of the predicate symbols in $\gamma$ are pairwise distinct existential variables, thus also distinct from the root $y_0$ of the points-to atom. Furthermore, $\gamma$ is of the form $\psi \wedge \zeta$, where $x \in \mathcal{V}(\psi)$ and $\zeta$ is a conjunction of disequations $u \not\approx v$, with $u \neq v$.

Let $\mathfrak{s}'$ be an associate of $\mathfrak{s}$ w.r.t. $\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$ mapping the variables in $\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$ to pairwise distinct locations in $U$. Since by hypothesis $U \cap \mathfrak{s}(\mathcal{V}) = \emptyset$, $\mathfrak{s}'$ is injective on any set of the form $E \cup (\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi))$ when $\mathfrak{s}$ is injective on $E$. Let $U' \stackrel{\mathrm{def}}{=} U \setminus \mathfrak{s}'(\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi))$. By the induction hypothesis, there exists a heap $\mathfrak{h}$ such that $(\mathfrak{s}', \mathfrak{h}) \models_{\mathfrak{R}} \psi$, with $\mathfrak{s}'(x) \in \mathrm{ref}(\mathfrak{h})$, $\mathrm{dom}(\mathfrak{h}) \subseteq U' \cup \mathfrak{s}'(\mathrm{alloc}(\psi))$ and $\mathrm{ref}(\mathfrak{h}) \subseteq U' \cup \mathfrak{s}'(\mathcal{V}(\psi))$. Now if $\mathfrak{s}$ is injective then (as $\mathfrak{s}'$ is also injective in this case), $(\mathfrak{s}', \mathfrak{h})$ is a $\to$-compatible $\mathfrak{R}$-model of $\psi$. We show that $(\mathfrak{s}, \mathfrak{h})$ fulfills all the properties of the lemma.

- Since $\mathfrak{s}'$ maps the variables in $\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$ to pairwise distinct locations in $U$ and $\mathfrak{s}(\mathcal{V}) \cap U$ is $\emptyset$, necessarily $\mathfrak{s}' \models_{\mathfrak{R}} \zeta$, thus $(\mathfrak{s}', \mathfrak{h}) \models_{\mathfrak{R}} \gamma$ which entails that $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi$. We also have $\mathfrak{s}(x) = \mathfrak{s}'(x) \in \mathrm{ref}(\mathfrak{h})$.

- Let $\ell \in \mathrm{ref}(\mathfrak{h})$. We show that $\ell \in U \cup \mathfrak{s}(\mathcal{V}(\phi))$. By the induction hypothesis, we have $\ell \in U' \cup \mathfrak{s}'(\mathcal{V}(\psi))$. If $\ell \in U' \subseteq U$ then the proof is completed, otherwise we have $\ell = \mathfrak{s}'(y)$ for some $y \in \mathcal{V}(\psi)$. If $y \in \mathcal{V}(\phi)$ then $\mathfrak{s}(y) = \mathfrak{s}'(y)$ thus $\ell \in \mathfrak{s}(\mathcal{V}(\phi))$. Otherwise, we must have $y \in \mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$, thus $\mathfrak{s}'(y) \in U$ by definition of $\mathfrak{s}'$ and the result holds.
- Let $\ell \in \text{dom}(\mathfrak{h})$, we show that $\ell \in U \cup \mathfrak{s}(\text{alloc}(\phi))$. By the induction hypothesis we have $\ell \in U' \cup \mathfrak{s}'(\text{alloc}(\psi))$. If $\ell \in U' \subseteq U$ then the proof is completed. Otherwise, $\ell = \mathfrak{s}'(y)$ with $y \in \text{alloc}(\psi)$. Since the rules in $\mathfrak{R}$ are P-rules, $y$ is either the root $y_0$ of $\phi$, in which case we have $y \in \text{alloc}(\phi)$ and $\mathfrak{s}(y) = \mathfrak{s}'(y)$, thus the result holds; or $y$ occurs in $\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$, in which that we have $\mathfrak{s}'(y) \in U$, by definition of $\mathfrak{s}'$.

- There remains to show that $(\mathfrak{s}, \mathfrak{h})$ is a $\to$-compatible $\mathfrak{R}$-model of $\phi$, in the case where $\mathfrak{s}$ is injective. Assume that $\mathfrak{s}(u) \to_{\mathfrak{h}}^{*} \mathfrak{s}(v)$. If $\mathfrak{s}(u) = \mathfrak{s}(v)$ then $u = v$ by injectivity of $\mathfrak{s}$, hence $u \to_{\mathfrak{h}}^{*} v$. Otherwise, we must have $\{\mathfrak{s}(u), \mathfrak{s}(v)\} \subseteq \text{ref}(\mathfrak{h}) \subseteq U' \cup \mathfrak{s}'(\mathcal{V}(\psi))$, and since $U' \subseteq U$ and $U \cap \mathfrak{s}(\mathcal{V}) = \emptyset$, we have $\{\mathfrak{s}(u), \mathfrak{s}(v)\} \subseteq \mathfrak{s}'(\mathcal{V}(\psi))$. We also have $\mathfrak{s}'(\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)) \subseteq U$, which entails that $\{\mathfrak{s}(u), \mathfrak{s}(v)\} \subseteq \mathfrak{s}'(\mathcal{V}(\phi))$. Since $\mathfrak{s}'$ is an associate of $\mathfrak{s}$ w.r.t. $\mathcal{V}(\gamma) \setminus \mathcal{V}(\phi)$, $\mathfrak{s}$ and $\mathfrak{s}'$ coincide on all variables in $\mathcal{V}(\phi)$ and we deduce that $\{\mathfrak{s}(u), \mathfrak{s}(v)\} \subseteq \mathfrak{s}(\mathcal{V}(\phi))$. Because $\mathfrak{s}$ is injective, this entails that $u, v \in \mathcal{V}(\phi)$, so that $\mathfrak{s}(u) = \mathfrak{s}'(u)$ and $\mathfrak{s}(v) = \mathfrak{s}'(v)$. By hypothesis $(\mathfrak{s}', \mathfrak{h})$ is a $\to$-compatible $\mathfrak{R}$-model of $\psi$, and we deduce that $u \to_{\psi}^{*} v$. Since $u \neq v$, necessarily $u \in \text{alloc}(\psi)$ (by definition of $\to_{\psi}$), and since the rules in $\mathfrak{R}$ are P-rules, and $u \in \mathcal{V}(\phi)$, this entails that $u = \text{roots}(\phi)$. Since $v \in \mathcal{V}(\phi)$, by Assumption 2.15 we have $u \to_{\phi}^{*} v$.

* Assume that $\phi = \phi_1 * \phi_2$, with $\phi_i \neq \text{emp}$. Let $U_1, U_2$ be disjoint infinite subsets of $U$. Let $\{x_1, x_2\}$ be some arbitrary chosen variables such that $x_i \in \mathcal{V}(\phi_i)$ and $x \in \{x_1, x_2\}$ (it is easy to check that such a pair of variables always exists). By the induction hypothesis, there exist heaps $\mathfrak{h}_i$ such that $(\mathfrak{s}, \mathfrak{h}_i) \models \phi_i$ where $\mathfrak{s}(x_i) \in \text{ref}(\mathfrak{h}_i)$, $\text{dom}(\mathfrak{h}_i) \subseteq U_i \cup \mathfrak{s}(\text{alloc}(\phi_i))$ and $\text{ref}(\mathfrak{h}_i) \subseteq U_i \cup \mathfrak{s}(\mathcal{V}(\phi_i))$. Moreover, if $\mathfrak{s}$ is injective, then $(\mathfrak{s}, \mathfrak{h}_i)$ is an $\to$-compatible $\mathfrak{R}$-model of $\phi_i$. We first show that $\mathfrak{h}_1$ and $\mathfrak{h}_2$ are disjoint. Assume for the sake of contradiction that $\ell \in \text{dom}(\mathfrak{h}_1) \cap \text{dom}(\mathfrak{h}_2)$. Since $U_1 \cap U_2 = \emptyset$, necessarily $\ell = \mathfrak{s}(y_i)$ (for $i = 1, 2$), with $y_i \in \text{alloc}(\phi_i)$. Since $\mathfrak{s}$ is injective on $\text{alloc}(\phi)$, we deduce that $y_1 = y_2$. We have $\{y_1, y_2\} \subseteq_m \text{alloc}(\phi)$, hence $\phi$ is heap-unsatisfiable, which contradicts the hypotheses of the lemma. Thus $\mathfrak{h}_1$ and $\mathfrak{h}_2$ are disjoint.

Let $\mathfrak{h} = \mathfrak{h}_1 \uplus \mathfrak{h}_2$. We have $\mathfrak{s}(x) \in \{\mathfrak{s}(x_1), \mathfrak{s}(x_2)\} \subseteq \text{ref}(\mathfrak{h}_1) \cup \text{ref}(\mathfrak{h}_2) = \text{ref}(\mathfrak{h})$. Moreover, $\text{dom}(\mathfrak{h}) = \text{dom}(\mathfrak{h}_1) \cup \text{dom}(\mathfrak{h}_2) \subseteq U_1 \cup U_2 \cup \mathfrak{s}(\text{alloc}(\phi_1)) \cup \mathfrak{s}(\text{alloc}(\phi_2)) \subseteq U \cup \mathfrak{s}(\text{alloc}(\phi))$, and $\text{ref}(\mathfrak{h}) = \text{ref}(\mathfrak{h}_1) \cup \text{ref}(\mathfrak{h}_2) \subseteq U_1 \cup U_2 \cup \mathfrak{s}(\mathcal{V}(\phi_i)) \cup \mathfrak{s}(\mathcal{V}(\phi_2)) \subseteq U \cup \mathfrak{s}(\mathcal{V}(\phi))$. Furthermore, $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi_1 * \phi_2 = \phi$.

There only remains to prove that $(\mathfrak{s}, \mathfrak{h})$ is a $\to$-compatible $\mathfrak{R}$-model of $\phi$ when $\mathfrak{s}$ is injective. Assume that this is not the case, and let $u, v$ be variables such that $\mathfrak{s}(u) \to_{\mathfrak{h}}^{*} \mathfrak{s}(v)$ and $u \not\to_{\phi}^{*} v$. This entails that $u \neq v$. By definition, there exist $\ell_0, \dots, \ell_m$ such that $\ell_0 = \mathfrak{s}(u)$, $\ell_m = \mathfrak{s}(v)$, and $\forall i = 1, \dots, m$, $\ell_{i-1} \to_{\mathfrak{h}} \ell_i$. We assume, w.l.o.g., that $m$ is miminal, i.e., that there is no sequence $\ell'_0, \dots, \ell'_k$ and no variables $x_0, x_k$ such that $k < m$, $\ell'_0 = \mathfrak{s}(x_0)$, $\ell'_k = \mathfrak{s}(x_k)$ and $x_0 \not\to_{\phi}^{*} x_k$. We may also assume, by symmetry, that $\ell_0 \in \text{dom}(\mathfrak{h}_1)$. If all the locations $\ell_1, \dots, \ell_{m-1}$ occur in $\text{dom}(\mathfrak{h}_1)$ then $\mathfrak{s}(u) \to_{\mathfrak{h}_1}^{*} \mathfrak{s}(v)$, thus $u \to_{\phi_i}^{*} v$ because $(\mathfrak{s}, \mathfrak{h}_i)$ is an $\to$-compatible $\mathfrak{R}$-model of $\phi_i$, which entails that $u \to_{\phi}^{*} v$ since by definition $\to_{\phi_i} \subseteq \to_{\phi}$, contradicting our assumption. Otherwise, let $j$ be the smallest index in $\ell_1, \dots, \ell_{m-1}$ such that $\ell_j \notin \text{dom}(\mathfrak{h}_1)$. Since $\ell_j \in \text{dom}(\mathfrak{h})$ (as $\ell_j \to_{\lambda} \ell_{j+1}$) we deduce that $\ell_j \in \text{dom}(\mathfrak{h}_2) \subseteq \text{ref}(\mathfrak{h}_2)$, and $\ell_j \in \text{ref}(\mathfrak{h}_1)$. Since $U_1 \cap U_2 = \emptyset$, we get $\ell_j = \mathfrak{s}(\mathcal{V}(\phi_i))$, for some $i = 1, 2$. Thus
$l_j = s(u')$ with $u' \in V(\phi)$. Since $u \not\to_{\phi}^* v$, we have by transitivity either $u \not\to_{\phi}^* u'$ or $u' \not\to_{\phi}^* v$, which contradicts the minimality of $m$ (one of the sequences $l_1, \dots, l_j$ or $l_j, \dots, l_m$ satisfies the conditions above and has a length strictly less than $m+1$).

□

**Lemma 4.27.** All anti-axioms admit counter-models.

**Proof:**

Consider an anti-axiom $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$, with the same notations as in Definition 4.24. Let $s$ be an injective store such that $\mathfrak{U}_{\text{loc}} \setminus s(V)$ is infinite, such a store always exists since $\mathfrak{U}_{\text{loc}}$ is infinite. First assume that $\phi \neq \text{emp}$. In this case $\phi$ necessarily contains at least one spatial atom $\alpha$, hence at least one variable $x = \text{root}(\alpha)$ of sort loc. Since $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$ is not an axiom, $\phi$ is heap-satisfiable, thus by Lemma 4.26 (applied with $U \stackrel{\text{def}}{=} \mathfrak{U}_{\text{loc}} \setminus s(V)$), $\phi \wedge \xi$ admits a $\to$-compatible model $(s, h)$, such that $\text{dom}(h) \subseteq U \cup s(\text{alloc}(\phi))$. Since $U \cap s(V) = \emptyset$, we have, for all $u \in V$, $s(u) \in \text{dom}(h) \iff s(u) \in s(\text{alloc}(\phi))$. Since $s$ is injective, we deduce that

$$s(u) \in \text{dom}(h) \iff u \in \text{alloc}(\phi) \ (\dagger).$$

Note that if $\phi = \text{emp}$, then the structure $(s, h)$ with $h = \emptyset$ also satisfies $(\dagger)$, since $\to_h, \to_{\phi}, \text{dom}(h)$ and $\text{alloc}(\phi)$ are all empty in this case.

We show that $(s, h)$ is a counter-model of $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$. Since $s$ is injective, in particular $s$ must be injective on $V$, because otherwise $V$ would contain two occurrences of the same variable, hence $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$ would be an axiom, contradicting Definition 4.24. If $V$ contains a variable $y$ such that $s(y) \in \text{dom}(h)$ then $(\dagger)$ entails that $y \in \text{alloc}(\phi)$, which is impossible since $\phi \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \zeta$ would then be an axiom. We prove that $(s, h) \not\models_{\mathfrak{R}} \psi \wedge \zeta$ by considering each case from Definition 4.24 separately.

1. If $\text{alloc}(\psi) \setminus \text{alloc}(\phi)$ contains a variable $y$, then by $(\dagger)$ we have $s(y) \notin \text{dom}(h)$, which by Lemma 4.2 entails that $(s, h) \not\models_{\mathfrak{R}} \psi$.

2. If $\psi = \text{emp}$ and $\phi \neq \text{emp}$, then $\phi$ contains at least one atom, hence $\text{alloc}(\phi) \neq \emptyset$. By Lemma 4.2, $s(\text{alloc}(\phi)) \subseteq \text{dom}(h)$, thus $h \neq \emptyset$ and $(s, h) \not\models_{\mathfrak{R}} \psi \wedge \zeta$.

3. Assume that there exists a variable $x' \in \text{alloc}(\phi) \setminus \text{alloc}(\psi)$ such that $y \not\to_{\phi} x'$, for all $y \in \text{alloc}(\psi)$, and that $(s, h) \models_{\mathfrak{R}} \psi$. By Lemma 4.2 we have $s(x') \in \text{dom}(h) \subseteq \text{ref}(h)$, thus by Proposition 4.6 there exists $y \in \text{alloc}(\psi)$ such that $s(y) \to_{h}^* s(x)$. Since $(s, h)$ is a $\to$-compatible model of $\phi$ necessarily $y \to_{\phi}^* x'$, which contradicts the above assumption.

For the remaining cases, we will apply Lemma 4.26 to obtain a heap, using a variable $x$ that is in $V \cap (V(\phi) \setminus V(\psi))$ (for Condition 4) or in $V_{\text{loc}}(\phi) \setminus (V(\psi) \cup \text{alloc}(\phi))$ (for Condition 5). Note that by Lemma 4.26 this entails in particular that $s(x) \in \text{ref}(h)$.

4. Assume that $x \in V \cap V(\phi)$ and $x \notin V(\psi)$. Then $s(x) \in \text{ref}(h)$ and since $x \in V$ we get $s(x) \notin \text{dom}(h)$. By Lemma 4.7, if $(s, h) \models_{\mathfrak{R}} \psi$ then we have $s(x) \in s(V(\psi))$, and $x \in V(\psi)$ since $s$ is injective. Thus we get a contradiction.
5. Assume that $x \in V_{\text{loc}}(\phi)$, $x \notin V(\psi)$ and $x \notin \text{alloc}(\phi)$. By $(\dagger)$, we deduce that $s(x) \notin \text{dom}(h)$. Assume that $(s, h) \models_{\mathfrak{R}} \psi$. Since $x \notin V(\psi)$ and $s$ is injective, we get $s(x) \notin s(V(\psi))$. By Lemma 4.7, we deduce that $s(x) \notin \text{ref}(h)$, a contradiction.

□

## 4.5. Proof Trees

A proof tree is a (possibly infinite) tree with nodes labeled by sequents, such that if a node labeled by $S$ has successors labeled by $S_1, \dots, S_n$ then there exists a rule instance of the form $\frac{S_1 \dots S_n}{S}$. We will usually identify the nodes in a proof tree with the sequents labeling them. A path from $S$ to $S'$ in a proof tree is a finite sequence $S_0, \dots, S_n$ such that $S = S_0, S_n = S'$ and for all $i = 1, \dots, n$, $S_i$ is a successor of $S_{i-1}$. A proof tree is fully expanded if all its leaves are axioms. It is rational if it contains a finite number of subtrees, up to a renaming of variables. Note that rational trees may be infinite, but they can be represented finitely. A sequent $S'$ is a descendant of a sequent $S$ if there exists a proof tree with a path from $S$ to $S'$.

**Example 4.28.** Let $\mathfrak{R}$ be the following set of rules, where a, b denote constant symbols and $u$ is a variable of the same sort as b:

$$
\begin{align*}
p(x, y) &\Leftarrow x \mapsto (a, y, z) * p(z, y) \\
p(x, y) &\Leftarrow x \mapsto (b) \\
r(x) &\Leftarrow x \mapsto (a, y, z) * r(z) \\
r(x) &\Leftarrow x \mapsto (u)
\end{align*}
$$

The sequent $p(x, y) \vdash_{\mathfrak{R}}^0 r(x)$ admits the following rational proof tree (the sequent $p(z, y) \vdash_{\mathfrak{R}}^0 r(z)$ is identical to the conclusion up to a renaming):

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \begin{array}{c} \xrightarrow{x \mapsto (a, y, z) \vdash_{\mathfrak{R}}^{\{z\}} x \mapsto (a, y, z)} \text{axiom} \\ \xrightarrow{x \mapsto (a, y, z) * p(z, y) \vdash_{\mathfrak{R}}^{0} x \mapsto (a, y, z) * r(z)} \text{axiom} \end{array}
    &
    \begin{array}{c} \xrightarrow{p(z, y) \vdash_{\mathfrak{R}}^{0} r(z)} \text{V} \\ \xrightarrow{p(z, y) \vdash_{\mathfrak{R}}^{\{x\}} r(z)} \text{S} \end{array}
    &
    \begin{array}{c} \xrightarrow{x \mapsto (b) \vdash_{\mathfrak{R}}^{0} x \mapsto (b)} \text{I} \\ \xrightarrow{x \mapsto (b) \vdash_{\mathfrak{R}}^{0} r(x)} \text{U} \end{array}
\end{tikzcd}
$$

**Remark 4.29.** Note that, since infinite proof trees are allowed, the fact that each rule is sound does not imply that the procedure itself is sound, i.e., that the root of every fully expanded proof tree is valid. The latter property holds only for the strategy introduced in the next section, see Theorem 5.13.

## 4.6. The Strategy

In this section, we introduce a strategy to restrict the application of the inference rules, which will ensure both the soundness and efficiency of the proof procedure. To this purpose, we define a set of variables $V^\dagger(S)$ which denotes the variables occurring at non-root positions on the right-hand side of
the considered sequent, but not in the set of non-allocated variables $V$. As we shall see, the strategy will handle the sequents in different ways depending on the number of such variables. Recall that $width(\mathfrak{R})$ denotes the maximal arity of the predicate symbols and tuples occurring in $\mathfrak{R}$.

**Definition 4.30.** For every sequent $S = \lambda \vdash_{\mathfrak{R}}^{V} \gamma$, we denote by $V^{\dagger}(S)$ the set $V_{\text{loc}}(\gamma) \setminus (V \cup \text{alloc}(\gamma))$. A sequent $S$ is narrow if it is equality-free and $\text{card}(V^{\dagger}(S)) \leq \text{width}(\mathfrak{R})$.

Note that in particular, if $\gamma$ is a spatial atom, then $S$ is necessarily narrow since in this case we must have $\text{card}(V(\gamma)) \leq \text{ar}_{\text{max}}(\mathfrak{R}) \leq \text{width}(\mathfrak{R})$. The inference rules are applied with the following strategy:

**Definition 4.31.** We assume a selection function is given, mapping every nonempty finite set of expressions (i.e., formulas or rule applications) $S$ to an element of $S$; this element is said to be selected in $S$. We also assume that this function can be computed in polynomial time. A proof tree is admissible if all the rule applications occurring in it fulfill the following conditions (see Figure 3 for the notations):

1. No rule is applied on an axiom or an anti-axiom, and no rule is applied if one of the premises is an anti-axiom.

2. I is applied only if $\zeta = \top$ and $\psi = \text{emp}$.

3. U is applied only if $\gamma$ is of one of the forms $q(x_1, y) \wedge \top$ or $x_1 \mapsto y \wedge \top$, where $x_1$ is the first component of the vector $t$ (as defined in the rule).

4. C is applied only if $\gamma$ is of the form $\psi \wedge \top$, $x \in \text{alloc}(\phi)$, $y \in V(\gamma) \setminus (\text{alloc}(\phi) \cup V)$, $\psi$ is a predicate atom and $x \not\approx y$ does not already occur in $\xi$.

5. S is applied only if $\xi_1 = \xi_2$, $\zeta_1 = \zeta_2 = \top$, and $\psi_1$ is selected in the set of atoms in $\psi_1 * \psi_2$. Furthermore, if the conclusion is not narrow, then the rule is applied only if the left-premise is valid (this will be tested by applying the decision procedure recursively).

6. The rules are applied with the following priority (meaning that no rule can be applied if a rule with a higher priority is also applicable):

$W > V > R > E > S > U > C > I.$

7. For all the rules other than S, and for all applications of S on a sequent that is not narrow, if several applications of the rule are possible and all fulfill the conditions above, then only the one that is selected in the set of possible rule applications can be applied.

From now on, we assume that all the considered proof trees are admissible (the soundness<fnref n="3" /> and completeness proofs below, as well as the complexity analysis hold with this requirement). No assumption is made on the selection function, for instance one may assume that $\psi_1$ is the leftmost atom

<footnote n="3">³The soundness of each individual rule, as stated by Lemmata 4.19 and 4.21, does not depend on Definition 4.31, but the global soundness of the procedure, as stated in Theorem 5.13 holds only for admissible proof trees.</footnote>
in $\psi_1 * \psi_2$ (i.e., the atoms are ordered according to the order in which they occur in the formula) and
that the first detected rule application is applied, except for S if the conclusion is narrow.

Many of the conditions in Definition 4.31 are quite natural, and simply aim at pruning the search
space by avoiding irrelevant rule applications. For instance, applying a rule on an axiom or on an anti-
axiom is clearly useless. The priority order is chosen in such a way that the rules with the minimal
branching factor are applied first, postponing the most computationally costly rules. Similarly, the
rules operating on spatial atoms (I or U) are postponed until all pure formulas have been handled. The
unfolding of the atoms on the left-hand side of a sequent (Rule U) is postponed until the right-hand
side has been fully decomposed (using rule S), yielding a unique spatial atom. This permits to guide
the choice of the atom to be unfolded on the left-hand side: we only unfold the atom with the same
root as the one on the right-hand side. Rule C may cause a costly explosion if applied blindly, thus
the application conditions are carefully designed. They are meant to ensure that the rule application is
really useful, in the sense that it permits further applications of rule I. Condition 7 in Definition 4.31
is meant to ensure that the considered rules are applied with a "don't care" strategy, meaning that
if several rule applications are possible then one of them (the selected one) is chosen arbitrarily and
the others are ignored. This is justified by the fact that these rules are invertible, hence exploring all
possibilities is useless. Such a strategy is crucial for proving that the procedure runs in polynomial
time. In contrast, if the conclusion of S is narrow, then the rule must applied with a "don't know"
indeterminism, i.e., all possible applications must be considered. This is necessary for completeness,
due to the fact that the rule is *not* invertible in this case. Of course, all these possible rule applications
must be taken into account for the complexity analysis. In other words, one must cope with two
different kinds of branching: an "and-branching" due to the fact that a given rule may have several
premises, and an "or-branching" due to the fact that there may be several ways of applying a given
rule on a given sequent. By Condition 7, the latter branching occurs only when the rule S is applied on
a narrow sequent; in all other cases, only the selected rule application can be considered hence there
is no or-branching.

The requirement that $\psi_1$ must be selected in Condition 5 ensures that only one decomposition
$\psi_1 * \psi_2$ can be considered for the right-hand side of a given sequent. This avoids for instance the
exponential blow-up that would occur if the same decomposition was performed in different orders.
Note that, to check whether the left premise is valid in Condition 5, it is necessary to recursively
invoke the proof procedure. As we shall see below, this is feasible because this premise and all its
descendants are necessarily narrow:

**Proposition 4.32.** Let $S_1$ be an equality-free sequent. For every successor $S_2$ of $S_1$, the relation $V^\dagger(S_2) \subseteq V^\dagger(S_1)$ holds. Consequently, if a sequent is narrow then all its descendants are narrow.

**Proof:**

Let $S_i = \lambda_i \vdash_{\mathfrak{S}_i}^{V_i} \gamma_i$ for $i = 1, 2$. Assume for the sake of contradiction that $V^\dagger(S_2) \setminus V^\dagger(S_1)$ contains a variable $u$. By definition, $u \in V(\gamma_2)$ and $u \notin \text{alloc}(\gamma_2) \cup V_2$. First assume that $u \notin V(\gamma_1)$, i.e., that $u$ was introduced by the application of an inference rule to $S_1$. By Proposition 4.17 (4), the only rule that can introduce new variables to the right-hand side of a sequent is I. Indeed, since we assume that all inferences are admissible, by Condition 4 of Definition 4.31, C must replace a variable $x$ by a variable $y$ occurring in $V(\gamma_1)$. Rule I replaces a predicate atom $p(x, z)$ that occurs in $\gamma_1$ by a formula
of the form $\gamma'_1\sigma$, where $p(x, z) \Leftarrow \Re \ \gamma'_1 \wedge \zeta'$. Since the rules in $\Re$ are P-rules, by Condition 2 of Definition 2.7, all the variables occurring in $\gamma'_1\sigma$ but not in $p(x, z)$ must occur as roots in $\gamma'_1\sigma$. This entails that $V(\gamma_2) \setminus V(\gamma_1) \subseteq alloc(\gamma_2)$, which contradicts the fact that $u \notin alloc(\gamma_2) \cup V$. We deduce that $u \in V(\gamma_1)$.

Assume that $u \in V_1$. Since $u \notin V_2$, the inference rule applied to $S_1$ must have deleted a variable from $V_1$. The only rules that can delete variables from $V_1$ are V and C by Proposition 4.17 (2). Rule V applies only on a variable $x \notin V(\gamma_1)$, thus we cannot have $x = u$. If Rule C is applied and replaces a variable $x$ by $y$, then $x$ cannot occur in $S_2$, hence $u \neq x$. Thus we must have $u \notin V_1$.

Finally assume that $u \in alloc(\gamma_1)$. Since $u \notin alloc(\gamma_2)$, the inference rule applied to $S_1$ must have deleted a variable from $alloc(\gamma_1)$. The only rules that can delete variables from $alloc(\gamma_1)$ are S and C by Proposition 4.17 (3). Again, if rule C replaces a variable $x$ by $y$, then $x$ cannot occur in $S_2$, hence $u \neq x$. Now, consider rule S and let $S'_2 \stackrel{\text{def}}{=} \lambda'_2 \vdash_{\Re}^{V'_2} \gamma'_2$ be the other premise of the rule. Since $u \in alloc(\gamma_1)$ and $S_1$ is not an anti-axiom, we must have $u \in alloc(\lambda_1)$, which entails by definition of the rule that $u \in alloc(\lambda_2) \cup V_2$ and $u \in alloc(\lambda'_2) \cup V'_2$. Still by definition of rule S, if a variable is the root of a spatial atom occurring on the right-hand side of the conclusion $\gamma_1$, then this spatial atom must occur on the right-hand side of one of the premises $\gamma_2$ or $\lambda'_2$. This entails that $u \in alloc(\gamma_2) \cup alloc(\lambda'_2)$. Furthermore, we must have $alloc(\lambda_2) \cap alloc(\lambda'_2) = \emptyset$ because otherwise $S_1$ would contain two atoms with the same root, hence would be an axiom. Since $u \notin V_2$ we deduce that $u \in alloc(\lambda_2)$, and that $u \in V'_2$. If $u \notin alloc(\gamma_2)$ then necessarily $u \in alloc(\gamma'_2)$. Since $S'_2$ is not an anti-axiom we deduce that $u \in alloc(\lambda'_2)$, which entails that $S'_2$ is an axiom since $alloc(\lambda'_2) \cap V'_2 \neq \emptyset$, a contradiction.

The second part of the proposition follows by an immediate induction, using the fact that no rule can introduce any equality in its premises. $\square$

We call auxiliary successors the sequents whose validity must be tested to check whether rule S is applicable or not, according to Definition 4.31:

**Definition 4.33.** A sequent $S$ is an auxiliary successor of a sequent $S'$ if:

* $S$ is not an anti-axiom and is not narrow,

* $S'$ is not an axiom,

* $S'$ and $S$ are of the form $\phi' \wedge \xi \vdash_{\Re}^{V'} \psi' \wedge \top$ and $(\phi' * \phi) \wedge \xi \vdash_{\Re}^{V} (\psi' * \psi) \wedge \top$ respectively, where $\psi'$ is a spatial atom, and $V' = V \cup alloc(\phi)$.

If the sequent $S$ in Definition 4.33 is valid, then it is the left premise of an application of $S$ on $S'$. The following proposition gives an upper-bound on the number of auxiliary successors.

**Proposition 4.34.** Assume that $ar_{max}(\Re) \le \kappa$ (i.e., that the maximal arity of the predicates is bounded by $\kappa$). Then every sequent $S$ has at most $2^\kappa$ auxiliary successors, and each of these auxiliary successors can be computed in polynomial time.

**Proof:**

If $S$ admits an auxiliary successor, then $S$ is necessarily of the form $\phi \wedge \xi \vdash_{\Re}^{V} \psi_1 * \psi_2$ where $\psi_1$ is the selected predicate atom in $\psi_1 * \psi_2$ according to Definition 4.31. To get an auxiliary successor of $S$,
one has to decompose $\phi$ into $\phi_1 * \phi_2$, in such a way that the obtained premises $S_i = \phi_i \wedge \xi \vdash_{\mathfrak{R}}^{V_i} \psi_i$ (with $V_i = V \cup alloc(\phi_{3-i})$) are not anti-axioms. For each atom $\alpha$ in $\phi$ such that $root(\alpha) \in V(\psi_1)$, we first choose whether $\alpha$ occurs in $\phi_1$ or $\phi_2$. There is at most one such atom for each variable, because otherwise $\phi$ would be heap-unsatisfiable and $S$ would be an axiom, and $\psi_1$ contains at most $\kappa$ variables, thus there are at most $2^\kappa$ possible choices.

We show that, once this choice is performed, the decomposition $\phi = \phi_1 * \phi_2$ is also fixed. We denote by $E$ the set of variables $V(\psi_1) \setminus alloc(\phi_1)$. Let $\alpha$ be a predicate atom with root $x$ in $\phi$, and let $y_0$ be the root of $\psi_1$. If $x = y_0$ then necessarily $\alpha$ occurs in $\phi_1$, since otherwise $x \in V_1$ and $S_1$ would be an anti-axiom. If for all paths $y_0 \to_\phi y_1 \to_\phi \dots \to_\phi y_n \to_\phi x$, there exists $i = 1, \dots, n$ such that $y_i \in E$, then necessarily $y \nVdash_{\phi_1}^* x$ and thus $\alpha$ cannot occur in $\phi_1$, as otherwise $S_1$ would be an anti-axiom. We finally show that for every atom $\alpha'$ in $\phi$ with root $x'$, if there exists a path $y_0 \to_\phi y_1 \to_\phi \dots \to_\phi y_n \to_\phi x'$ such that $\{y_1, \dots, y_n, x'\} \cap E = \emptyset$, then $\alpha'$ occurs in $\phi_1$ (thus, in particular, $\alpha$ occurs in $\phi_1$ if the previous conditions are not satisfied, since $x \notin E$, as $x \notin V(\psi_1)$). We assume, w.l.o.g., that the considered path is the minimal one not satisfying the property, so that the atoms with roots $y_0, \dots, y_n$ all occur in $\phi_1$. This entails that $y_0 \to_{\phi_1}^* x'$. If $x' \notin V(\psi_1)$ then $\alpha$ must occur in $\phi_1$, otherwise $S_1$ would be an anti-axiom, because we would have $x' \in V_1$, as $x' \in alloc(\phi_2)$. Otherwise, since $x' \notin E$, we have $x' \in alloc(\phi_2)$, by definition of $E$.

To sum up, assuming that $S = \phi \wedge \xi \vdash_{\mathfrak{R}}^{V} \psi$ is neither an axiom nor an anti-axiom, the auxiliary successors of $S$ are computed as follows. We first compute the selected atom $\psi_1$ in $\psi$ (which can be done in polynomial time by the assumption in Definition 4.31). The atoms $\alpha$ in $\phi$ are added either to $\phi_1$ or to $\phi_2$ using the following algorithm. Initially, $\phi_1$ and $\phi_2$ are both empty. If $root(\alpha) = root(\psi_1)$ then $\alpha$ is moved from $\phi$ to $\phi_1$ (there is exactly one atom with this property). For each atom $\alpha$ in $\phi$ with $root(\alpha) \in V(\psi_1)$ and $root(\alpha) \neq root(\psi_1)$, we nondeterministically add $\alpha$ to either $\phi_1$ or $\phi_2$ (which yields at most $2^\kappa$ possible choices) and remove $\alpha$ from $\phi$. Then, for each atom $\alpha$ in $\phi_1$, all the remaining atoms $\alpha'$ in $\phi$ such that $root(\alpha') \in V(\alpha)$ are also moved from $\phi$ to $\phi_1$. This rule is applied recursively until no such atom exists. Afterwards, all the atoms still remaining in $\phi$ are added to $\phi_2$. It is clear that all these operations can be performed in polynomial time w.r.t. the size of $S$ (in particular, the number of applications of the previous rule is bounded by the number of atoms in $\phi$). $\square$

# 5. Properties of the Proof Procedure

## 5.1. Soundness

We prove that the proof procedure is sound, in the sense that the root of every fully expanded proof tree fulfilling the conditions of Definition 4.31 is valid. As infinite proof trees are allowed, this does not follow from the fact that all the rules are sound. We show that every infinite branch contains infinitely many applications of the rule $S$. As we shall see, this is sufficient to ensure that no counter-model exists, since otherwise the size of the smallest counter-model would be decreasing indefinitely along some infinite branch. We recall that the rules are meant to be applied bottom-up: a rule is applicable on some sequent $S$ if it admits an instance with conclusion $S$, yielding some premises $S_1, \dots, S_n$. We focus on sequents on which rule $I$ is applied (which we call $I$-reducible), and we establish some useful properties.
**Definition 5.1.** A sequent is I-reducible if rule I can be applied on it; this entails that no other rule is applicable, as all other rules have priority over I. A sequent $\mathcal{S}$ is quasi-I-reducible if it is of the form $(x \mapsto y * \phi) \wedge \xi \vdash_{\mathfrak{R}}^V \psi \wedge \top$, where $\xi$ is a conjunction of disequations, $\psi$ is a predicate atom with root $x$, and $\mathcal{S}$ is not an axiom. If $\mathcal{S}$ is quasi-I-reducible then we denote by $V_{\mapsto}(\mathcal{S})$ the set of variables occurring in $y$.

Note that the definition of $V_{\mapsto}(\mathcal{S})$ is unambiguous because the left-hand side of $\mathcal{S}$ cannot contain more than one points-to atom with root $x = \text{root}(\psi)$, otherwise it would be heap-unsatisfiable and $\mathcal{S}$ would be an axiom. It is easy to check that every I-reducible sequent is quasi-I-reducible (see Definition 4.31, Condition 2). The converse does not hold in general, because rules W, V or C may be applicable on the considered sequent, and they have priority over I. We observe that the application of I is necessarily interleaved with that of S:

**Lemma 5.2.** Every path in a proof tree between two distinct I-reducible sequents contains an application of rule S.

**Proof:**

Let $S_1$ be an I-reducible sequent and assume that $S_2$ is a descendant of $S_1$. By definition, the only rule that applies on $S_1$ is I, yielding a sequent $S_1'$. Since the rules in $\mathfrak{R}$ are P-rules, necessarily the right-hand side of $S_1'$ contains exactly one points-to atom. Since $S_2$ is I-reducible, I applies on $S_2$, which entails that no points-to atom can occur on the right-hand side of $S_2$ (since I applies only when the right-hand side is a predicate atom). The only rule that can remove a points-to atom from the right-hand side of a sequent is S, thus S necessarily applies along the path from $S_1$ to $S_2$. $\square$

To analyze the termination behavior of the rules, we define a new set of variables $V^*(S)$, which is similar to $V^\dagger(S)$: it contains variables that occur on the right-hand side of the considered sequent but are not allocated on the left-hand side, and that do not occur either in the set of non-allocated variables $V$.

**Definition 5.3.** For every sequent $S = \lambda \vdash_{\mathfrak{R}}^V \gamma$, we denote by $V^*(S)$ the set $V_{\text{loc}}(\gamma) \setminus (V \cup \text{alloc}(\lambda))$.

Note that, since the considered inferences are admissible, if rule C applies on variables $x, y$ (with the notations of the rule), then necessarily $y \in V^*(S)$ and $x \in V(\lambda)$ (see Condition 4 in Definition 4.31). The next proposition states that the rules (except possibly R) cannot add new variables in the set $V^*(S)$.

**Proposition 5.4.** Let $S_1$ be a sequent containing no equality. For every successor $S_2$ of $S_1$, we have $V^*(S_2) \subseteq V^*(S_1)$.

**Proof:**

The proof is similar to that of Proposition 4.32. Let $S_i = \lambda_i \vdash_{\mathfrak{R}}^{V_i} \gamma_i$ (for $i = 1, 2$). Assume for the sake of contradiction that $v \in V^*(S_2) \setminus V^*(S_1)$. By definition of $V^*(S_i)$, $v$ is of sort loc, $v \in V(\gamma_2)$, $v \notin \text{alloc}(\lambda_2) \cup V_2$, and either $v \notin V(\gamma_1)$ or $v \in \text{alloc}(\gamma_1) \cup V_1$. First assume that $v \notin V(\gamma_1)$. Since $S_1$ contains no equality and $v \notin V^*(S_1)$, by Proposition 4.17 (4), the only rule that can introduce new variables to the right-hand side of a sequent is I. If Rule I is applied, then we must have $v = y_i\sigma$ for
some $i = 1, \dots, n$, with the notations used in the definition of the rule. Since all the rules in $\Re$ are P-rules, $\gamma_2$ necessarily contains an atom with root $v$ and $v \in \mathit{alloc}(\gamma_2)$. Since $v \notin \mathit{alloc}(\lambda_2)$, this entails by Definition 4.24 (1) that $S_2$ is an anti-axiom, which contradicts Condition 1 in Definition 4.31. Thus we necessarily have $v \in \mathcal{V}(\gamma_1)$. Now assume that $v \in \mathit{alloc}(\gamma_1) \cup V_1$. Then by Proposition 4.17 (7), the only rule that can remove a variable $v$ from $\mathit{alloc}(\gamma_1) \cup V_1$ is C, setting $x = v$. However, C replaces $x$ by another variable in the entire sequent, hence we have $x \notin \mathcal{V}(\gamma_2)$, thus $x$ cannot be $v$. $\square$

We show (Lemma 5.12) that the rules terminate in polynomial time if I is not applied. To this purpose we prove that both the depth of the proof tree and the number of branches are polynomial. We first introduce the following definition:

**Definition 5.5.** A path $S_0, \dots, S_n$ in a proof tree from $S$ to $S'$ is I-free if there is no application of the rule I on $S_0, \dots, S_{n-1}$. A descendant $S'$ of $S$ is called I-free if the path from $S$ to $S'$ is I-free.

The first goal is thus to prove that the length of all I-free paths is bounded. Then we will derive a bound on the total number of I-free descendants. To this purpose, we analyze the rules that can be applied on quasi-I-reducible sequents, and derive a number of easy but useful technical results.

**Proposition 5.6.** If a sequent $S$ is quasi-I-reducible then the only rules that can be applied on $S$ are I, W, C, or V. Moreover, for every I-free descendant $S'$ of $S$, the sequent $S'$ is quasi-I-reducible and $\mathcal{V} \mapsto (S) \cap \mathcal{V}(S') \subseteq \mathcal{V} \mapsto (S')$.

**Proof:**

The proof is by an inspection of the different rules. Note that if U applies on $(x \mapsto y * \phi) \wedge \xi \vdash_{\Re}^{V} \psi \wedge \top$ (with the notations of Definition 5.1), then, by Definition 4.31 (Condition 3), $\phi$ must contain an atom with the same root as $\mathit{root}(\psi) = x$, hence $(x \mapsto y * \phi)$ is heap-unsatisfiable and the sequent is an axiom. For the second part, it is clear that the only rule among W, C or V that can delete a variable $x$ from $\mathcal{V} \mapsto (S)$ is C, and this rule entirely removes $x$ from the sequent. $\square$

**Proposition 5.7.** The premises of U are quasi-I-reducible.

**Proof:**

We use the notations of the rule. By Definition 4.31 (Condition 3), $\gamma$ is a predicate atom with the same root as $p(t)$ and $\xi$ is a conjunction of disequations. Since the rules in $\Re$ are P-rules, every formula $\phi_i$ contains a points-to atom with root $\mathit{root}(p(t)) = \mathit{root}(\gamma)$. Thus the premises of U are necessarily quasi-I-reducible. $\square$

**Corollary 5.8.** There is at most one application of U along a path containing no I-reducible sequent.

**Proof:**

The result follows immediately from Propositions 5.6 and 5.7. $\square$

We eventually derive (Lemma 5.10) the result concerning the length of the I-free paths. To this aim we first introduce a new notation:
**Definition 5.9.** For every sequent $S = \lambda \vdash_{\mathfrak{R}}^{V} \gamma$, we denote by NbDisEq($S$) the number of disequations $x \not\approx y$ not occurring in $\lambda$ such that $x, y \in \mathcal{V}(S)$.

**Lemma 5.10.** The length of every I-free path from $S$ is at most $O(|S|^2)$.

**Proof:**

By Corollary 5.8, an I-free path contains at most one application of U. Rule R applies at most $card(V(S)^2)$ times, with highest priority, yielding an equality-free sequent, and afterward R can no longer be applied, since no inference rules introduce any equality to a sequent. Thus it is sufficient to prove the result for I-free paths containing no application of rules R or U. Let $S_1, \dots, S_n$ be a path with no application of R, U or I, where $S_1 = S$. Let $S_i = \phi_i \wedge \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i \wedge \zeta_i$. An inspection of the rules shows that we have $5 \cdot NbDisEq(S_i) + |S_i| > 5 \cdot NbDisEq(S_{i+1}) + |S_{i+1}|$, for all $i = 1, \dots, n$. Indeed, none of the considered rules can add new variables to $S_i$ by Proposition 4.17 (4) and Condition 4 of Definition 4.31, all the rules (except possibly C) decrease $|S_i|$ and W cannot remove disequations between variables occurring in predicate atoms. Rule C may add a disequation $x \not\approx y$ in $S_{i+1}$ (increasing the size by $4 = |S_i| \not\approx |S_{i+1}|$), but simultaneously removes the disequation $x \not\approx y$ from $NbDisEq(S_{i+1})$. Then the proof follows from the fact that $5 \cdot NbDisEq(S_1) + |S_1| = O(|S_1|^2)$. $\square$

To derive the result about the total number of I-free descendants, knowing the length of the paths is of course not sufficient: it is also necessary to estimate the number of such paths, which depends in particular on the number of applications of rule C. To this purpose, we prove the following result:

**Lemma 5.11.** Let $S$ be a sequent, with $card(V^*(S)) = \kappa$. The exhaustive application of C on $S$ yields at most $\kappa \cdot NbDisEq(S)^\kappa$ different branches.

**Proof:**

The proof is by induction on the pair $(\kappa, NbDisEq(S))$. By definition, every application of C on $S$ yields two sequents $S_1$ and $S_2$, where $S_1$ is obtained from $S$ by replacing a variable $x$ by $y$ and $S_2$ is obtained by adding the disequation $x \not\approx y$. By the application condition of the rule (Definition 4.31, Condition 4) necessarily $y \in V^*(S)$. Since $x$ is replaced by $y$ and $x$ is the root of an atom from the left-hand side of $S$, we must have $y \notin V^*(S_1)$, thus $card(V^*(S_1)) = \kappa - 1$. Now $NbDisEq(S_1) \le NbDisEq(S)$, $NbDisEq(S_2) = NbDisEq(S) - 1$ (since by Definition 4.31, Condition 4, $x, y \in V(S)$ and $x \not\approx y$ does not occur in $S$) and $V^*(S_2) = V^*(S)$, hence $card(V^*(S_2)) = \kappa$. By the induction hypothesis, the application of C generates at most $(\kappa - 1) \cdot NbDisEq(S_1)^{\kappa-1} \le \kappa \cdot NbDisEq(S)^{\kappa-1}$ branches on $S_1$ and $\kappa \cdot (NbDisEq(S)-1)^\kappa \le \kappa \cdot NbDisEq(S)^{\kappa-1} \cdot (NbDisEq(S)-1) = \kappa \cdot NbDisEq(S)^\kappa - \kappa \cdot NbDisEq(S)^{\kappa-1}$ branches on $S_2$. Thus the total number of branches is at most $\kappa \cdot NbDisEq(S)^\kappa$. $\square$

**Lemma 5.12.** Assume that $width(\mathfrak{R}) \le \kappa$, for some fixed $\kappa \in \mathbb{N}$ (i.e., that both the maximal arity of the symbols and the number of record fields are bounded by $\kappa$). The number of I-free descendants of any sequent $S$ is polynomial w.r.t. $|S| + |\mathfrak{R}|$ (but it is exponential w.r.t. $\kappa$).

**Proof:**

By Lemma 5.10, it is sufficient to prove that the total number of paths occurring in a proof tree with no application of I is polynomial w.r.t. $|S| + |\mathfrak{R}|$.
The rules R, W, V, E apply with the highest priority and yield only one branch, yielding a (unique) sequent $\phi \lambda \xi \vdash \psi \lambda \zeta$. If $\zeta \neq \top$, then by Definition 4.31, no other rule can be applied because these other rules apply only when the right-hand side is of the form $\psi \lambda \top$. Otherwise, the rule S may apply (possibly several times), and eventually transforms the sequent into sequents $\phi_i \lambda \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i \lambda \top$, where each $\psi_i$ is a predicate atom, $\phi = *_{i=1}^n \phi_i$ and $\psi = *_{i=1}^n \psi_i$ (we may have $\xi_i \neq \zeta$ since the rule may interleaved with applications of rule W).

If the considered sequent is not narrow, then by definition of the strategy (Condition 7 in Definition 4.31), there is at most one application of rule S; indeed, if several rule applications are possible then only the one that is selected is considered. We thus obtain at most $|S|$ branches, each ending with a narrow sequent (because $\psi_i$ is a predicate atom, thus $\phi_i \lambda \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i$ is necessarily narrow).

Now assume that $S$ is narrow and let $x_i$ be the root of $\psi_i$. We have $alloc(\psi_i) = \{x_i\}$, because $\psi_i$ is a predicate atom. Since $\phi_i * \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i$ is not an axiom, we have $x_i \in alloc(\phi_i)$. By definition of rule S, this entails that $x_i \in V_j$, for all $j \in \{1, \dots, i-1, i+1, \dots, n\}$. For S to be applied, it is only necessary to choose how to decompose the formula $\phi$ into $*_{i=1}^n \phi_i$. To this aim, we only have to associate each atom in $\phi$ with a formula $\phi_i$, hence to associate each variable $y \in alloc(\phi)$ (that are by definition the roots of the spatial atoms in $\phi$) to an index $i = 1, \dots, n$. By definition, the variable $x_i$ must be associated with index $i$, as otherwise we would have $x_i \notin alloc(\phi_i)$ and the premise $\phi_i * \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i$ would be an anti-axiom. We then arbitrarily choose the image of each variable occurring in $V^\dagger(S)$. Afterward, the image of the other variables are fixed inductively as follows. Let $y \in alloc(\phi)$ and assume that $y \notin V^\dagger(S) \cup \{x_1, \dots, x_n\}$. If $y$ occurs in some atom with root $y'$ in $\phi$ and $y'$ has already been associated with $i$, then we also associate $y$ with $i$. For the sake of contradiction, assume that $y$ is associated with an index $j \neq i$. By definition of rule S, this entails that $y \in V_i$, and since $\phi_i * \xi_i \vdash_{\mathfrak{R}}^{V_i} \psi_i$ is not an anti-axiom, we deduce that $y \in V(\psi_i)$, hence $y \in V(\psi) \setminus (alloc(\psi) \cup V) = V^\dagger(S)$, which contradicts our assumption (we cannot have $y \in V$ since $S$ would then be an axiom). Note that, for all variables $y \in alloc(\phi) \setminus \{x_1, \dots, x_n\}$, we have $x_i \to_{\phi}^* y$, for some $i = 1, \dots, n$, because otherwise $S$ would be an anti-axiom. Hence all such variables $y$ must be eventually associated with some index $i = 1, \dots, n$. Since $S$ is narrow, $card(V^\dagger(S)) \le \kappa$. Consequently, there exist at most $|S|^\kappa$ possible applications of rule S, each yielding $n \le |S|$ branches. We thus get a total of at most $|S|^{\kappa+1}$ branches.

Afterwards, rule U applies, yielding at most $|\mathfrak{R}|$ premises in each branch. Then C applies on each leaf sequent $S'$, and by Lemma 5.11 we get at most $|\mathfrak{R}| \cdot \text{NbDisEq}(S')^\kappa$ branches. The variables in $S'$ either occur in $S$ or are introduced by the rule U. Since each application of U introduces at most $\text{record}_{\max}(\mathfrak{R})$ variables, we get $\text{NbDisEq}(S') \le (|S| + \text{record}_{\max}(\mathfrak{R}))^2$. $\square$

We derive the main result of this section:

**Theorem 5.13.** The root sequent of every (possibly infinite) fully expanded proof tree is valid.

**Proof:**

Let $S$ be a non-valid sequent, with a counter-model $(s, h)$. By Lemma 4.23, $S$ is not an axiom, hence by definition of a fully expanded proof tree, it admits successors. By Lemmata 4.19 and 4.21, one of these successors must be non-valid and must admit a counter-model $(s, h')$, with $card(h') \le card(h)$, and if the rule that applies on $S$ is $S$, then $card(h') < card(h)$. Starting from the root of the tree, we thus obtain (if this root is not valid) an infinite path $S_0, \dots, S_n, \dots$, such that all the $S_i$ admit a
counter-model ($\mathfrak{s}_i, \mathfrak{h}_i$), $card(\mathfrak{h}_{i+1}) \leq card(\mathfrak{h}_i)$ and if $\mathfrak{S}$ is applied on $\mathcal{S}_i$ then $card(\mathfrak{h}_{i+1}) < card(\mathfrak{h}_i)$. Since $card(\mathfrak{h})$ is finite this entails that there exists $i \geq 0$ such that rule $\mathfrak{S}$ does not apply on $\mathcal{S}_j$, for all $j \geq i$. By Lemma 5.2, this entails that there exists $k$ such that $\mathfrak{I}$ does not apply on $\mathcal{S}_j$, for all $j \geq k$. Thus $\mathcal{S}_k$ admits an infinite number of $\mathfrak{I}$-free descendants, which contradicts Lemma 5.12. $\square$

## 5.2. Completeness

We now establish completeness, i.e., we prove that every valid sequent admits a fully expanded tree. To this aim, we prove that for every valid sequent, there exists a rule application yielding valid premises. Lemma 5.20 handles the case of rule $\mathfrak{S}$, and Lemma 5.21 handles all the other rules. We begin by establishing several preliminary results. First, we note that the truth value of a formula in a structure is not dependent on the *names* of the locations: these locations can be freely renamed, provided the relations between the variables are preserved, and provided allocated locations are not mapped to the same image. This result will be useful to construct copies of models when needed in forthcoming proofs. More formally, we introduce a notion of a *$\mathfrak{U}$-mapping* and state some conditions ensuring that the application of such $\mathfrak{U}$-mappings on a structure preserves the truth value of a formula.

**Definition 5.14.** A $\mathfrak{U}$-mapping is a function $\nu$ mapping every element of $\mathfrak{U}_s$ to an element of $\mathfrak{U}_s$. Let $\mathfrak{h}$ be a heap. If $\nu$ is injective on $dom(\mathfrak{h})$, then we denote by $\nu(\mathfrak{h})$ the heap with domain $\nu dom(\mathfrak{h})$, such that for all $\ell_0 \in dom(\mathfrak{h})$, with $\mathfrak{h}(\ell_0) = (\ell_1, \dots, \ell_n)$, we have $\nu(\mathfrak{h})(\nu(\ell_0)) = (\nu(\ell_1), \dots, \nu(\ell_n))$.

**Lemma 5.15.** Let $\lambda$ be a symbolic heap, let $(\mathfrak{s}, \mathfrak{h})$ be an $\mathfrak{R}$-model of $\lambda$ and let $\nu$ be a $\mathfrak{U}$-mapping that is injective on $\mathfrak{s}(\mathfrak{V}(\lambda)) \cup dom(\mathfrak{h})$. Then $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.

**Proof:**

The proof is by induction on the satisfiability relation. The result is established also for spatial formulas and pure formulas.

* If $\lambda$ is an equation $x \approx y$, then $\mathfrak{s}(x) = \mathfrak{s}(y)$, hence $\nu(\mathfrak{s}(x)) = \nu(\mathfrak{s}(y))$ and $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.

* If $\lambda$ is a disequation $x \not\approx y$, then $\mathfrak{s}(x) \neq \mathfrak{s}(y)$, and since $\nu$ is injective on $\mathfrak{s}(\mathfrak{V}(\lambda))$ we get $\nu(\mathfrak{s}(x)) \neq \nu(\mathfrak{s}(y))$ and $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.

* If $\lambda = y_0 \mapsto (y_1, \dots, y_n)$ then we must have $\mathfrak{h} = \{(\mathfrak{s}(y_0), \dots, \mathfrak{s}(y_n))\}$, which entails that $\nu(\mathfrak{h})$ is $\{(\nu(\mathfrak{s}(y_0)), \dots, \nu(\mathfrak{s}(y_n)))\}$ and that $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.

* If $\lambda = \phi \land \xi$ (or $\lambda = \phi \land \xi$) then we have $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi$ and $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \xi$. By the induction hypothesis, we get $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \phi$ and $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \xi$, thus $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.

* If $\lambda = \phi_1 * \phi_2$ then there exists disjoint heaps $\mathfrak{h}_i$ (for $i = 1, 2$) such that $\mathfrak{h} = \mathfrak{h}_1 \uplus \mathfrak{h}_2$ and $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \phi_i$. Since $\mathfrak{s}(\mathfrak{V}(\phi_i)) \cup dom(\mathfrak{h}_i) \subseteq \mathfrak{s}(\mathfrak{V}(\lambda)) \cup dom(\mathfrak{h})$, by the induction hypothesis we have $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h}_i)) \models_{\mathfrak{R}} \phi_i$ (for $i = 1, 2$). But $\nu(\mathfrak{h}_1)$ and $\nu(\mathfrak{h}_2)$ must be disjoint since $dom(\mathfrak{h}_1) \cap dom(\mathfrak{h}_2) = \emptyset$ and $\nu$ is injective, therefore $(\nu \circ \mathfrak{s}, \nu(\mathfrak{h})) \models_{\mathfrak{R}} \lambda$.
* If $\lambda$ is a predicate atom, then we have $\lambda \Leftarrow \mathfrak{R} \ \gamma$ and $(s', h) \models_{\mathfrak{R}} \gamma$, for some associate $s'$ of $s$ w.r.t. $V(\gamma) \setminus V(\lambda)$. Since the rules in $\mathfrak{R}$ are P-rules, for all variables $x \in V(\gamma) \setminus V(\lambda)$, we have $x \in \mathit{alloc}(\gamma)$ thus $s'(x) \in \mathit{dom}(h)$ by Lemma 4.2. This entails that $\nu$ is injective on $s'(V(\gamma)) \cup \mathit{dom}(h)$, and by the induction hypothesis we get $(\nu \circ s', \nu(h)) \models_{\mathfrak{R}} \xi$. Moreover, it is clear that $\nu(s')$ is an associate of $\nu(s)$ w.r.t. $V(\gamma) \setminus V(\lambda)$, thus $(\nu \circ s, \nu(h)) \models_{\mathfrak{R}} \lambda$. $\square$

This result entails that for every set $U$ that is sufficiently large, counter-models may always be re-named, so that all locations occur in $U$:

**Corollary 5.16.** Let $U$ be an infinite subset of $\mathfrak{U}_S$. Any non-valid and equality-free sequent $\lambda \vdash_{\mathfrak{R}}^V \gamma$ admits a counter-model $(s, h)$ such that $\mathit{dom}(h) \cup s(V_{1oc}) \subseteq U$.

**Proof:**

It suffices to consider any counter-model of $\gamma$ and apply a bijective $\mathfrak{U}$-mapping (or any $\mathfrak{U}$-mapping that is injective on $s(V(\lambda)) \cup \mathit{dom}(h))$ that maps all locations $\ell \in \mathfrak{U}_{1oc}$ to an element in $U$. $\square$

The first step toward establishing completeness is to show that rule S always applies (on a valid sequent) if the right-hand side of the sequent contains several spatial formulas (assuming that the rules of higher priority do not apply). This is essential because the strategy in Definition 4.31 forbids the application of the other rules in this case. The difficulty is that, of course, S cannot be applied arbitrarily: we are required to obtain valid premises. To this purpose we show that the heap decomposition of the left-hand side $(\phi_1 * \phi_2)$ matches that of the right-hand side $(\psi_1 * \psi_2)$. This will be proven thanks to the next lemma. Intuitively, this lemmas states that, under some additional conditions, if a structure $(s, h_1 \uplus h_2)$ validates a formula $\phi_1 * \phi_2$, then we may deduce that each structure $(s, h_i)$ validates $\phi_i$, when all the variables allocated by $\phi_i$ are in the domain of $h_i$.

**Lemma 5.17.** Let $\phi_i, \psi_i$ (for $i = 1, 2$) be spatial formulas, with $\mathit{alloc}(\psi_1 * \psi_2) \subseteq \mathit{alloc}(\phi_1 * \phi_2)$. Let $h_1$ and $h_2$ be disjoint heaps such that $(s, h_1 \uplus h_2) \models_{\mathfrak{R}} \phi_1 * \phi_2$ and $(s, h_i) \models_{\mathfrak{R}} \psi_i$, for $i = 1, 2$. If $(\mathit{dom}(h_1) \cup \mathit{dom}(h_2)) \cap s(V) \subseteq s(\mathit{alloc}(\phi_1 * \phi_2))$ and $s(\mathit{alloc}(\phi_i)) \subseteq \mathit{dom}(h_i)$ for $i = 1, 2$, then $(s, h_i) \models_{\mathfrak{R}} \phi_i$, for $i = 1, 2$.

**Proof:**

By definition, since $(s, h_1 \uplus h_2) \models_{\mathfrak{R}} \phi_1 * \phi_2$, there exist disjoint heaps $\hat{h}_1, \hat{h}_2$ such that $(s, \hat{h}_i) \models_{\mathfrak{R}} \phi_i$, for all $i = 1, 2$, and $h_1 \uplus h_2 = \hat{h}_1 \uplus \hat{h}_2$. We prove that $\hat{h}_i = h_i$ for $i = 1, 2$. Since $\hat{h}_1 \uplus \hat{h}_2 = h_1 \uplus h_2$ and $\hat{h}_1$ and $\hat{h}_2$ are disjoint, it is sufficient to prove that $\mathit{dom}(h_i) \subseteq \mathit{dom}(\hat{h}_i)$, for $i = 1, 2$. By symmetry, we prove the result for $i = 1$. Assume, for the sake of contradiction, that $\ell \in \mathit{dom}(h_1)$ and $\ell \notin \mathit{dom}(\hat{h}_1)$. By Proposition 4.6, since $(s, h_1) \models_{\mathfrak{R}} \psi_1$ and $\ell \in \mathit{dom}(h_1) \subseteq \mathit{ref}(h_1)$, there exists $y \in \mathit{alloc}(\psi_1)$ such that $s(y) \to_{\hat{h}_1}^* \ell$, thus there is a sequence of locations $\ell_0, \dots, \ell_n$ with $\ell_0 = s(y)$, $\ell = \ell_n$ and $\ell_i \to_{\hat{h}_1} \ell_{i+1}$, for all $i = 0, \dots, n-1$. Let $k$ be the smallest index such that $\ell_k \notin \mathit{dom}(\hat{h}_1)$. Note that $\ell_i \in \mathit{dom}(h_1)$, for all $i \le k$ and that $y \in \mathit{alloc}(\phi_1)$. Indeed, $y \in \mathit{alloc}(\psi_1) \subseteq \mathit{alloc}(\phi_1) \cup \mathit{alloc}(\phi_2)$ by the hypothesis of the lemma, and if $y \in \mathit{alloc}(\phi_2)$, then we get (again by the hypothesis of the lemma) $s(y) \in \mathit{dom}(h_2)$, which contradicts the fact that $\ell_0 = s(y) \in \mathit{dom}(h_1)$, as $h_1$ and $h_2$ are disjoint. By
Lemma 4.2, we deduce that $l_0 = s(y) \in \text{dom}(\hat{h}_1)$ since $y \in \text{alloc}(\phi_1)$ and $(s, \hat{h}_1) \models_{\mathfrak{R}} \phi_1$. Thus $k > 0$, and necessarily $l_k \in \text{ref}(\hat{h}_1)$ (since $l_{k-1} \in \text{dom}(\hat{h}_1)$, by minimality of $k$). We deduce that $l_k \in \text{ref}(\hat{h}_1) \setminus \text{dom}(\hat{h}_1)$. By Lemma 4.7, this entails that $l_k = s(x)$ for some $x \in \mathcal{V}(\phi_1)$, as $(s, \hat{h}_1) \models \phi_1$. By the hypothesis of the lemma, we may assume that $x \in \text{alloc}(\phi_1 * \phi_2)$, since $l_k \in \text{dom}(\hat{h}_1)$ and $(\text{dom}(\hat{h}_1) \cup \text{dom}(\hat{h}_2)) \cap s(\mathcal{V}) \subseteq s(\text{alloc}(\phi_1 * \phi_2))$. However, we cannot have $x \in \text{alloc}(\phi_1)$ because otherwise we would have $s(x) \in \text{dom}(\hat{h}_1)$ by Lemma 4.2, as $(s, \hat{h}_1) \models_{\mathfrak{R}} \phi_1$. We cannot have $x \in \text{alloc}(\phi_2)$ either, since otherwise we would have $s(x) \in \text{dom}(\hat{h}_2)$, as $s(\text{alloc}(\phi_2)) \subseteq \text{dom}(\hat{h}_2)$ by the hypothesis of the lemma, hence $s(x) \notin \text{dom}(\hat{h}_1)$ because $\hat{h}_1$ and $\hat{h}_2$ are disjoint. Thus we obtain a contradiction. □

We then derive the result about rule S. The main issue is that we have to take into account the fact that the strategy “blocks” some applications of S, if the sequent is not narrow (see Condition 5 in Definition 4.31). We show that blocked applications do not yield valid premises. To illustrate the difficulties that arise when applying S, we provide the examples below. The first one illustrates the importance of the fact that each predicate allocates at most one parameter.

**Example 5.18.** Consider the sequent $p(x, y) \Vdash_{\mathfrak{R}} q(x, y) * r(y)$, with the rules:

$$ \begin{array}{lclcl} p(x, y) & \Leftarrow & x \mapsto (y) * p'(y) & q(x, y) & \Leftarrow & x \mapsto (y) \\ p'(y) & \Leftarrow & y \mapsto () & r(y) & \Leftarrow & y \mapsto () \end{array} $$

Note that the rules of *p* are *not* P-rules, as both *x* and *y* are allocated by *p(x, y)*. Here, although the sequent is indeed valid, no application of *S* yields valid premises: to show that the sequent is valid, one has first to unfold *p(x, y)* once, before applying *S*. In our context, such a situation cannot arise as each predicate atom allocates only one of its parameters, namely its root. As we shall see, this entails that every decomposition of the right-hand side of the sequent necessarily corresponds to some (purely syntactic) decomposition of the left-hand side.

The next example illustrates the importance of determinism.

**Example 5.19.** Consider the sequent $S: p(x, y) * q(y) * p(z, y) \Vdash_{\mathfrak{R}} p'(x, y) * q'(z, y)$, with the rules:

$$ \begin{array}{lclcl} p(x, y) & \Leftarrow & x \mapsto (y) & q(y) & \Leftarrow & y \mapsto (z) * q(z) \\ q(y) & \Leftarrow & y \mapsto () & q(y) & \Leftarrow & y \mapsto (y) \\ p'(x, y) & \Leftarrow & x \mapsto (z) * p'(z, y) & q'(x, y) & \Leftarrow & x \mapsto (z) * q'(z, y) \\ p'(x, y) & \Leftarrow & x \mapsto (y) & q'(x, y) & \Leftarrow & x \mapsto (y) \\ p'(x, y) & \Leftarrow & x \mapsto () & q'(x, y) & \Leftarrow & x \mapsto (x) \end{array} $$

Intuitively, $q(y)$ denotes a list starting at $y$ and ending either with an empty tuple or with a loop on its last element, whereas $p'(x, y)$ (resp. $q'(x, y)$) denotes a list starting at $x$ and ending either with $y$ or with an empty tuple (resp. with a loop on the last element). These rules are not deterministic (for instance there is an overlap between the rules $p'(x, y) \Leftarrow x \mapsto (z) * p'(z, y)$ and $p'(x, y) \Leftarrow x \mapsto (y)$). Although the sequent *S* is valid, there is no application of *S* that yields valid premises. Indeed, none
of the sequents $p(x, y) * q(y) \vdash_{\mathfrak{R}}^\emptyset p'(x, y)$, or $q(y) * p(z, y) \vdash_{\mathfrak{R}}^\emptyset q'(z, y)$ are valid. Here $\mathcal{S}$ cannot be applied before the entire list $q(y)$ is unfolded, as the decision to group $q(y)$ with $p(x, y)$ or $p(y, z)$ cannot be made before the last cell in $q(y)$ is known. This would yield an infinite proof tree (with infinitely many branches). The fact that the rules are deterministic prevents such a behavior to occur.

**Lemma 5.20.** Let $\mathcal{S} : \phi \wedge \xi \vdash_{\mathfrak{R}}^V (\psi_1 * \psi_2) \wedge \top$ be a valid sequent where $\psi_i \neq \text{emp}$ for $i = 1, 2$ and $\xi$ is a conjunction of disequations. If $\mathcal{S}$ is not an axiom, then there exists an application of $\mathcal{S}$ with conclusion $\mathcal{S}$ for which all the premises are valid.

**Proof:**

To prove that $\mathcal{S}$ applies on $\mathcal{S}$, it is necessary to show that $\phi$ is of the form $\phi_1 * \phi_2$. However $\phi_i$ cannot be chosen arbitrarily, since the premises have to be valid. To construct $\phi_i$, we shall construct a model of $\phi$ of a particular form, get a decomposition of the heap of this model from the formula $\psi_1 * \psi_2$ on the right-hand side of the sequent, and use this decomposition to compute suitable formulas $\phi_1$ and $\phi_2$. We first notice that, since $\mathcal{S}$ is not an axiom, $\phi$ must be heap-satisfiable. Furthermore, since $\mathcal{S}$ is valid, it cannot be an anti-axiom by Lemma 4.27, thus $\text{alloc}(\psi_i) \subseteq \text{alloc}(\phi)$ for $i = 1, 2$. Since $\psi_i \neq \text{emp}$, this entails that $\text{alloc}(\phi)$ is not empty. Let $U_1, U_2$ be disjoint infinite subsets of $U_{1\text{loc}}$ and let $\mathfrak{s}$ be an injective store such that $\mathfrak{s}(\mathcal{V}) \cap U_i = \emptyset$, for $i = 1, 2$. Note that such $U_1, U_2$ and $\mathfrak{s}$ exist since $U_{\mathfrak{s}}$ is infinite, for all $\mathfrak{s} \in \mathcal{G}$. By Lemma 4.26 applied with $U = U_1$ and with any variable $x \in \text{alloc}(\phi)$, there exists an $\mathfrak{R}$-model $(\mathfrak{s}, \mathfrak{h})$ of $\phi$ such that $\text{dom}(\mathfrak{h}) \subseteq U_1 \cup \mathfrak{s}(\text{alloc}(\phi))$. Since $\mathfrak{s}$ is injective and $\xi$ is a conjunction of disequations, necessarily $\mathfrak{s} \models \xi$ (observe that $\xi$ contains no disequation of the form $u \not\approx u$ as otherwise $\mathcal{S}$ would be an axiom). If there exists $x \in \mathcal{V}$ such that $\mathfrak{s}(x) \in \text{dom}(\mathfrak{h})$, then since $\text{dom}(\mathfrak{h}) \subseteq U_1 \cup \mathfrak{s}(\text{alloc}(\phi))$ and $\mathfrak{s}(\mathcal{V}) \cap U_1 = \emptyset$, there must exist $x' \in \text{alloc}(\phi)$ such that $\mathfrak{s}(x) = \mathfrak{s}(x')$. Since $\mathfrak{s}$ is injective, necessarily $x = x'$, which entails that $\mathcal{S}$ is an axiom, contradicting the hypotheses of the lemma. We deduce that $\mathfrak{s}(\mathcal{V}) \cap \text{dom}(\mathfrak{h}) = \emptyset$. Since $\mathfrak{s}$ is injective, it is injective on $\mathcal{V}$, as otherwise $\mathcal{V}$ would contain two occurrences of the same variable and $\mathcal{S}$ would be an axiom. Because $\mathcal{S}$ is valid, we deduce that $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} (\psi_1 * \psi_2)$, hence there exist disjoint heaps $\mathfrak{h}_1$ and $\mathfrak{h}_2$ such that $\mathfrak{h} = \mathfrak{h}_1 \uplus \mathfrak{h}_2$ and $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \psi_i$, for $i = 1, 2$. Let $\phi_i$ be the separating conjunction of all the spatial atoms $\alpha$ occurring in $\phi$ such that $\mathfrak{s}(\text{alloc}(\alpha)) \subseteq \text{dom}(\mathfrak{h}_i)$. By Lemma 4.2, $\mathfrak{s}(\text{alloc}(\phi)) \subseteq \text{dom}(\mathfrak{h}) = \text{dom}(\mathfrak{h}_1) \cup \text{dom}(\mathfrak{h}_2)$, hence every atom $\alpha$ occurs in either $\phi_1$ or $\phi_2$, and since $\mathfrak{h}_1$ and $\mathfrak{h}_2$ are disjoint, no atom $\alpha$ can occur both in $\phi_1$ and $\phi_2$. Therefore, $\phi = \phi_1 * \phi_2$.

We now prove that $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \phi_i$ for $i = 1, 2$. To this aim we use Lemma 5.17, thus we verify that all the hypotheses of the lemma are satisfied. Since $\text{dom}(\mathfrak{h}) \subseteq U_1 \cup \mathfrak{s}(\text{alloc}(\phi))$ and $U_1 \cap \mathfrak{s}(\mathcal{V}) = \emptyset$, we have $\text{dom}(\mathfrak{h}) \cap \mathfrak{s}(\mathcal{V}) \subseteq \mathfrak{s}(\text{alloc}(\phi))$, i.e. $(\text{dom}(\mathfrak{h}_1) \cup \text{dom}(\mathfrak{h}_2)) \cap \mathfrak{s}(\mathcal{V}) = \mathfrak{s}(\text{alloc}(\phi_1 * \phi_2))$. Furthermore, $\mathfrak{s}(\text{alloc}(\phi_i)) \subseteq \text{dom}(\mathfrak{h}_i)$ for $i = 1, 2$ by definition of $\phi_i$, $(\mathfrak{s}, \mathfrak{h}_1 \uplus \mathfrak{h}_2) = (\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi = \phi_1 * \phi_2$, $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \psi_i$ (for all $i = 1, 2$) and $\text{alloc}(\psi_1 * \psi_2) \subseteq \text{alloc}(\phi_1 * \phi_2)$. By Lemma 5.17, we deduce that $(\mathfrak{s}, \mathfrak{h}_i) \models_{\mathfrak{R}} \phi_i$ for $i = 1, 2$.

It is clear that there is an application of $\mathcal{S}$ on $\mathcal{S} = (\phi_1 * \phi_2) \wedge \xi \models_{\mathfrak{R}} (\psi_1 * \psi_2) \wedge \top$ yielding the premises $\phi_i \wedge \xi \vdash_{\mathfrak{R}}^V \psi_i$ for $i = 1, 2$, where $V_i = \mathcal{V} \cup \text{alloc}(\phi_{3-i})$. There remains to prove that these premises are valid and that the application of the rule is allowed by the strategy. Assume that one of these premises, say $\phi_1 \wedge \xi \vdash_{\mathfrak{R}}^V \psi_1$, is not valid. By Corollary 5.16 applied with $U = U_2$, $\phi_1 \wedge \xi \vdash_{\mathfrak{R}}^V \psi_1$ admits a counter-model $(\mathfrak{s}', \mathfrak{h}')$, where $\text{dom}(\mathfrak{h}')_1 \cup \mathfrak{s}'(\mathcal{V}_{1\text{loc}}) \subseteq U_2$. By construction we have $\mathfrak{s}'(V_1) \cap \text{dom}(\mathfrak{h}')_1 = \emptyset$, thus $\mathfrak{s}'(\mathcal{V}) \cap \text{dom}(\mathfrak{h}')_1 = \emptyset$ since $\mathcal{V} \subseteq V_1$. Moreover, $\mathfrak{s}'$ is injective
on $V_1 = V \cup \text{alloc}(\phi_2)$. By Lemma 4.26, $\phi_2$ therefore admits a model $(s', \mathfrak{h}_2')$ with $\text{dom}(\mathfrak{h}_2') \subseteq U_1 \cup s'(\text{alloc}(\phi_2))$. We show that $\mathfrak{h}_1'$ and $\mathfrak{h}_2'$ are disjoint. Assume for the sake of contradiction that $\ell \in \text{dom}(\mathfrak{h}_1') \cap \text{dom}(\mathfrak{h}_2')$. Since $U_1 \cap U_2 = \emptyset$, we have $\text{dom}(\mathfrak{h}_1') \cap \text{dom}(\mathfrak{h}_2') \subseteq s'(\text{alloc}(\phi_2))$, thus $\ell \in s'(\text{alloc}(\phi_2))$. But since $s'(V_1) \cap \text{dom}(\mathfrak{h}_1') = \emptyset$ and $\text{alloc}(\phi_2) \subseteq V_1$ we also have $\ell \notin s'(\text{alloc}(\phi_2))$, a contradiction. Thus $\mathfrak{h}_1'$ and $\mathfrak{h}_2'$ are disjoint and we have $(s', \mathfrak{h}_1' \uplus \mathfrak{h}_2') \models_{\mathfrak{R}} (\phi_1 * \phi_2) \wedge \xi = \phi \wedge \xi$. If $s'(V) \cap \text{dom}(\mathfrak{h}_2')$ contains a location $\ell$ then since $U_1 \cap U_2 = \emptyset$, necessarily $\ell = s'(x)$, for some $x \in \text{alloc}(\phi_2)$, and since $s'$ is injective on $V_1 = V \cup \text{alloc}(\phi_2)$ and $\ell \in s'(V)$, necessarily, $x \in V$ and $S$ is an axiom, which contradicts the hypotheses of the lemma. We deduce that $s'(V) \cap \text{dom}(\mathfrak{h}_2') = \emptyset$, and since $s'(V) \cap \text{dom}(\mathfrak{h}_1') = \emptyset$, that $s'(V) \cap \text{dom}(\mathfrak{h}_1' \uplus \mathfrak{h}_2') = \emptyset$. Furthermore, by construction, $s'$ is injective on $V$. Since $S$ is valid, this entails that $(s', \mathfrak{h}_1' \uplus \mathfrak{h}_2') \models_{\mathfrak{R}} (\psi_1 * \psi_2)$, hence $\mathfrak{h}_1' \uplus \mathfrak{h}_2' = \mathfrak{h}_1'' \uplus \mathfrak{h}_2''$, where $(s', \mathfrak{h}_i'') \models_{\mathfrak{R}} \psi_i$. By Lemma 3.6, since $(s', \mathfrak{h}_2'') \models_{\mathfrak{R}} \psi_2$ and $\mathfrak{R}$ is deterministic, we get $\mathfrak{h}_2'' = \mathfrak{h}_2''$, and therefore $\mathfrak{h}_1'' = \mathfrak{h}_1'$, thus $(s', \mathfrak{h}_1') \models_{\mathfrak{R}} \psi_1$. This contradicts the fact that $(s', \mathfrak{h}_1')$ is a counter-model of $\phi_1 \wedge \xi \vdash_{\mathfrak{R}}^{V_2} \psi_1$.

If $S$ is narrow, then the proof is completed, since all the applications of rule $S$ are considered by the strategy in this case. If $S$ is not narrow, then the application of the rule may be blocked by Condition 7 of Definition 4.31. In this case, this means that there exist $\phi_1'$, $\phi_2'$ such that $\phi = \phi_1' * \phi_2'$ and $\phi_1' \wedge \xi \vdash_{\mathfrak{R}}^{V_1'} \psi_1$ is valid, where $V_1' = V \cup \text{alloc}(\phi_2')$. We assume that the other premise, $\phi_2' \wedge \xi \vdash_{\mathfrak{R}}^{V_2'} \psi_2$ (with $V_2' = V \cup \text{alloc}(\phi_1')$) is not valid, and we derive a contradiction. By Corollary 5.16, this premise admits a counter-model $(s'', \mathfrak{h}_2'')$ such that $\text{dom}(\mathfrak{h}_2'') \cup s''(V_{1\text{oc}}) \subseteq U_1$. We have $(s'', \mathfrak{h}_2'') \models_{\mathfrak{R}} \phi_2'$, $s'' \models \xi$, $s''(V_2') \cap \text{dom}(\mathfrak{h}_2'') = \emptyset$, $s''$ is injective on $V_2'$ and $(s, \mathfrak{h}_2'') \not\models_{\mathfrak{R}} \psi_2$. By Lemma 4.26, $\phi_1'$ admits a model $(s'', \mathfrak{h}_1'')$ such that $\text{dom}(\mathfrak{h}_1'') \subseteq U_2 \cup s''(\text{alloc}(\phi_1'))$.

Note that the heaps $\mathfrak{h}_1''$ and $\mathfrak{h}_2''$ are disjoint. Indeed, if $\ell \in \text{dom}(\mathfrak{h}_1'') \cap \text{dom}(\mathfrak{h}_2'')$ then, since $\text{dom}(\mathfrak{h}_1'') \subseteq U_2 \cup s''(\text{alloc}(\phi_1'))$ and $\text{dom}(\mathfrak{h}_2'') \cup s''(V_{1\text{oc}}) \subseteq U_1$, with $U_1 \cap U_2 = \emptyset$, we obtain $\ell \in s''(\text{alloc}(\phi_1'))$, so that $\ell \in s''(V_2')$, contradicting the fact that $s''(V_2') \cap \text{dom}(\mathfrak{h}_2'') = \emptyset$.

We prove that $s''$ is injective on $V_1'$, and that $\text{dom}(\mathfrak{h}_1'') \cap s''(V_1) = \emptyset$, which entails that $(s'', \mathfrak{h}_1'') \models_{\mathfrak{R}} \psi_1$, since $\phi_1' \wedge \xi \vdash_{\mathfrak{R}}^{V_1'} \psi_1$ is valid. If there exist $x_1, x_2$ such that $\{x_1, x_2\} \subseteq_m V_1' = V \cup \text{alloc}(\phi_2')$ and $s''(x_1) = s''(x_2)$ then, as $s''$ is injective on $V_2' = V \cup \text{alloc}(\phi_1')$, necessarily at least one of the variables $x_1, x_2$ say $x_1$ is in $\text{alloc}(\phi_2')$. As $(s'', \mathfrak{h}_2'') \models \phi_2'$, we get $s''(x_1) \in \text{dom}(\mathfrak{h}_2'')$ (by Lemma 4.2), and $\{x_1, x_2\} \not\subseteq_m \text{alloc}(\phi_2')$ (by Corollary 4.3). This entails that $s''(x_1) \notin s''(V_2')$ (as $s''(V_2') \cap \text{dom}(\mathfrak{h}_2'') = \emptyset$) and $x_2 \in V \subseteq V_2'$, yielding a contradiction, since $s''(x_1) = s''(x_2)$. Now assume that there exists $y \in V_1' = V \cup \text{alloc}(\phi_2')$ such that $s''(y) \in \text{dom}(\mathfrak{h}_1'')$. As $\text{dom}(\mathfrak{h}_1'') \subseteq U_2 \cup s''(\text{alloc}(\phi_1'))$ and $\text{dom}(\mathfrak{h}_2'') \cup s''(V_{1\text{oc}}) \subseteq U_1$, we get $s''(y) \in s''(\text{alloc}(\phi_1'))$, i.e., there exists $y' \in \text{alloc}(\phi_1')$ such that $s''(y) = s''(y')$. If $y \in V$, then $\{y, y'\} \subseteq_m V_2'$, contradicting the fact that $s''$ is injective on $V_2'$. Thus $y \in \text{alloc}(\phi_2')$, so that $s(y) \in \text{dom}(\mathfrak{h}_2'')$ (by Lemma 4.2), contradicting the fact that $\mathfrak{h}_1''$ and $\mathfrak{h}_2''$ are disjoint.

Thus $(s'', \mathfrak{h}_1'' \uplus \mathfrak{h}_2'') \models_{\mathfrak{R}} \phi_1' * \phi_2' = \phi$. As $s'' \models \xi$ and $s''(V) \cap \text{dom}(\mathfrak{h}_i'') \subseteq s(V_i) \cap \text{dom}(\mathfrak{h}_i'')$ is empty, $s''$ is injective on $V$, and $S$ is valid, we get $(s'', \mathfrak{h}_1'' \uplus \mathfrak{h}_2'') \models_{\mathfrak{R}} \psi_1 * \psi_2$. Therefore, there exist disjoint heaps $\hat{\mathfrak{h}}_i''$ (for $i = 1, 2$), such that $(s'', \hat{\mathfrak{h}}_i'') \models_{\mathfrak{R}} \psi_i$ and $\mathfrak{h}_1'' \uplus \mathfrak{h}_2'' = \mathfrak{h}_1'' \uplus \mathfrak{h}_2''$. By Lemma 3.6, since $(s'', \mathfrak{h}_1'') \models_{\mathfrak{R}} \psi_1$, we deduce that $\mathfrak{h}_1'' = \hat{\mathfrak{h}}_1''$, thus $\mathfrak{h}_2'' = \hat{\mathfrak{h}}_2''$, hence and $(s'', \mathfrak{h}_2'') \models_{\mathfrak{R}} \psi_2$, which contradicts the fact that $(s'', \mathfrak{h}_2'')$ is a counter-model of $\phi_2' \wedge \xi \vdash_{\mathfrak{R}}^{V_2'} \psi_2$. $\square$
We handle the case of the other rules, more precisely we show that there is always an inference rule that applies on a valid sequent (if it is not an axiom):

**Lemma 5.21.** For any valid sequent $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ that is not an axiom, there exists an application of the inference rules that yields valid premises.

**Proof:**

Since $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ is not an axiom, $\phi$ is heap-satisfiable, $V \cap \text{alloc}(\phi) = \emptyset$ and $V$ contains at most one occurrence of each variable. Note that if an invertible rule applies on $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ then the result holds, since the premises are necessarily valid. Thus we may assume that $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ is irreducible by all invertible rules, hence (by Lemma 4.19) by all the rules except S.

Let $\mathfrak{s}$ be an injective store such that the set $U = \mathfrak{U}_{\text{loc}} \setminus \mathfrak{s}(V)$ is infinite. If $\phi \neq \text{emp}$, then $\phi$ contains at least one variable of sort $\text{loc}$, and by Lemma 4.26, we deduce that $\phi$ admits a model $(\mathfrak{s}, \mathfrak{h})$ such that $\text{dom}(\mathfrak{h}) \subseteq U \cup \mathfrak{s}(\text{alloc}(\phi))$. If $\phi = \text{emp}$ then the same property trivially holds, with $\mathfrak{h} = \emptyset$. Note in particular that the assertion $\text{dom}(\mathfrak{h}) \subseteq U \cup \mathfrak{s}(\text{alloc}(\phi))$ entails that $\mathfrak{s}(V) \cap \text{dom}(\mathfrak{h}) = \emptyset$ since $\mathfrak{s}(V) \cap U = \emptyset$, $V \cap \text{alloc}(\phi) = \emptyset$ and $\mathfrak{s}$ is injective.

If $\xi$ contains an equation then rule R applies, which contradicts our assumption that the sequent is irreducible by all invertible rules; thus $\xi$ is a conjunction of disequations. Furthermore, none of these disequations may be of the form $x \not\approx x$ because otherwise $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ would be an axiom. This entails that $\mathfrak{s} \models \xi$. Since $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ is valid, $\mathfrak{s}(V) \cap \text{dom}(\mathfrak{h}) = \emptyset$ and $\mathfrak{s}$ is injective (hence injective on $V$ because $V$ contains at most one occurrence of each variable), we deduce that

$$ (\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \psi \lambda \zeta. \quad (\dagger) $$

Assume that $\zeta$ contains an equation $x \approx y$. If $x = y$ then Rule E applies, and otherwise, we necessarily have $\mathfrak{s}(x) \neq \mathfrak{s}(y)$, hence $(\mathfrak{s}, \mathfrak{h}) \not\models_{\mathfrak{R}} \psi \lambda \zeta$ which contradicts (†). Thus $\zeta$ contains no equation. Now assume that $\zeta$ contains a disequation $x \not\approx y$. If $\{x, y\} \subseteq C$ (i.e., both $x$ and $y$ are constants) or $\{x, y\} \subseteq_m \text{alloc}(\phi) \cup V$ then $\phi \lambda \xi \triangleright_V x \not\approx y$, and E applies, which is impossible by hypothesis. If $x = y$ then $x \not\approx y$ is unsatisfiable, which contradicts (†). Let $\mathfrak{s}'$ be a store verifying $\mathfrak{s}'(x) = \mathfrak{s}'(y)$, that maps all other variables to pairwise distinct elements of the appropriate sort, also distinct from $\mathfrak{s}(x)$, and such that $U' = \mathfrak{U}_{\text{loc}} \setminus \mathfrak{s}'(V)$ is infinite. Such a store exists since $\mathfrak{U}_{\text{loc}}$ is infinite and $\{x, y\} \not\subseteq C$. If $\mathfrak{s}' \not\models \xi$, then since $\xi$ contains no equation, $x \not\approx y$ must occur in $\xi$. Then the rule E applies, which contradicts our assumption that the sequent is irreducible by all invertible rules. Thus $\mathfrak{s}' \models \xi$. Since $\{x, y\} \notsubseteq_m \text{alloc}(\phi)$, $\mathfrak{s}'$ is injective on $\text{alloc}(\phi)$. By Lemma 4.26, we deduce that $\phi$ admits a model of the form $(\mathfrak{s}', \mathfrak{h}')$ with $\text{dom}(\mathfrak{h}') \subseteq U' \cup \mathfrak{s}'(\text{alloc}(\phi))$. If $\mathfrak{s}'(V) \cap \text{dom}(\mathfrak{h}')$ contains a location $\ell$, then $\ell = \mathfrak{s}'(z) = \mathfrak{s}'(z')$, for some $z \in \text{alloc}(\phi)$ and $z' \in V$. Since $\text{alloc}(\phi) \cap V = \emptyset$ and $\mathfrak{s}'$ is injective on all pair of variables except on $\{x, y\}$, necessarily we have either $x = z$ and $y = z'$, or $x = z'$ and $y = z$, which means that $\{x, y\} \subseteq_m \text{alloc}(\phi) \cup V$, hence E applies, contradicting our assumption that the sequent is irreducible by all invertible rules. We deduce that $\mathfrak{s}'(V) \cap \text{dom}(\mathfrak{h}') = \emptyset$. Since $\{x, y\} \notsubseteq_m \mathfrak{s}'$ is necessarily injective on $V$. As $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ is valid, we deduce that $(\mathfrak{s}', \mathfrak{h}') \models_{\mathfrak{R}} \psi \lambda \zeta$ hence $\mathfrak{s}'(x) \neq \mathfrak{s}'(y)$, which contradicts the definition of $\mathfrak{s}'$. Therefore, $\zeta = \top$.

If $\psi = \text{emp}$ then necessarily $\phi = \text{emp}$, since otherwise by Corollary 4.4 we would have $\mathfrak{h} \neq \emptyset$, which contradicts (†). Hence in this case, $\phi \lambda \xi \vdash_{\mathfrak{R}}^{V} \psi \lambda \zeta$ is of the form $\text{emp} \lambda \xi \vdash_{\mathfrak{R}}^{V} \text{emp}$ and is an axiom.
If $\psi$ is of the form $\psi_1 * \psi_2$, where $\psi_i \neq \text{emp}$ for $i = 1, 2$, then the proof follows from Lemma 5.20. Thus, we may assume that $\psi$ is a spatial atom. Let $x$ be the root of $\psi$. If $x \notin \text{roots}(\phi)$, then we have $(\mathfrak{s}, \mathfrak{h}) \not\models_{\mathfrak{R}} \psi$ by Lemma 4.2, which contradicts (†). Therefore, $\phi$ contains a spatial atom with root $x$. If this spatial atom is a predicate atom then $\mathfrak{U}$ can be applied. Now assume that $\phi$ contains a points-to atom $x \mapsto (y_1, \dots, y_n)$, i.e., is of the form $x \mapsto (y_1, \dots, y_n) * \phi'$ (modulo AC). Since $\psi$ is a spatial atom with root $x$, there are two cases to consider:

1. $\psi$ is of the form $x \mapsto (y'_1, \dots, y'_n)$. We have $\mathfrak{h} = \{(\mathfrak{s}(x), \mathfrak{s}(y_1), \dots, \mathfrak{s}(y_n))\} \uplus \mathfrak{h}'$, where $\mathfrak{h}'$ is a heap such that $(\mathfrak{s}, \mathfrak{h}') \models_{\mathfrak{R}} \phi'$ and $\mathfrak{s}(x) \notin \text{dom}(\mathfrak{h}')$. By (†), we have $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \psi$, thus $\mathfrak{h} = \{(\mathfrak{s}(x), \mathfrak{s}(y'_1), \dots, \mathfrak{s}(y'_n))\}$. This entails that $\mathfrak{h}' = \emptyset$ (hence $\phi' = \text{emp}$ by Corollary 4.4), and that $\mathfrak{s}(y_i) = \mathfrak{s}(y'_i)$ for all $i = 1, \dots, n$. Since $\mathfrak{s}$ is injective, we have $y_i = y'_i$ for all $i = 1, \dots, n$. Therefore, $\psi = \phi$, and $\phi \wedge \xi \vdash_{\mathfrak{R}} \psi \wedge \zeta$ is an axiom (because $\zeta = \top$), which contradicts the hypothesis of the lemma.

2. $\psi$ is a predicate atom. By (†), we have $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \psi$ and by definition there exists a formula $\gamma'$ such that $\psi \Leftarrow_{\mathfrak{R}} \gamma'$, where $(\mathfrak{s}', \mathfrak{h}) \models_{\mathfrak{R}} \gamma'$ for some associate $\mathfrak{s}'$ of $\mathfrak{s}$ w.r.t. $\mathcal{V}(\gamma') \setminus \mathcal{V}(\psi)$, and in particular we have $\mathfrak{s}(x) = \mathfrak{s}'(x)$. As the rules in $\mathfrak{R}$ are P-rules, $\gamma'$ is of the form $(x \mapsto (u_1, \dots, u_m) * \psi') \wedge \zeta'$, with $\mathcal{V}(\gamma') \subseteq \mathcal{V}(\psi) \cup \{u_1, \dots, u_m\}$, and we have $\mathfrak{h}(\mathfrak{s}(x)) = \mathfrak{h}(\mathfrak{s}'(x)) = (\mathfrak{s}'(u_1), \dots, \mathfrak{s}'(u_m))$. Since $\phi$ contains a points-to atom $x \mapsto (y_1, \dots, y_n)$ and $(\mathfrak{s}, \mathfrak{h}) \models_{\mathfrak{R}} \phi$, necessarily $\mathfrak{h}(\mathfrak{s}(x)) = (\mathfrak{s}(y_1), \dots, \mathfrak{s}(y_n))$. Consequently $n = m$ and $\mathfrak{s}(y_i) = \mathfrak{s}'(u_i)$ for all $i = 1, \dots, n$. Let $\sigma$ be the substitution mapping every variable $u_i$ not occurring in $\mathcal{V}(\psi)$ to $y_i$. Note that $\sigma$ is well-defined: if $u_i = u_j$ then $\mathfrak{s}(y_i) = \mathfrak{s}(y_j)$ and $y_i = y_j$ since $\mathfrak{s}$ is injective. It is straightforward to check that $\mathfrak{s}''(z) = \mathfrak{s}(z\sigma)$ for all variables $z \in \mathcal{V}$, using the definition of $\sigma$ and the fact that $\mathfrak{s}'$ and $\mathfrak{s}$ coincide on all variables not occurring in $u_1, \dots, u_n$. If I applies with this substitution $\sigma$ then the proof is completed. Otherwise, we must have $\phi \wedge \xi \nvDash_V \zeta'\sigma$, i.e., $\zeta'$ must contain a disequation $u' \not\approx v'$ such that $\phi \wedge \xi \nvDash_V u'\sigma \not\approx v'\sigma$. Note that this entails that $u'\sigma$ and $v'\sigma$ cannot both be constants. Consider a store $\mathfrak{s}''$ verifying $\mathfrak{s}''(u'\sigma) = \mathfrak{s}''(v'\sigma)$, and mapping all other variables to pairwise distinct elements of the appropriate sort. We may assume that $\mathfrak{s}''$ is chosen in such a way that the set $U' = \mathfrak{U} \setminus \mathfrak{s}''(\mathcal{V})$ is infinite. By definition, $\mathfrak{s}'' \not\models \zeta'\sigma$, and since $\phi \wedge \xi \nvDash_V u'\sigma \not\approx v'\sigma$, we have $\{u'\sigma, v'\sigma\} \not\subseteq_m V \cup \text{alloc}(\phi)$, thus $\mathfrak{s}''$ is injective on $\text{alloc}(\phi) \cup V$ and $\mathfrak{s}'' \models \xi$ (since $\xi$ is a conjunction of disequations not containing $u'\sigma \not\approx v'\sigma$). By Lemma 4.26, $\phi$ admits a model $(\mathfrak{s}'', \mathfrak{h}'')$ such that $\text{dom}(\mathfrak{h}'') \subseteq U'' \cup \mathfrak{s}''(\text{alloc}(\phi))$. This entails that $\mathfrak{s}''(V) \cap \text{dom}(\mathfrak{h}'') = \emptyset$. Since $\mathfrak{s}''$ is injective on $V$ and $\phi \wedge \xi \vdash_{\mathfrak{R}} \psi \wedge \zeta$ is valid, we deduce that $(\mathfrak{s}''(x), \mathfrak{h}'') \models_{\mathfrak{R}} \psi$, thus $\psi \Leftarrow_{\mathfrak{R}} \gamma''$, where $(\hat{\mathfrak{s}}, \mathfrak{h}'') \models_{\mathfrak{R}} \gamma''$, for some formula $\gamma''$ and associate $\hat{\mathfrak{s}}$ of $\mathfrak{s}''$ w.r.t. $\mathcal{V}(\gamma'') \setminus \mathcal{V}(\psi)$. Since the rules in $\mathfrak{R}$ are P-rules, $\gamma''$ is of the form $(x \mapsto (u'_1, \dots, u'_k) * \psi'') \wedge \zeta''$, and we have $\mathfrak{h}''(\mathfrak{s}''(x)) = (\hat{\mathfrak{s}}(u'_1), \dots, \hat{\mathfrak{s}}(u'_k))$. We may assume, by renaming, that $\{u'_1, \dots, u'_k\} \cap \{u_1, \dots, u_m\} \subseteq \mathcal{V}(\psi)$. Since $\phi$ contains a points-to atom $x \mapsto (y_1, \dots, y_n)$ and $(\mathfrak{s}''(x), \mathfrak{h}'') \models_{\mathfrak{R}} \phi$, necessarily $\mathfrak{h}''(\mathfrak{s}''(x)) = (\mathfrak{s}''(y_1), \dots, \mathfrak{s}''(y_n))$, and thus we must have $k = n = m$ and for all $i = 1, \dots, n$, $\mathfrak{s}''(y_i) = \hat{\mathfrak{s}}(u'_i)$. Let $\sigma'$ be the substitution mapping every variable $u'_i$ not occurring in $\mathcal{V}(\psi)$ to the first variable $y_j$ in $y_1, \dots, y_n$ such that $\mathfrak{s}''(y_j) = \hat{\mathfrak{s}}(u'_i)$, and let $\theta$ be the substitution mapping every variable $y_i$ to $y_j$, where $j$ is the smallest index in $1, \dots, n$ such that $\mathfrak{s}'' \models y_i \approx y_j$. Let $\hat{\sigma} = \sigma \cup \sigma'$ and $\theta' = \hat{\sigma}\theta$; note that $\hat{\sigma}$ is well-defined since $\text{dom}(\sigma) \cap \text{dom}(\sigma') = \emptyset$, as $\{u'_1, \dots, u'_k\} \cap \{u_1, \dots, u_m\} \subseteq \mathcal{V}(\psi)$. By
construction, $\theta'$ is a unifier of $(u_1, \dots, u_n)$ and $(u'_1, \dots, u'_n)$. Since $\Re$ is loc-deterministic, one of the two formulas $\zeta'$ or $\zeta''$ contains a disequation $v \not\approx w$ with $v\theta' = w\theta'$ and $v, w \in V_{\text{loc}}$. Note that $v\hat{\sigma} \neq w\hat{\sigma}$ since otherwise $\zeta'\sigma$ or $\zeta''\sigma'$ would be unsatisfiable. We show that $v \not\approx w$ occurs in $\zeta'$. Assume, for the sake of contradiction, that $v \not\approx w$ occurs in $\zeta''$. Then $v\hat{\sigma} = v\sigma'$ and $w\hat{\sigma} = w\sigma'$. By definition of $\sigma'$ and $\theta'$, we have $z\sigma' = z\theta'$ for all $z \in \text{dom}(\sigma')$, thus we get $v\sigma' = w\sigma'$, hence (by definition of $\sigma'$) $\hat{s}(v) = \hat{s}(w)$, which contradicts the fact that $(\hat{s}, \hat{h}'') \models_{\Re} \gamma'' = (x \mapsto (u'_1, \dots, u'_k) * \psi'') \wedge \zeta''$. Thus necessarily $v \not\approx w$ occurs in $\zeta'$ and we have $v\hat{\sigma} = v\sigma$ and $w\hat{\sigma} = w\sigma$. As all rules are P-rules, necessarily at least one of the two variables $v, w$ (say $v$) is an existential variable, and we must have $v \in \text{alloc}(\psi')$. Since $(s', h) \models_{\Re} \gamma' = (x \mapsto (u_1, \dots, u_m) * \psi') \wedge \zeta'$, we deduce by Lemma 4.2 that $s'(v) \in \text{dom}(h)$, hence $s(v\sigma) \in \text{dom}(h)$. By definition of $(s, h)$, this entails that $s(v\sigma) \in s(\text{alloc}(\phi))$, and since $s$ is injective we get $v\sigma \in \text{alloc}(\phi)$.

Assume that $w\sigma \in \text{alloc}(\phi)$. Then $\text{alloc}(\phi)$ contains spatial atoms with respective roots $w\sigma$ and $v\sigma$. These atoms must be distinct since $v\sigma \neq w\sigma$. By Lemma 4.2 these locations are allocated in disjoint part of the heap $h''$, hence necessarily $s''(w\sigma) \neq s''(v\sigma)$. We deduce that $v\theta' \neq w\theta'$, which contradicts our assumption. Thus $w\sigma \notin \text{alloc}(\phi)$, and since $\phi \wedge \xi \vdash_{\Re}^V \psi \wedge \zeta$ cannot be an anti-axiom, necessarily $w\sigma \in V(\psi)$. We also have $w\sigma \notin V$, since $\text{dom}(h'') \cap s''(V) = \emptyset$. We may assume that the sequent $\phi \wedge \xi \vdash_{\Re}^V \psi \wedge \zeta$ is irreducible by the rule C, so that, as $\psi$ is a predicate atom, $\xi$ contains a disequation $v\sigma \not\approx w\sigma$ (since $v\sigma \in \text{alloc}(\phi)$, $w\sigma \in V(\psi) \setminus (\text{alloc}(\phi) \cup V)$). But then we have $s'' \not\models \xi$, contradicting the definition of $s''$.

□

The completeness result follows immediately:

**Theorem 5.22.** If $S$ is a valid sequent, then it admits a fully expanded (possibly infinite) proof tree.

**Proof:**

The theorem follows from Lemma 5.21. □

**5.3. Termination and Complexity**

We now show that the proof procedure runs in polynomial time. To this purpose we provide (Definition 5.23 and Lemma 5.26) a characterization of the I-reducible sequents that may occur in a proof tree.

**Definition 5.23.** Let $\kappa \in \mathbb{N}$. A sequent $S$ is a $\kappa$-companion of a symbolic heap $\phi \wedge \xi$ if $S$ is of the form $(\phi_1\sigma * \phi_2 * \phi_3) \wedge (\xi_0 \wedge \xi_1 \wedge \xi_2) \vdash_{\Re}^V \psi \wedge \top$, where:

1. $\xi_0$ is the set of disequations occurring in $\xi$ that are of the form $x \not\approx t$ (up to commutativity), with $x \in (V(\phi_1\sigma * \phi_2 * \phi_3) \cup V(\psi)) \setminus V_{\text{loc}}$ and $t \neq x$.

2. $\xi_1 = \bigwedge_{x \in V^*(S), y \in A} x \not\approx y$, where $A = \text{alloc}(\phi_1\sigma * \phi_2 * \phi_3) \setminus V(\psi)$.

3. $\xi_2$ is a conjunction of disequations of the form $u \not\approx v$, where $u, v \in V(\psi)$.
4. $\psi$ is a predicate atom.

5. $V \subseteq \mathcal{V}(\psi)$.

6. Either $\phi_1 = emp$, or there exists a predicate atom $\alpha$ such that $\mathrm{root}(\alpha) = \mathrm{root}(\psi)$ and $\alpha \Leftarrow \mathfrak{R} \phi_1$.

7. $\mathrm{len}(\phi_2) \le \kappa + 1$.

8. $\sigma$ is a substitution such that $\mathrm{card}(\mathrm{dom}(\sigma)) \le \kappa$.

9. $\phi\sigma$ is of the form $\phi_3 * \eta_1 * \eta_2$ (modulo AC), where $\mathrm{len}(\eta_1) \le 2 \cdot \kappa$ and:

(a) no atom $\beta$ occurring in $\phi_3$ is such that $\mathrm{root}(\psi) \stackrel{*}{\to}_{\phi_1\sigma*\phi_2*\phi_3*\eta_2} \mathrm{root}(\beta)$; and

(b) no atom $\beta$ occurring in $\eta_2$ is such that $\mathrm{root}(\psi) \to^{*}_{\phi_1\sigma*\phi_2*\phi_3*\eta_2} \mathrm{root}(\beta)$.

Intuitively, we aim at describing sequents $S$ that are I-reducible and occur in some proof tree, where the formula $\phi \wedge \xi$ is meant to denote the left-hand side of the root sequent. It is clear that the left-hand side of $S$ will contain some parts that are inherited from the formula $\phi \wedge \xi$, together with some other parts, that are introduced by the inference rules applied along the branch of $S$ in the proof tree. First, observe that Conditions 4 (stating that the right-hand side of $S$ is a predicate atom $\psi$) and 5 (stating that the variables in $V$ must occur in $\psi$) are easy consequences of the fact that $S$ is I-reducible: rules S and V cannot be applied. The substitution $\sigma$ is intended to encode the effect of the (cumulative) applications of rule C (in the left branch): some variables initially occurring in $\phi \wedge \xi$ are replaced by other variables. Note that Condition 8 bounds the size of this substitution, which is essential to avoid any exponential blow-up. As we shall see, it stems from the fact that rule C only applies, by Definition 4.31 (4), to a variable in $V^*(S)$ which restricts the number of applications of the rule. The formula $\xi_0$ denotes the set of disequations between variables of a sort distinct from loc, which are all inherited from $\xi$ (as the rules contain no disequations of this form). On the other hand, $\xi_1$ denotes the set of disequations that were introduced by previous applications of C (in the right branch). Note that since $S$ is I-reducible, we may assume that all the possible applications of C have been applied, leading either to the elimination of a variable (encoded in $\sigma$) or to the addition of some disequation, this is why $\xi_1$ contains the set of all possible disequations. The formula $\xi_2$ denotes the set of disequations between variables in $\psi$, which are arbitrary (this is not problematic as the number of such disequations is bounded, as $\psi$ is an atom). The formula $\phi_1$ denotes the part of the formula added in the left-hand side of the sequent by the last application of U. The formula may be empty, because such application does not always exist (for instance if $S$ is the root sequent). The atom $\alpha$ then denotes the predicate atom on which U was previously applied. Observe that the root of this atom is always the same as that of $\psi$, by Definition 4.31 (3). Note also that the formula contains no atom obtained from any application of U occurring before the last one (i.e., on atoms other than $\alpha$): indeed, we shall prove that all such atoms must have been eliminated by previous decomposition steps when I was applied. The formula $\phi_1\sigma$ contains all spatial atoms inherited from the initial formula $\phi$. Note that some atoms in $\phi$ may have been deleted, by previous applications of S. The difficulty here is that this could lead to an exponential blow-up, since in principle one could consider all possible subsets of $\phi$. To overcome this issue, we refine the criterion by taking into account all the additional reachability conditions that
prevent $\mathcal{S}$ from being an axiom or an anti-axiom. We thus further split the conjunction of atoms that were deleted from $\phi$ into two parts $\eta_1 * \eta_2$, where $\eta_1$ contains a *bounded* number of atoms that can be chosen in an *arbitrary* way, and $\eta_2$ may contain an *arbitrary* number of atoms, but is fully determined by the choice of $\phi_1, \phi_2$ and $\eta_1$.

The following lemma shows that a formula has only polynomially many $\kappa$-companions, up to a renaming of variables.

**Lemma 5.24.** Let $\phi \wedge \xi$ be a spatial formula and $E$ be a set of variables. For every fixed number $\kappa$, if $ar_{max}(\mathfrak{R}) \le \kappa$ (i.e., if the maximal arity of the predicate symbols in bounded by $\kappa$), then the number of sequents $\mathcal{S}$ that are $\kappa$-companions of $\phi \wedge \xi$ and such that $\mathcal{V}(\mathcal{S}) \subseteq E$ is polynomial w.r.t. $|\phi| + |\mathfrak{R}| + \text{card}(E)$ (up to AC), and the size of $\mathcal{S}$ is polynomial w.r.t. $|\phi| + |\mathfrak{R}|$.

**Proof:**

By Definition 5.23, $\mathcal{S}$ is of the form $(\phi_1\sigma * \phi_2 * \phi_3) \wedge (\xi_1 \wedge \xi_2) \vdash_{\mathfrak{R}}^{\mathcal{V}} \psi \wedge \top$, and satisfies Conditions 1-9. Note that since $\psi$ is a predicate atom, we have $|\psi| \le 1 + ar_{max}(\mathfrak{R}) \le \kappa + 1$ and $\text{card}(\mathcal{V}(\psi)) \le ar_{max}(\mathfrak{R}) \le \kappa$.

We have $\text{len}(\phi_1 * \phi_2 * \phi_3) = \text{len}(\phi_1) + \text{len}(\phi_2) + \text{len}(\phi_3) \le \text{len}(\phi_1) + \kappa + 1 + \text{len}(\phi) \le |\mathfrak{R}| + |\phi| + \kappa + 1$, thus $|\phi_1\sigma * \phi_2 * \phi_3| \le (\kappa + 1) \cdot (|\mathfrak{R}| + |\phi| + \kappa + 1) = O(|\phi| + |\mathfrak{R}|)$. Since $\mathcal{V}(\zeta_1) \cup \mathcal{V}(\zeta_2) \subseteq \mathcal{V}(\phi_1\sigma * \phi_2 * \phi_3) \cup \mathcal{V}(\psi)$, we deduce that $|\xi_1 \wedge \xi_2| = O((|\phi| + |\mathfrak{R}|)^2)$ hence $|\mathcal{S}| = O((|\phi| + |\mathfrak{R}|)^2)$.

Let $n = \text{card}(E) + |\phi| + \text{card}(\mathcal{C}) + 1$. Note that $n \le \text{card}(E) + |\phi| + |\mathfrak{R}| + 1$. The number of possible predicate atoms $\psi$ and $\alpha$ is at most $\text{card}(\mathcal{P}) \cdot n^\kappa \le |\mathfrak{R}| \cdot n^\kappa$. Similarly, the number of formulas $\phi_2$ is at most $|\mathfrak{R}|^{\kappa+1} \cdot n^{(\kappa+1)^2}$. Once $\alpha$ is fixed, the number of formulas $\phi_1$ cannot be greater than the number of rules in $\mathfrak{R}$, up to a renaming of variables. Since $\text{card}(\text{dom}(\sigma)) \le \kappa$, there are at most $n^{2\kappa}$ possible substitutions $\sigma$ we only have to choose the set $\text{dom}(\sigma)$, i.e., at most $\kappa$ elements among the variables occurring in $\phi$ or $\phi_1$, and the image of each variable in $\text{dom}(\sigma)$ among the variables in $E$. The number of formulas $\phi_3$ is at most $\text{len}(\phi)^{2\kappa}$ (since we only have to choose the formula $\eta_1$ in $\phi$, as $\eta_2$ is entirely determined by the choice of $\phi_1, \phi_2$ and $\eta_1$). We have $\mathcal{V}(\xi_2) \subseteq \mathcal{V}(\psi)$ thus $\text{card}(\mathcal{V}(\xi_2)) \le \kappa$, and there are $2^{\kappa^2}$ possible formulas $\xi_2$. Since $V \subseteq \mathcal{V}(\psi)$, we have $\text{card}(V) \le \kappa$ and the number of possible sets $V$ is $2^\kappa$. Finally, the formulas $\xi_0$ and $\xi_1$ are fixed once $\phi$ and $\phi_1, \phi_2, \phi_3$ are fixed. $\square$

Lemma 5.26 below is used to prove that every sequent that is I-reducible and occurs in a proof tree is a companion of the left-hand side of the root of the proof tree. Together with Lemma 5.24 and the result stated in Lemma 5.12 on the number of I-free descendants of a sequent, this will entail that the size of the proof tree is polynomial w.r.t. the size of the root. We need the following proposition, which is an easy consequence of the definition of the rules.

**Proposition 5.25.** Let $S_i = \lambda_i \vdash_{\mathfrak{R}}^{V_i} \gamma_i$ (for $i = 1, 2$) be sequents. If $S_2$ is a successor of $S_1$, then $\text{alloc}(\lambda_1) \cap \text{alloc}(\gamma_1) \cap \text{alloc}(\lambda_2) \subseteq \text{alloc}(\gamma_2)$.

**Proof:**

Assume that $x \in \text{alloc}(\lambda_1) \cap \text{alloc}(\gamma_1) \cap \text{alloc}(\lambda_2)$ and $x \notin \text{alloc}(\gamma_2)$. It is easy to check, by inspection
of the rules, that the only rule that can remove the variable $x$ from $alloc(\gamma_1)$ is $S$ (indeed, $I$ deletes a predicate atom but introduce a points-to atom with the same root, and the rules $R$ and $C$ cannot replace $x$ as otherwise it would not occur in $\lambda_2$). By definition of the rule, $S_1$ also has a successor $S'_2 = \lambda'_2 \vdash_{\mathfrak{R}}^{V'_2} \gamma'_2$ such that $x \in V'_2$ (since $x \in alloc(\lambda_2)$) and $x \in alloc(\gamma'_2)$ (since $x \notin alloc(\gamma_2)$). This entails that $S'_2$ is an anti-axiom, contradicting Condition 1 in Definition 4.31. □

**Lemma 5.26.** Assume that $ar_{max}(\mathfrak{R}) \le \kappa$ for $\kappa \in \mathbb{N}$, and let $S = \phi \wedge \xi \vdash \psi \wedge \zeta$ be an equality-free sequent. Every $I$-reducible sequent occurring in a proof tree with root $S$ is a $\kappa$-companion of the left-hand side $\phi \wedge \xi$ of $S$.

**Proof:**

Let $S' = \phi' \wedge \xi' \vdash_{\mathfrak{R}}^{V'} \psi' \wedge \zeta'$ be an $I$-reducible sequent occurring in a proof tree with root $S$. Let $S_1, \dots, S_n$, be a path from $S$ to $S'$, where $S_1 = S, S_n = S'$ and $S_i = \lambda_i \vdash_{\mathfrak{R}}^{V_i} \gamma_i$ for $i = 1, \dots, n$. We check that all the conditions in Definition 5.23 are satisfied. Note that by Condition 1 in Definition 4.31, $S'$ cannot be an axiom or an anti-axiom.

* **Right-Hand Side.** We first show that the right-hand side $\psi'$ is indeed a predicate atom. By Condition 2 in Definition 4.31, $\zeta' = \top$ and $\psi'$ is a predicate atom, thus Condition 4 of Definition 5.23 holds.

* **Pure Formulas.** We then prove that the pure formulas $\xi'$ fulfill Conditions 1, 2 and 3. If $\xi'$ contains an equality then the rule $R$ applies, hence $S'$ cannot be $I$-reducible because $R$ has priority over $I$ (Condition 6 in Definition 4.31). Thus $\xi'$ is a conjunction of disequations, and it can be written as $\xi_0 \wedge \xi_1 \wedge \xi_2$ where $\xi_0$ is the set of disequations in $\xi'$ between terms of a sort distinct from $\text{loc}$, $\mathcal{V}(\xi_2) \subseteq \mathcal{V}(\psi') \cap \mathcal{V}_{\text{loc}}$ and $\xi_1$ only contains disequations of the form $u \not\approx v$ (up to commutativity of $\not\approx$) with $u, v \in \mathcal{V}_{\text{loc}}$ and $u \notin \mathcal{V}(\psi')$. Note that each disequation involves distinct terms because by hypothesis, $S'$ is not an axiom. Consider one such disequation $u \not\approx v$ in $\xi_1$. If $u \notin \mathcal{V}(\phi')$ then rule $W$ applies by the second application condition of the rule, which is impossible since this rule has priority over $I$ and $S'$ would not be $I$-reducible. We deduce that $u \in \mathcal{V}(\phi')$, and since $S'$ is not an anti-axiom, we must have $u \in \text{alloc}(\phi')$. If $v \notin \mathcal{V}(\phi') \cup \mathcal{V}(\psi')$ or $v \in \text{alloc}(\phi') \cup V'$ then rule $W$ also applies (in the latter case, we have $\phi' \triangleright_{V_i} u \not\approx v$ by Condition 3 of Definition 4.8). Thus $v \in \mathcal{V}(\phi') \cup \mathcal{V}(\psi')$ and $v \notin \text{alloc}(\phi') \cup V$. This entails that $v \in \mathcal{V}(\psi')$ since otherwise $S'$ would be an anti-axiom by Condition 5 of Definition 4.24 because $u \in \text{alloc}(\phi')$, hence $v$ is necessarily of sort $\text{loc}$. We therefore have $v \in \mathcal{V}^*(S')$ and $u \in \text{alloc}(\phi') \setminus \mathcal{V}(\psi')$. Conversely, if a disequation $u \not\approx v$ with $v \in \mathcal{V}^*(S')$ and $u \in \text{alloc}(\phi') \setminus \mathcal{V}(\psi')$ does not occur in $\xi_1$ then by Condition 4 in Definition 4.31, $C$ would be applicable, which is impossible. Thus Conditions 2 and 3 in Definition 5.23 are satisfied. By Proposition 4.17 (5) no rule introduces a disequation between terms of a sort distinct from $\text{loc}$, all disequations in $\xi_0$ must occur in $\xi$. Furthermore, such a disequation cannot be of the form $t \not\approx t$ (otherwise $S'$ would be an axiom as explained above) and must contain a variable occurring in $\phi'$ or $\psi'$ (otherwise $W$ would apply). Conversely, no rule can delete a disequation containing a variable in $(\mathcal{V}(\phi') \cup \mathcal{V}(\psi')) \setminus \mathcal{V}_{\text{loc}}$ from the left-hand side of the sequent. Thus Condition 1 holds.
• **Non Allocated Variables.** We now check that Condition 5 applies, namely that $V' \subseteq \mathcal{V}(\psi')$. Assume, for the sake of contradiction, that $V'$ contains a variable $x \notin \mathcal{V}(\psi')$. Since $S'$ is not an anti-axiom, we have $V' \cap (\mathcal{V}(\phi') \setminus \mathcal{V}(\psi')) = \emptyset$, hence $x \notin \mathcal{V}(\phi')$. If $x \in \mathcal{V}(\xi')$ then **W** applies, and otherwise **V** applies. In both cases, $S'$ cannot be **I**-reducible (since **W** and **V** have priority over **I**), which contradicts our assumption. Thus Condition 5 holds.

• **Substitution σ.** We now define the substitution σ, and we show that Condition 8 holds. Let *i* be the least number such that the right-hand side γᵢ of *S*ᵢ is a spatial atom (*i* must exist since *n* fulfills this condition, by Condition 2 in Definition 4.31), and let *V*° = *V*°(*S*ᵢ). Note that γᵢ must be a predicate atom. Indeed, the right-hand side of γᵢ = λn ⊢<sub>Π</sub><sup>Vn</sup> γn is a predicate atom since *S*ₙ is **I**-reducible, and by Condition 6 of Proposition 4.17, the only rule that can introduce a predicate atom to the right-hand side of a premise is **I**, which by Condition 2 in Definition 4.31, applies only if the right-hand side of the conclusion is a predicate atom. Thus γⱼ cannot be a points-to atom. By Proposition 5.4 we have *V*°(*S*ⱼ) ⊆ *V*°, for all j = *i*, ..., *n*, and *card*(*V*°) ≤ *ar*<sub>max</sub>(*Π*) ≤ κ since *V*° ⊆ *V*(*S*ᵢ) and γᵢ is a predicate atom. Let *I* ⊆ {1, ..., *n*} be the set of indices *j* such that rule **C** applies on *S*ⱼ, and replaces a variable *x*ⱼ by a variable *y*ⱼ (i.e., such that *S*ⱼ₊₁ is a left premise of an application of **C** on *S*ⱼ with variables *x*ⱼ and *y*ⱼ). By Condition 4 of Definition 4.31, **C** applies only if the right-hand side of the conclusion is a predicate atom, thus we must have *I* ⊆ {*i*, ..., *n*}. Let σ = σₙ, where σ₀ = *id*, σⱼ₊₁ = σⱼ{*x*ⱼ₊₁ ← *y*ⱼ₊₁} if *j* + 1 ∈ *I* and σⱼ₊₁ = σⱼ otherwise. By Condition 4 in Definition 4.31, for all *j* ∈ *I*, we have *y*ⱼ ∈ *V*°(*S*ⱼ) ⊆ *V*°(*S*ᵢ) = *V*°. Also, *y*ⱼ ∉ *V*°(*S*ⱼ₊₁) because *x*ⱼ must be allocated in the left-hand side of *S*ⱼ, hence, after the replacement, *y*ⱼ is allocated in the left-hand side of *S*ⱼ₊₁. Thus by Proposition 5.4, *y*ⱼ ∉ *V*°(*S*ⱼ'), for all *j'* > *j*, which entails that the *y*ⱼ for *j* ∈ *I* are pairwise distinct. Therefore, *card*(*I*) ≤ *card*(*V*°) ≤ κ, hence *card*(*dom*(*σ*)) ≤ κ and Condition 8 is satisfied.

• **Unfolded Atom.** Now we define the unfolded predicate atom $\alpha$ and we prove that Condition 6 holds. If rule **U** is applied on a sequent $S_k$ and $S'$ is an **I**-free descendant of $S_k$, then we denote by $\alpha$ the predicate atom on which **U** is applied, and by $\phi_1 \triangleleft \chi$ the formula occurring in $S_{k+1}$ such that $\alpha \Leftarrow \Re \ \phi_1 \triangleleft \chi$. If no such application of **U** exists then we simply set $\phi_1 = \text{emp}$. Note that if $k$ and $\alpha$ exist then they must be unique, since we assumed that $S'$ is an **I**-free descendant of $S_k$ and by Corollary 5.8 there must be an application of **I** along the path between any two applications of **U**. Also, by Condition 3 in Definition 4.31, $\gamma_k$ is a spatial atom and $\text{root}(\alpha) = \text{root}(\gamma_k)$. By Proposition 5.6, the only rules that can be applied on $S_{k+1}, \dots, S_{n-1}$ are **W**, **C**, or **V**. Each of these rules only affects the right-hand side of its premise by instantiating it with $\sigma$ thus $\text{root}(\alpha)\sigma = \text{root}(\psi')$. First consider the case where $k$ exists. Since the rules in $\Re$ are $P$-rules, $\lambda_{k+1}$ must contain a points-to atom. By Condition 3 in Definition 4.31, the root of this atom must be the same as that of $\gamma_k = \gamma_{k+1}$. Furthermore, $\lambda_{k+1}$ contains no equation, since otherwise this equation would occur in $\lambda_k$, rule **R** would be applicable on $S_k$ and this rule has priority over **U**. Therefore, $S_{k+1}$ is quasi-**I**-reducible. By Proposition 5.6, this entails that only the rules **W**, **V** or **C** may be applied along the path $S_{k+1}, \dots, S_n$. These rules either do not affect spatial formulas, or uniformly replace a variable $x_j$ (for $j \in I$) by $y_j = x_j\sigma_j$ (hence eventually, every variable $x$ is replaced by $x\sigma$). Thus $\phi'$ is of the form $\phi_1\sigma * \phi_1'$. It is clear that