The Bernays-Sch\"onfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable

TL;DR

This paper proves that the satisfiability problem for a fragment of first-order linear real arithmetic with bounded difference constraints and uninterpreted predicates is decidable, extending the understanding of decidable logical fragments over the reals.

Contribution

It introduces a decidable fragment of first-order real arithmetic with bounded difference constraints and uninterpreted predicates, which was previously undecidable.

Findings

Decidability is achieved by bounding the ranges of universally quantified variables.

The fragment includes difference constraints over reals with bounded intervals.

Trivial instantiation procedures are insufficient due to infinite value ranges.

Abstract

First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, even if we restrict the uninterpreted predicate symbols to arity one. In order to find decidable fragments of this language, it is necessary to restrict the expressiveness of the arithmetic part. One possible path is to confine arithmetic expressions to difference constraints of the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations $<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it is known that combining difference constraints with uninterpreted predicate symbols yields an undecidable satisfiability problem again. In this paper, it is shown that satisfiability becomes decidable if we in addition bound the ranges of universally quantified variables. As bounded intervals over the reals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the problem.

Equations

$$\displaystyle\widehat{\chi}(\bar{r}):=\bigl{\langle}\chi_{\mathcal{A}}$$

$$\displaystyle\ldots,\chi_{\mathcal{A}}\bigl{(}\langle r_{\varrho_{k}(1)}+\sigma_{k}(1),\ldots,r_{\varrho_{k}(m)}+\sigma_{k}(m)\rangle\bigr{)}\bigr{\rangle}$$

$$\phi :=\underset{x_1,x_2\in \bar{x}}{\bigwedge }$$

$$\displaystyle\hskip 77.49976pt\wedge\;\bigl{(}x_{1}-x_{2}\geq k\;\leftrightarrow\;x^{\prime}_{1}-x^{\prime}_{2}\geq k\bigr{)}$$

$$\displaystyle\wedge\;\bigwedge_{x\in\bar{x}}x^{\prime}\geq x\;\;\wedge\;\;\text{{inv}}_{\ell}[\bar{x}^{\prime}]\;\;\bigm{\|}\;\;\text{{Reach}}(\ell,\bar{x})\rightarrow\text{{Reach}}(\ell,\bar{x}^{\prime})~{}.~{}$$

$${\bar{r}}_1=⟨r_{⟨1,1⟩},\dots ,r_{⟨1,m⟩}⟩$$

$$⋮$$

$${\bar{r}}_p=⟨r_{⟨p,1⟩},\dots ,r_{⟨p,m⟩}⟩$$

$${\chi }^{\prime }(r_{⟨1,1⟩},\dots ,r_{⟨1,m⟩},\dots ,r_{⟨p,1⟩},\dots ,r_{⟨p,m⟩}):=\chi (r_{\varrho (1)},\dots ,r_{\varrho (m)})$$

$$⟨s_{⟨1,1⟩},\dots ,s_{⟨1,m⟩}⟩$$

$$⋮$$

$$⟨s_{⟨p,1⟩},\dots ,s_{⟨p,m⟩}⟩$$

$$q_{\ell }^{\prime }:=\{\begin{array}{ll}{c}^{\mathcal{A}}& \text{if rℓ=cA for some c∈bconsts(N)},\\ q_{i,j}& \text{if rℓ=si,j for some i, 0≤i≤κ, and some j, 1≤j≤ki,}\end{array}$$

$$⟨\bar{a},\bar{r}⟩\in P^{\mathcal{B}}\text{if and only if}⟨\bar{a},\bar{q}⟩\in P^{\mathcal{A}}.$$

$${\bar{r}}_1$$

$$⋮$$

$${\bar{r}}_{\kappa +1}$$

$${\bar{r}}_{\kappa +2}$$

$$⋮$$

$${\bar{r}}_{2K+1}$$

$$⟨\bar{a},\bar{r}⟩\in P^{\mathcal{B}}\text{if and only if}⟨\bar{a},\bar{q}⟩\in P^{\mathcal{A}}.$$

$$(*)\qquad\bigl{\langle}\widehat{\beta}_{C}(x_{1}),\ldots,\widehat{\beta}_{C}(x_{\ell})\bigr{\rangle}\mathrel{\widehat{\simeq}}_{\kappa}\bigl{\langle}\beta(x_{1}),\ldots,\beta(x_{\ell})\bigr{\rangle}~{}.$$

$$\lfloor {\hat{\beta }}_C(x)-{\hat{\beta }}_C(y)\rfloor$$

$$\displaystyle=\lfloor\beta(x)\rfloor-\lfloor\beta(y)\rfloor+\bigl{\lfloor}\text{fr}(\beta(x))-\text{fr}(\beta(y))\bigr{\rfloor}$$

$$=\lfloor \beta (x)-\beta (y)\rfloor$$

$$\lceil {\hat{\beta }}_C(x)-{\hat{\beta }}_C(y)\rceil$$

$$\displaystyle=\lceil\beta(x)\rceil-\lceil\beta(y)\rceil+\bigl{\lceil}\text{fr}(\beta(x))-\text{fr}(\beta(y))\bigr{\rceil}$$

$$=\lceil \beta (x)-\beta (y)\rceil .$$

$$\displaystyle\widehat{\chi}(\bar{r}):=\bigl{\langle}\chi_{\mathcal{A}}$$

$$\displaystyle\ldots,\chi_{\mathcal{A}}\bigl{(}\langle r_{\varrho_{k}(1)}+\sigma_{k}(1),\ldots,r_{\varrho_{k}(m)}+\sigma_{k}(m)\rangle\bigr{)}\bigr{\rangle}$$

$${\chi }_{\mathcal{A}}(\bar{s})$$

$$\displaystyle=\chi_{\mathcal{A}}\bigl{(}\langle q^{\prime}_{\varrho_{j}(1)}+\sigma(1),\ldots,q^{\prime}_{\varrho_{j}(m)}+\sigma(m)\rangle\bigr{)}=\chi_{\mathcal{A}}(\bar{s}^{\prime})~{}.\qed$$

$$\displaystyle\widehat{S}_{1}:=\bigl{\{}\bar{q}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}\bigm{|}\,$$

$$\displaystyle\text{we have $q_{i}\leq q^{\prime}_{i}$ and $q^{\prime}_{0}-q^{\prime}_{i}=q_{0}-q_{i}$}\bigl{\}}~{},$$

$$\displaystyle\widehat{S}_{2}:=\bigl{\{}\bar{q}^{\prime}\in[0$$

$$\bar{q}\in S$$

$$q_{i_1}\le q_{i_1}^{\prime }$$

$$q_{i_1}-q_{i_2}\le k$$

$$\displaystyle\qquad\text{$q_{i_{1}}-q_{i_{2}}\geq k$ if and only if $q^{\prime}_{i_{1}}-q^{\prime}_{i_{2}}\geq k$}\bigl{\}}~{},$$

$$(\ast )\text{fr}(q_0)-\text{fr}(q_i)=(\lfloor q_0^{\prime }\rfloor -\lfloor q_i^{\prime }\rfloor )-(\lfloor s_0\rfloor -\lfloor s_i\rfloor )+\text{fr}(q_0^{\prime })-\text{fr}(q_i^{\prime }).$$

$$\displaystyle\bigl{(}\lfloor s_{k_{1}}\rfloor+\text{fr}(q_{k_{1}})\bigr{)}-\bigl{(}\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\bigr{)}$$

$$\displaystyle=\lfloor s_{k_{1}}\rfloor+\varepsilon+\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{1}})\bigr{)}-\lfloor s_{k_{j}}\rfloor-\varepsilon-\bigl{(}\text{fr}(q^{\prime}_{k_{j}})-\text{fr}(q^{\prime}_{k_{1}})\bigr{)}$$

Full text

1 Introduction

It has been discovered about half a century ago that linear arithmetic with additional uninterpreted predicate symbols has an undecidable satisfiability problem [15]. Even enriching Presburger arithmetic with only a single uninterpreted predicate symbol of arity one suffices to facilitate encodings of the halting problem for two-counter machines [5, 10]. These results do not change substantially when we use the reals as underlying domain instead of the integers. This means, in order to obtain a decidable subfragment of the combination of linear arithmetic with uninterpreted predicate symbols, the arithmetic part has to be restricted considerably. In this paper, two subfragments with a decidable satisfiability problem are presented. Both are based on the Bernays–Schönfinkel–Ramsey fragment (BSR) of first-order logic, which is the $\exists^{*}\forall^{*}$ prefix class. Uninterpreted constant symbols and the distinguished equality predicate are allowed, non-constant function symbols are not. The arity of uninterpreted predicate symbols is not restricted. We extend BSR in two ways and call the obtained fragments BSR modulo simple linear real constraints (BSR(SLR)) and BSR modulo bounded difference constraints (BSR(BD)).

The first clause class—defined in Definition 1 and treated in detail in Section 4—adds constraints of the form $s\mathrel{\triangleleft}t$, $x\mathrel{\triangleleft}t$, and $x\mathrel{\triangleleft}y$ to BSR clauses, where $x$ and $y$ are real-valued variables that are implicitly universally quantified, $s$ and $t$ are linear arithmetic terms that are ground, and $\mathrel{\triangleleft}{\in}\{<,\leq,=,\neq,\geq,$ $>\}$. We allow Skolem constants in the ground terms $s$ and $t$. Since their value is not predetermined, they can be conceived as being existentially quantified. The constraints used in this clause fragment are similar to the kind of constraints that appear in the context of the array property fragment [4] and extensions thereof (see, e.g., [7, 9]). The main differences are that we use the real domain in this paper instead of the integer domain, and that we allow strict inequalities and disequations between universally quantified variables. In the presence of uninterpreted function symbols, strict inequality or disequations can be used to assert that some uninterpreted function $f$ is injective. This expressiveness prevents certain instantiation-based approaches to satisfiability checking from being applicable, e.g. the methods in [4, 9]. In the context of the array property fragment, this expressiveness even leads to undecidability.

The BSR(BD) clause class—presented in Definition 2 and in Section 5—adds constraints of the form $x\mathrel{\triangleleft}c$, $x\mathrel{\triangleleft}y$ and $x-y\mathrel{\triangleleft}c$ to BSR clauses, where $x$ and $y$ are real-valued variables, $c$ could be any rational number, and $\mathrel{\triangleleft}$ ranges over $\{<,\leq,=,\neq,\geq,>\}$ again. We refer to constraints of the form $x-y\mathrel{\triangleleft}c$ as difference constraints. Already in the seventies, Pratt identified difference constraints and boolean combinations thereof as an important tool for the formalization of verification conditions [14]. Applications include the verification of timed systems and scheduling problems (see, e.g., [11] for references). As unrestricted combinations of uninterpreted predicate symbols with difference constraints lead to an undecidable satisfiability problem (once more, two-counter machines can be encoded in a simple way [17]), we have to further confine the language. Every difference constraint $x-y\mathrel{\triangleleft}c$ has to be conjoined with four additional constraints $c_{x}\leq x$, $x\leq d_{x}$, $c_{y}\leq y$, $y\leq d_{y}$, where $c_{x},d_{x},c_{y},d_{y}$ are rationals. This restriction seems to weaken expressiveness severely. Indeed, it has to, since we aim for a decidable satisfiability problem. Yet, we show in Section 6 that BSR(BD) clause sets are expressive enough to formulate the reachability problem for timed automata. In [13] an encoding of the reachability problem for timed automata in difference logic (boolean combinations of difference constraints without uninterpreted predicate symbols) is given, which facilitates deciding bounded reachability, i.e. the problem of reaching a given set of states within a bounded number of transitions. When using BSR(BD) as a modeling language, we do not have to fix an upper bound on the number of steps a priori.

The main result of the present paper is that satisfiability of finite BSR(SLR) clause sets and finite BSR(BD) clause sets is decidable (Theorems 13 and 20), respectively. The proof technique is very similar for the two fragments. It is partially based on methods from Ramsey theory, which are briefly introduced in Section 3. The used approach may turn out to be applicable to other fragments of BSR modulo linear real arithmetic as well.

In order to facilitate smooth reading, long proofs are only sketched in the main text and presented in full in the appendix. The present paper is an extended version of [16].

2 Preliminaries and notation

Hierarchic combinations of first-order logic with background theories build upon sorted logic with equality [2, 3, 12]. We instantiate this framework with the BSR fragment and linear arithmetic over the reals as the base theory. The base sort $\mathcal{R}$ shall always be interpreted by the reals $\mathbb{R}$. For simplicity, we restrict our considerations to a single free sort $\mathcal{S}$, which may be freely interpreted as some nonempty domain, as usual.

We denote by $V_{\mathcal{R}}$ a countably infinite set of base-sort variables. Linear arithmetic (LA) terms are build from rational constants $0,1,\tfrac{1}{2},-2,-\tfrac{3}{4}$, etc., the operators $+,-$, and the variables from $V_{\mathcal{R}}$. We moreover allow base-sort constant symbols whose values have to be determined by an interpretation (Skolem constants). They can be conceived as existentially quantified. As predicates over the reals we allow the standard relations $<,\leq,=,\not=,\geq,>$.

In order to hierarchically extend the base theory by the BSR fragment, we introduce the free sort $\mathcal{S}$, a countably infinite set $V_{\mathcal{S}}$ of free-sort variables, a finite set $\Omega_{\mathcal{S}}$ of free (uninterpreted) constant symbols of sort $\mathcal{S}$ and a finite set $\Pi$ of free predicate symbols equipped with sort information. Note that every predicate symbol in $\Pi$ has a finite, nonnegative arity and can be of a mixed sort over the two sorts $\mathcal{R}$ and $\mathcal{S}$, e.g. $P:\mathcal{R}\times\mathcal{S}\times\mathcal{R}$. We use the symbol $\approx$ to denote the built-in equality predicate on $\mathcal{S}$. To avoid confusion, we tacitly assume that no constant or predicate symbol is overloaded, i.e. they have a unique sort.

Definition 1** (BSR with simple linear real constraints—BSR(SLR)).**

A BSR(SLR) clause has the form $\Lambda\,\|\,\Gamma\to\Delta$, where $\Lambda$, $\Gamma$, $\Delta$ are multisets of atoms satisfying the following conditions. (i) Every atom in $\Lambda$ is an LA constraint of the form $s\mathrel{\triangleleft}t$ or $x\mathrel{\triangleleft}t$ or $x\mathrel{\triangleleft}y$ where $s,t$ are ground (i.e. variable-free) LA terms, $x,y\in V_{\mathcal{R}}$, and $\mathrel{\triangleleft}\,{\in}\{<,\leq,$ $=,\not=,\geq,>\}$. (ii) Every atom in $\Gamma$ and $\Delta$ is either an equation $s\approx s^{\prime}$ over free-sort variables and constant symbols, or a non-equational atom $P(s_{1},\ldots,s_{m})$ that is well sorted and where the $s_{i}$ range over base-sort variables, free-sort variables, and free-sort constant symbols.

Definition 2** (BSR with bounded difference constraints—BSR(BD)).**

A BSR(BD) clause has the form $\Lambda\,\|\,\Gamma\to\Delta$, where the multisets $\Gamma$, $\Delta$ satisfy Condition (ii) of Definition 1, and every atom in $\Lambda$ is an LA constraint of the form $x\mathrel{\triangleleft}c$, $x\mathrel{\triangleleft}y$, or $x-y\mathrel{\triangleleft}c$ where $c$ may be any rational constant (not a Skolem constant), $x,y\in V_{\mathcal{R}}$, and $\mathrel{\triangleleft}\,{\in}\{<,\leq,$ $=,\not=,\geq,>\}$. Moreover, we require that whenever $\Lambda$ contains a constraint of the form $x-y\mathrel{\triangleleft}c$, then $\Lambda$ also contains constraints $c_{x}\leq x$, $x\leq d_{x}$, $c_{y}\leq y$, and $y\leq d_{y}$ with $c_{x},d_{x},c_{y},d_{y}\in\mathbb{Q}$.

We omit the empty multiset left of “$\rightarrow$” and denote it by $\Box$ right of “$\rightarrow$” (where $\Box$ at the same time stands for falsity). The introduced clause notation separates arithmetic constraints from the free first-order part. We use the vertical double bar “$\|$” to indicate this syntactically. Intuitively, clauses $\Lambda\,\|\,\Gamma\to\Delta$ can be read as \bigl{(}\bigwedge\Lambda\wedge\bigwedge\Gamma\bigr{)}\to\bigvee\Delta, i.e. the multisets $\Lambda,\Gamma$ stand for conjunctions of atoms and $\Delta$ stands for a disjunction of atoms. Requiring the free parts $\Gamma$ and $\Delta$ of clauses to not contain any base-sort terms apart from variables does not limit expressiveness. Every base-sort term $t\not\in V_{\mathcal{R}}$ in the free part can safely be replaced by a fresh base-sort variable $x_{t}$ when an atomic constraint $x_{t}=t$ is added to the constraint part of the clause (a process known as purification or abstraction [2, 12]).

A (hierarchic) interpretation is an algebra $\mathcal{A}$ which interprets the base sort $\mathcal{R}$ as $\mathcal{R}^{\mathcal{A}}=\mathbb{R}$, assigns real values to all occurring base-sort Skolem constants and interprets all LA terms and constraints in the standard way. Moreover, $\mathcal{A}$ comprises a nonempty domain $\mathcal{S}^{\mathcal{A}}$, assigns to each free-sort constant symbol $c$ in $\Omega_{\mathcal{S}}$ a domain element $c^{\mathcal{A}}\in\mathcal{S}^{\mathcal{A}}$, and interprets every sorted predicate symbol $P\!:\!\xi_{1}\times\ldots\times\xi_{m}$ in $\Pi$ by some set $P^{\mathcal{A}}\subseteq\xi_{1}^{\mathcal{A}}\times\ldots\times\xi_{m}^{\mathcal{A}}$. Summing up, $\mathcal{A}$ extends the standard model of linear arithmetic and adopts the standard approach to semantics of (sorted) first-order logics when interpreting the free part of clauses.

Given an interpretation $\mathcal{A}$ and a sort-respecting variable assignment $\beta:V_{\mathcal{R}}\cup V_{\mathcal{S}}\to\mathcal{R}^{\mathcal{A}}\cup\mathcal{S}^{\mathcal{A}}$, we write $\mathcal{A}(\beta)(s)$ to mean the value of the term $s$ under $\mathcal{A}$ with respect to the variable assignment $\beta$. The variables occurring in clauses are implicitly universally quantified. Therefore, given a clause $C$, we call $\mathcal{A}$ a (hierarchic) model of $C$, denoted $\mathcal{A}\models C$, if and only if $\mathcal{A},\beta\models C$ holds for every variable assignment $\beta$. For clause sets $N$, we write $\mathcal{A}\models N$ if and only if $\mathcal{A}\models C$ holds for every clause $C\in N$. We call a clause $C$ (a clause set $N$) satisfiable if and only if there exists a model $\mathcal{A}$ of $C$ (of $N$). Two clauses $C,D$ (clause sets $N,M$) are equisatisfiable if and only if $C$ ($N$) is satisfiable whenever $D$ ($M$) is satisfiable and vice versa.

Given a BSR(SLR) or BSR(BD) clause $C$, we use the following notation: the set of all constant symbols occurring in $C$ is denoted by $\text{{consts}}(C)$. The set $\text{{bconsts}}(C)$ ($\text{{fconsts}}(C)$) is the restriction of $\text{{consts}}(C)$ to base-sort (free-sort) constant symbols. We denote the set of all variables occurring in a clause $C$ by $\text{{vars}}(C)$. The same notation is used for sets of clauses.

Definition 3** (Normal form of BSR(SLR) and BSR(BD) clauses).**

A BSR(SLR) or BSR(BD) clause $\Lambda\,\|\,\Gamma\to\Delta$ is in normal form if (1) all non-ground atoms in $\Lambda$ have the form $x\mathrel{\triangleleft}c$, $x\mathrel{\triangleleft}y$, or $x-y\mathrel{\triangleleft}c$ where $c$ is a rational constant or a Skolem constant, and (2) every variable that occurs in $\Lambda$ also occurs in $\Gamma$ or in $\Delta$. A BSR(SLR) or BSR(BD) clause set $N$ is in normal form if all clauses in $N$ are in normal form and pairwise variable disjoint. Moreover, we assume that $N$ contains at least one free-sort constant symbol.

For BSR(SLR) clause sets, we pose the following additional requirement. $N$ can be divided into two parts $N_{\text{def}}$ and $N^{\prime}$ such that (a) every clause in $N_{\text{def}}$ has the form $c\neq t\,\|\,\rightarrow\Box$ where $c$ is a Skolem constant and $t$ is some ground LA term, and (b) any ground atom $s\mathrel{\triangleleft}t$ in any constraint part $\Lambda$ in any clause $\Lambda\,\|\,\Gamma\rightarrow\Delta$ in $N^{\prime}$ is such that $s$ and $t$ are constants (Skolem or rational, respectively).

For every BSR(SLR) clause set $N$ there is an equisatisfiable BSR(SLR) clause set $N^{\prime}$ in normal form. The same holds for BSR(BD) clause sets. Requirement (2) can be established by any procedure for eliminating existentially quantified variables in LA constraints (see, e.g., [6]). Establishing the other requirements is straightforward.

For two sets $R,Q\subseteq\mathbb{R}$ we write $R<Q$ if $r<q$ holds for all $r\in R$ and $q\in Q$. Given a real $r$, we denote the integral part of $r$ by $\lfloor r\rfloor$, i.e. $\lfloor r\rfloor$ is the largest integer for which $\lfloor r\rfloor\leq r$. By $\text{fr}(r)$ we denote the fractional part of $r$, i.e. $\text{fr}(r):=r-\lfloor r\rfloor$. Notice that $\text{fr}(r)$ is always nonnegative, e.g. $\text{fr}(3.71)=0.71$, whereas $\text{fr}(-3.71)=0.29$. Given any tuple $\bar{r}$ of reals, we write $\text{fr}(\bar{r})$ to mean the corresponding tuple of fractional parts, i.e. \text{fr}\bigl{(}\langle r_{1},\ldots,r_{\mu}\rangle\bigr{)}:=\bigl{\langle}\text{fr}(r_{1}),\ldots,\text{fr}(r_{\mu})\bigr{\rangle}. We use the notation $\lfloor\bar{r}\rfloor$ in a component-wise fashion as well.

We write $[k]$ to address the set $\{1,\ldots,k\}$ for any positive integer $k>0$. Finally, $\mathcal{P}$ denotes the power set operator, i.e. for any set $S$, $\mathcal{P}(S)$ denotes the set of all subsets of $S$.

3 Basic tools from Ramsey theory

In this section we establish two technical results based on methods usually applied in Ramsey theory. We shall use these results later on to prove the existence of models of a particular kind for BSR(SLR) or BSR(BD) clause sets that are finite and satisfiable. These models meet certain uniformity conditions. In order to construct them, we rely on the existence of certain finite subsets of $\mathbb{R}$ that are used to construct prototypical tuples of reals. These finite subsets, in turn, have to behave nicely as well, since tuples that are not distinguishable by BSR(SLR) or BSR(BD) constraints are required to have certain uniformity properties.

A tuple $\langle r_{1},\ldots,r_{m}\rangle\in\mathbb{R}^{m}$ is called ascending if $r_{1}<\ldots<r_{m}$. A coloring is a mapping $\chi:S\to\mathcal{C}$ for some arbitrary set $S$ and some finite set $\mathcal{C}$. For the most basic result of this section (Lemma 4), we consider an arbitrary coloring $\chi$ of $m$-tuples of real numbers and stipulate the existence of a finite subset $Q\subseteq\mathbb{R}$ of a given cardinality $n$ such that all ascending $m$-tuples of elements from $Q$ are assigned the same color by $\chi$.

Lemma 4**.**

Let $n,m>0$ be positive integers. Let $\chi:\mathbb{R}^{m}\to\mathcal{C}$ be some coloring. For every set $R\subseteq\mathbb{R}$ of sufficient size (either infinite or finite with sufficiently many elements) there exists a subset $Q\subseteq R$ of cardinality $n$ such that all ascending tuples $\langle r_{1},\ldots,r_{m}\rangle\in Q^{m}$ are assigned the same color by $\chi$.

adaptation of the proof of Ramsey’s Theorem on page 7 in [8].

For $n<m$ the lemma is trivially satisfied, since in this case $Q^{m}$ cannot contain ascending tuples. Hence, we assume $n\geq m$. In order to avoid technical difficulties when defining the sequence of elements $s_{m-1},s_{m},s_{m+1},\ldots$ below, we assume for the rest of the proof that $R$ is finite but sufficiently large. This assumption does not pose a restriction, as we can always consider a sufficiently large subset of $R$.

We proceed by induction on $m\geq 1$. The base case $m=1$ is easy, since $\chi$ can assign only finitely many colors to elements in $R$ and thus some color must be assigned at least \bigl{\lfloor}\tfrac{|R|}{|\mathcal{C}|}\bigr{\rfloor} times. Hence, if $R$ contains at least $n|\mathcal{C}|$ elements, we find a uniformly colored subset $Q$ of size $n$. Suppose $m>1$. At first, we pick the $m-2$ smallest reals $s_{1}<\ldots<s_{m-2}$ from $R$ and set $S_{m-2}:=R\setminus\{s_{1},\ldots,s_{m-2}\}$. Thereafter, we simultaneously construct two sufficiently long but finite sequences $s_{m-1},s_{m},s_{m+1},\ldots$ and $S_{m-1},S_{m},S_{m+1},\ldots$ as follows:

Given $S_{i}$, we define $s_{i+1}$ to be the smallest real in $S_{i}$.

Given $S_{i}$ and the element $s_{i+1}$, we define an equivalence relation $\sim_{i}$ on the set $S^{\prime}_{i}:=S_{i}\setminus\{s_{i+1}\}$ so that $s\sim_{i}s^{\prime}$ holds if and only if for every sequence of indices $j_{1},\ldots,j_{m-1}$ with $1\leq j_{1}<\ldots<j_{m-1}\leq i+1$, we have $\chi(s_{j_{1}},\ldots,s_{j_{m-1}},s)=\chi(s_{j_{1}},\ldots,s_{j_{m-1}},s^{\prime})$. This equivalence relation partitions $S^{\prime}_{i}$ into at most $|\mathcal{C}|^{{i+1}\choose{m-1}}$ equivalence classes. We choose one such class with largest cardinality to be $S_{i+1}$.

By construction of the sequence $s_{1},s_{2},s_{3},\ldots$, we must have $\chi(s_{j_{1}},\ldots,s_{j_{m-1}},$ $s_{k})=\chi(s_{j_{1}},\ldots,$ $s_{j_{m-1}},s_{k^{\prime}})$ for every sequence of indices $j_{1}<\ldots<j_{m-1}$ and all indices $k,k^{\prime}\geq j_{m-1}+1$. Please note that this covers all ascending $m$-tuples in $\{s_{1},s_{2},s_{3},\ldots\}^{m}$ starting with $s_{j_{1}},\ldots,s_{j_{m}-1}$, i.e. they all share the same color. We now define a new coloring $\chi^{\prime}:\{s_{1},s_{2},s_{3},\ldots\}^{m-1}\to\mathcal{C}$ so that $\chi^{\prime}(s_{j_{1}},\ldots,$ $s_{j_{m-1}}):=\chi(s_{j_{1}},\ldots,s_{j_{m-1}},s_{j_{m-1}+1})$ for every sequence of indices $j_{1}<\ldots<j_{m-1}$ (in case of $j_{m-1}$ being the index of the last element in the sequence $s_{1},s_{2},s_{3},\ldots$, $\chi^{\prime}(s_{j_{1}},\ldots,s_{j_{m-1}})$ shall be an arbitrary color from $\mathcal{C}$). By induction, there exists a subset $Q\subseteq\{s_{1},s_{2},s_{3},\ldots\}$ of cardinality $n$, such that every ascending $(m-1)$-tuple $\bar{r}\in Q^{m-1}$ is colored the same by $\chi^{\prime}$. The definition of $\chi^{\prime}$ entails that now all ascending $m$-tuples $\bar{r}^{\prime}\in Q^{m}$ are colored the same by $\chi$. Hence, $Q$ is the sought set. ∎

Based on Lemma 4, one can derive similar results for more structured ways of coloring tuples of reals. One such result is given in the next lemma. Its proof can be found in the appendix.

Lemma 5**.**

Let $n,m,p>0$ be positive integers, let $\kappa\geq 0$ be a nonnegative integer and let $\chi:\mathbb{R}^{m}\to\mathcal{C}$ be an arbitrary coloring. Let $R_{1},\ldots,R_{p}$ be sufficiently large but finite subsets of $\mathbb{R}$. Let $q_{1},\ldots,q_{\kappa}$ be fixed reals. Let $\varrho_{1},\ldots,\varrho_{L}$ be some enumeration of all mappings $\varrho_{j}:[m]\to[p+\kappa]\times[m]$ for which $\varrho_{j}(i)=\langle k,\ell\rangle$ with $k>p$ entails $\ell=1$. There exist subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p}\subseteq R_{p}$, each of cardinality $n$, such that for all ascending tuples $\bar{r}_{1},\bar{r}^{\prime}_{1}\in Q_{1}^{m},\ldots,\bar{r}_{p},\bar{r}^{\prime}_{p}\in Q_{p}^{m}$ and the reals $r_{\langle p+1,1\rangle}:=q_{1},\dots,r_{\langle p+\kappa,1\rangle}:=q_{\kappa}$ and every index $j$, $1\leq j\leq L$, we have \chi\bigl{(}r_{\varrho_{j}(1)},\ldots,r_{\varrho_{j}(m)}\bigr{)}=\chi\bigl{(}r^{\prime}_{\varrho_{j}(1)},\ldots,r^{\prime}_{\varrho_{j}(m)}\bigr{)}.

4 Decidability of satisfiability for BSR(SLR) clause sets

For the rest of this section we fix two positive integers $m,m^{\prime}>0$ and some finite BSR(SLR) clause set $N$ in normal form. For the sake of simplicity, we assume that all uninterpreted predicate symbols $P$ occurring in $N$ have the sort $P:\mathcal{S}^{m^{\prime}}\times\mathcal{R}^{m}$. This assumption does not limit expressiveness, as the arity of a predicate symbol $P$ can easily be increased in an (un)satisfiability-preserving way by padding the occurring atoms with additional arguments. For instance, every occurrence of atoms $P(t_{1},\ldots,t_{m})$ can be replaced with $P(t_{1},\ldots,t_{m},v,\ldots,v)$ for some fresh variable $v$ that is added sufficiently often as argument.

Given the BSR(SLR) clause set $N$, every interpretation $\mathcal{A}$ induces a partition of $\mathbb{R}$ into finitely many intervals: the interpretations of all the rational and Skolem constants $c$ occurring in $N$ yield point intervals that are interspersed with and enclosed by open intervals.

Definition 6** ($\mathcal{A}$-induced partition of $\mathbb{R}$).**

Let $\mathcal{A}$ be an interpretation and let $r_{1},\ldots,r_{k}$ be all the values in the set $\{c^{\mathcal{A}}\mid c\in\text{{bconsts}}(N)\}$ in ascending order. By ${\mathcal{J}_{\mathcal{A}}}$ we denote the following partition of $\mathbb{R}$:

{\mathcal{J}_{\mathcal{A}}}:=\bigl{\{}(-\infty,r_{1}),[r_{1},r_{1}],(r_{1},r_{2}),[r_{2},r_{2}],\ldots,(r_{k-1},r_{k}),[r_{k},r_{k}],(r_{k},+\infty)\bigr{\}}.

The idea of the following equivalence is that equivalent tuples are indistinguishable by the constraints that we allow in the BSR(SLR) clause set $N$.

Definition 7** (${\mathcal{J}_{\mathcal{A}}}$-equivalence, $\sim_{\mathcal{J}_{\mathcal{A}}}$).**

Let $\mathcal{A}$ be an interpretation and let $k$ be a positive integer. We call two $k$-tuples $\bar{r},\bar{q}\in\mathbb{R}^{k}$ ${\mathcal{J}_{\mathcal{A}}}$-equivalent if

(i) for every $J\in{\mathcal{J}_{\mathcal{A}}}$ and every $i$, $1\leq i\leq k$, we have $r_{i}\in J$ if and only if $q_{i}\in J$ and

(ii) for all $i,j$, $1\leq i,j\leq k$ we have $r_{i}<r_{j}$ if and only if $q_{i}<q_{j}$.

The induced equivalence relation on tuples of positive length is denoted by $\sim_{\mathcal{J}_{\mathcal{A}}}$.

For every positive $k$ the relation $\sim_{\mathcal{J}_{\mathcal{A}}}$ induces only finitely many equivalence classes on the set of all $k$-tuples over the reals. We intend to show that, if $N$ is satisfiable, then there is some model $\mathcal{A}$ for $N$ which does not distinguish between different ${\mathcal{J}_{\mathcal{A}}}$-equivalent tuples. First, we need some notion that reflects how the interpretation $\mathcal{A}$ treats a given tuple $\bar{r}\in\mathbb{R}^{m}$. This role will be taken by the coloring $\chi_{\mathcal{A}}$, which maps $\bar{r}$ to a set of expressions of the form $P\bar{a}$, where $P$ is some predicate symbol occurring in $N$ and $\bar{a}$ is an $m^{\prime}$-tuple of domain elements from $\mathcal{S}^{\mathcal{A}}$. The presence of $P\bar{a}$ in the set $\chi_{\mathcal{A}}(\bar{r})$ indicates that $\mathcal{A}$ interprets $P$ in such a way that $P^{\mathcal{A}}$ contains the pair $\langle\bar{a},\bar{r}\rangle$. In this sense, $\chi_{\mathcal{A}}(\bar{r})$ comprises all the relevant information that $\mathcal{A}$ contains regarding the tuple $\bar{r}$.

Definition 8** ($\mathcal{A}$-coloring $\chi_{\mathcal{A}}$).**

Given an interpretation $\mathcal{A}$, let \widehat{\mathcal{S}}:=\{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}}$for some$c\in} $\text{{fconsts}}(N)\}$ be the set of all domain elements assigned to free-sort constant symbols by $\mathcal{A}$. The $\mathcal{A}$-coloring of $\mathbb{R}^{m}$ is the mapping

\chi_{\mathcal{A}}:\mathbb{R}^{m}\to\mathcal{P}\{P\bar{a}\mid\text{\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$and$P$is an uninterpreted predicate symbol in$N}\}

defined such that for every $\bar{r}\in\mathbb{R}^{m}$ we have $P\bar{a}\in\chi_{\mathcal{A}}(\bar{r})$ if and only if $\langle\bar{a},\bar{r}\rangle\in P^{\mathcal{A}}$.

Having the coloring $\chi_{\mathcal{A}}$ at hand, it is easy to formulate a uniformity property for a given interpretation $\mathcal{A}$. Two tuples $\bar{r},\bar{r}^{\prime}\in\mathbb{R}^{m}$ are treated uniformly by $\mathcal{A}$, if the colors $\chi_{\mathcal{A}}(\bar{r})$ and $\chi_{\mathcal{A}}(\bar{r}^{\prime})$ agree. Put differently, $\mathcal{A}$ does not distinguish $\bar{r}$ from $\bar{r}^{\prime}$.

Definition 9** (${\mathcal{J}_{\mathcal{A}}}$-uniform interpretation).**

An interpretation $\mathcal{A}$ is ${\mathcal{J}_{\mathcal{A}}}$-uniform if $\chi_{\mathcal{A}}$ colors each and every $\sim_{\mathcal{J}_{\mathcal{A}}}$-equivalence class uniformly, i.e. for all $\sim_{\mathcal{J}_{\mathcal{A}}}$-equivalent tuples $\bar{r},\bar{r}^{\prime}$ we have $\chi_{\mathcal{A}}(\bar{r})=\chi_{\mathcal{A}}(\bar{r}^{\prime})$.

We next show that there exists a ${\mathcal{J}_{\mathcal{B}}}$-uniform model $\mathcal{B}$ of $N$, if $N$ is satisfiable. Since such a model does not distinguish between ${\mathcal{J}_{\mathcal{B}}}$-equivalent $m$-tuples, and as there are only finitely many equivalence classes induced by $\sim_{\mathcal{J}_{\mathcal{B}}}$, only a finite amount of information is required to describe $\mathcal{B}$. This insight will give rise to a decision procedure that nondeterministically guesses how each and every equivalence class shall be treated by the uniform model.

Given some model $\mathcal{A}$ of $N$, the following lemma assumes the existence of certain finite sets $Q_{i}$ with a fixed cardinality which are subsets of the open intervals in ${\mathcal{J}_{\mathcal{A}}}$. All ${\mathcal{J}_{\mathcal{A}}}$-equivalent $m$-tuples that can be constructed from the reals belonging to the $Q_{i}$ are required to be colored identically by $\chi_{\mathcal{A}}$. The existence of the $Q_{i}$ is the subject of Lemma 11.

Lemma 10**.**

Let $\lambda$ be the maximal number of distinct base-sort variables in any single clause in $N$. In case of $\lambda<m$, we set $\lambda:=m$. Let $\mathcal{A}$ be a model of $N$. Let $J_{0},\ldots,J_{\kappa}$ be an enumeration of all open intervals in ${\mathcal{J}_{\mathcal{A}}}$ sorted in ascending order, i.e. $J_{0}<\ldots<J_{\kappa}$. Suppose we are given a collection of finite sets $Q_{0},\ldots,Q_{\kappa}$ possessing the following properties:

(i) $Q_{i}\subseteq J_{i}$ and $|Q_{i}|=\lambda$ for every $i$, $0\leq i\leq\kappa$.

(ii) Let $Q:=\bigcup_{i}Q_{i}\cup\{c^{\mathcal{A}}\mid c\in\text{{bconsts}}(N)\}$. For all ${\mathcal{J}_{\mathcal{A}}}$-equivalent $m$-tuples $\bar{q},\bar{q}^{\prime}\in Q^{m}$ we have $\chi_{\mathcal{A}}(\bar{q})=\chi_{\mathcal{A}}(\bar{q}^{\prime})$.

Then we can construct a model $\mathcal{B}$ of $N$ that is ${\mathcal{J}_{\mathcal{B}}}$-uniform and that interprets the free sort $\mathcal{S}$ as a finite set.

Proof sketch.

Claim I: Let $\mu$ be a positive integer with $\mu\leq\lambda$. Every $\sim_{\mathcal{J}_{\mathcal{A}}}$-equivalence class over $\mathbb{R}^{\mu}$ contains some representative lying in $Q^{\mu}$. $\Diamond$

Let $\widehat{\mathcal{S}}$ denote the set \{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}}$for some$c\in\text{{fconsts}}(N)}\}. We construct the interpretation $\mathcal{B}$ as follows: $\mathcal{S}^{\mathcal{B}}:=\widehat{\mathcal{S}}$; $c^{\mathcal{B}}:=c^{\mathcal{A}}$ for every constant symbol $c$; for every uninterpreted predicate symbol $P$ and for all tuples $\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$ and $\bar{r}\in\mathbb{R}^{m}$ we pick some tuple $\bar{q}\in Q^{m}$ with $\bar{q}\sim_{\mathcal{J}_{\mathcal{A}}}\bar{r}$, and we define $P^{\mathcal{B}}$ so that $\langle\bar{a},\bar{r}\rangle\in P^{\mathcal{B}}$ if and only if $\langle\bar{a},\bar{q}\rangle\in P^{\mathcal{A}}$. By construction, $\mathcal{B}$ is ${\mathcal{J}_{\mathcal{B}}}$-uniform.

It remains to show $\mathcal{B}\models N$. Consider any clause $C=\Lambda\;\|\;\Gamma\to\Delta$ in $N$ and let $\beta$ be any variable assignment ranging over $\mathcal{S}^{\mathcal{B}}\cup\mathbb{R}$. Starting from $\beta$, we derive a special variable assignment $\widehat{\beta}_{C}$ as follows. Let $x_{1},\ldots,x_{\ell}$ be all base-sort variables in $C$. By Claim I, there is some tuple $\langle q_{1},\ldots,q_{\ell}\rangle\in Q^{\ell}$ such that \langle q_{1},\ldots,q_{\ell}\rangle\sim_{\mathcal{J}_{\mathcal{A}}}\bigl{\langle}\beta(x_{1}),\ldots,\beta(x_{\ell})\bigr{\rangle}. We set $\widehat{\beta}_{C}(x_{i}):=q_{i}$ for every $x_{i}$. For all other base-sort variables, $\widehat{\beta}_{C}$ can be defined arbitrarily. For every free-sort variable $u$ we set $\widehat{\beta}_{C}(u):=\beta(u)$.

As $\mathcal{A}$ is a model of $N$, we get $\mathcal{A},\widehat{\beta}_{C}\models C$. By case distinction on why $\mathcal{A},\widehat{\beta}_{C}\models C$ holds, one can infer $\mathcal{B},\beta\models C$. Consequently, $\mathcal{B}\models N$. ∎

In order to show that uniform models always exist satisfiable clause sets $N$, we still need to prove the existence of the sets $Q_{i}$ mentioned in Lemma 10. We use Lemma 5 to show this.

Lemma 11**.**

Let $\mathcal{A}$ be an interpretation. Moreover, let $q_{1},\ldots,q_{\kappa}$ be all reals in $\{c^{\mathcal{A}}\mid c\in\text{{bconsts}}(N)\}$ in ascending order and let $J_{1},\ldots,J_{\kappa+1}$ be all open intervals in ${\mathcal{J}_{\mathcal{A}}}$ in ascending order, i.e. $J_{1}<\{q_{1}\}<J_{2}<\{q_{2}\}<\ldots<J_{\kappa}<\{q_{\kappa}\}<J_{\kappa+1}$. Let $\lambda$ be a positive integer. There is a collection of finite sets $Q_{1},\ldots,Q_{\kappa+1}$ such that the following requirements are met.

(i) For every $i$, $1\leq i\leq\kappa+1$, we have $Q_{i}\subseteq J_{i}$ and $|Q_{i}|=\lambda$.

(ii) Let $Q:=\bigcup_{i}Q_{i}\cup\{q_{1},\ldots,q_{\kappa}\}$. For all ${\mathcal{J}_{\mathcal{A}}}$-equivalent $m$-tuples $\bar{s},\bar{s}^{\prime}\in Q^{m}$ we have $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\bar{s}^{\prime})$.

Proof sketch.

Let the sets $Q_{1},\ldots,Q_{\kappa+1}$ be the $Q_{1},\ldots,Q_{p}$ that we obtain by virtue of Lemma 5 when we set $n:=\lambda$, $p:=\kappa+1$, $\chi:=\chi_{\mathcal{A}}$, $R_{1}:=J_{1},\ldots,R_{\kappa+1}:=J_{\kappa+1}$. Requirement (i) is obviously satisfied for $Q_{1},\ldots,Q_{\kappa+1}$.

One can show that for every equivalence class $S\in\mathbb{R}^{m}/_{\sim_{\mathcal{J}_{\mathcal{A}}}}$ there is some mapping $\varrho:[m]\to[2\kappa+1]\times[m]$ such that

1. (1)

whenever $\varrho(i)=\langle k,\ell\rangle$ with $k>\kappa+1$ then $\ell=1$, and 2. (2)

for all ascending tuples

$\bar{r}_{1}=\langle r_{\langle 1,1\rangle},\ldots,r_{\langle 1,m\rangle}\rangle\in J_{1}^{m};\ldots;\bar{r}_{\kappa+1}=\langle r_{\langle\kappa+1,1\rangle},\ldots,r_{\langle\kappa+1,m\rangle}\rangle\in J_{\kappa+1}^{m}$;

$\bar{r}_{\kappa+2}=\langle r_{\langle\kappa+2,1\rangle}\rangle=\langle q_{1}\rangle;\ldots;\bar{r}_{2\kappa+1}=\langle r_{\langle 2\kappa+1,1\rangle}\rangle=\langle q_{\kappa}\rangle$

we have $\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle\in S$, and 3. (3)

for every tuple $\langle s_{1},\ldots,s_{m}\rangle\in S$ there exist ascending tuples $\bar{r}_{1},\ldots,\bar{r}_{2\kappa+1}$ defined as in (2) such that $\langle s_{1},\ldots,s_{m}\rangle=\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle$.

Consider any $\bar{s},\bar{s}^{\prime}\in S$. By (2), $\bar{s}$ can be written in the form $\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle$ for appropriate values $r_{\langle k,\ell\rangle}$ and $\bar{s}^{\prime}$ can be represented in the form $\langle r^{\prime}_{\varrho(1)},\ldots,r^{\prime}_{\varrho(m)}\rangle$ for appropriate $r^{\prime}_{\langle k,\ell\rangle}$. Lemma 5 entails $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle)=\chi_{\mathcal{A}}(\langle r^{\prime}_{\varrho(1)},\ldots,r^{\prime}_{\varrho(m)}\rangle)=\chi_{\mathcal{A}}(\bar{s}^{\prime})$. ∎

Lemmas 10 and 11 together entail the existence of some ${\mathcal{J}_{\mathcal{A}}}$-uniform model $\mathcal{A}\models N$ with a finite free-sort domain $\mathcal{S}^{\mathcal{A}}$, if $N$ is satisfiable.

Corollary 12**.**

If $N$ has a model, then it has a model $\mathcal{A}$ that is ${\mathcal{J}_{\mathcal{A}}}$-uniform and that interprets the sort $\mathcal{S}$ as some finite set.

Given any interpretation $\mathcal{A}$, the partition ${\mathcal{J}_{\mathcal{A}}}$ of the reals is determined by the rational constants in $N$ and by the values that $\mathcal{A}$ assigns to the base-sort Skolem constants in $N$. Let $d_{1},\ldots,d_{\lambda}$ be all the base-sort Skolem constants in $N$. If we are given some mapping $\gamma:\{d_{1},\ldots,d_{\lambda}\}\to\mathbb{R}$, then $\gamma$ induces a partition ${\mathcal{J}_{\gamma}}$, just as $\mathcal{A}$ induces ${\mathcal{J}_{\mathcal{A}}}$. We can easily verify whether $N$ has a model $\mathcal{B}$ that is compatible with $\gamma$ (i.e. $\mathcal{B}$ assigns the same values to $d_{1},\ldots,d_{\lambda}$) and that is ${\mathcal{J}_{\mathcal{B}}}$-uniform. Due to the uniformity requirement, there is only a finite number of candidate interpretations that have to be checked.

Consequently, in order to show decidability of the satisfiability problem for finite BSR(SLR) clause sets in normal form, the only question that remains to be answered is whether it is sufficient to consider a finite number of assignments $\gamma$ of real values to the Skolem constants in $N$. Recall that since $N$ is in normal form, we can divide $N$ into two disjoint parts $N_{\text{def}}$ and $N^{\prime}$ such that all ground LA terms occurring in $N^{\prime}$ are either (Skolem) constants or rationals. Moreover, every clause in $N_{\text{def}}$ constitutes a definition $c=t$ of some Skolem constant $c$. As far as the LA constraints occurring in $N^{\prime}$ are concerned, the most relevant information regarding the interpretation of Skolem constants is their ordering relative to one another and relative to the occurring rationals. This means, the clauses in $N^{\prime}$ cannot distinguish two assignments $\gamma,\gamma^{\prime}$ if

(a) for every Skolem constant $d_{i}$ and every rational $r$ occurring in $N^{\prime}$ we have (a.1) $\gamma(d_{i})\leq r$ if and only if $\gamma^{\prime}(d_{i})\leq r$, and (a.2) $\gamma(d_{i})\geq r$ if and only if $\gamma^{\prime}(d_{i})\geq r$, and

(b) for all $d_{i},d_{j}$ we have that $\gamma(d_{i})\leq\gamma(d_{j})$ if and only if $\gamma^{\prime}(d_{i})\leq\gamma^{\prime}(d_{j})$.

This observation leads to the following nondeterministic decision procedure for finite BSR(SLR) clause sets in normal form:

1. (1)

Nondeterministically fix a total preorder $\preceq$ (reflexive and transitive) on the set of all base-sort Skolem constants and rational constants occurring in $N^{\prime}$.

Define a clause set $N_{\preceq}$ that enforces $\preceq$ for base-sort Skolem constants, i.e. N_{\preceq}:=\bigl{\{}c>c^{\prime}\,\|\rightarrow\Box\bigm{|}c\preceq c^{\prime}\text{, either c$or$c^{\prime} or both are Skolem constants}\bigr{\}}. 2. (2)

Check whether there is some mapping $\gamma:\{d_{1},\ldots,d_{\lambda}\}\to\mathbb{R}$ such that $\gamma$ is a solution for the clauses in $N_{\text{def}}\cup N_{\preceq}$. (This step relies on the fact that linear arithmetic over existentially quantified variables is decidable.) 3. (3)

If such an assignment $\gamma$ exists, define an interpretation $\mathcal{B}$ as follows.

1. (3.1)

Nondeterministically define $\mathcal{S}^{\mathcal{B}}$ to be some subset of $\text{{fconsts}}(N)$, i.e. use a subset of the Herbrand domain with respect to the free sort $\mathcal{S}$. 2. (3.2)

For every $e\in\text{{fconsts}}(N)$ nondeterministically pick some ${a}\in\mathcal{S}^{\mathcal{B}}$ and set $e^{\mathcal{B}}:={a}$. 3. (3.3)

Set $d_{i}^{\mathcal{B}}:=\gamma(d_{i})$ for every $d_{i}$. 4. (3.4)

For every uninterpreted predicate symbol $P$ occurring in $N$ nondeterministically define the set $P^{\mathcal{B}}$ in such a way that $\mathcal{B}$ is ${\mathcal{J}_{\mathcal{B}}}$-uniform. 4. (4)

Check whether $\mathcal{B}$ is a model of $N$.

Theorem 13**.**

Satisfiability of finite BSR(SLR) clause sets is decidable.

5 Decidability of satisfiability for BSR(BD) clause sets

Similarly to the previous section, we fix some finite BSR(BD) clause set $N$ in normal form for the rest of this section, and we assume that all uninterpreted predicate symbols $P$ occurring in $N$ have the sort $P:\mathcal{S}^{m^{\prime}}\times\mathcal{R}^{m}$. Moreover, we assume that all base-sort constants in $N$ are integers. This does not lead to a loss of generality, as we could multiply all rational constants with the least common multiple of their denominators to obtain an equisatisfiable clause set in which all base-sort constants are integers. We could even allow Skolem constants, if we added clauses stipulating that every such constant is assigned a value that is (a) an integer and (b) is bounded from above and below by some integer bounds. For the sake of simplicity, however, we do not consider Skolem constants here.

Our general approach to decidability of the satisfiability problem for finite BSR(BD) clause sets is very similar to the path taken in the previous section. Due to the nature of the LA constraints in BSR(BD) clause sets, the employed equivalence relation characterizing indistinguishable tuples has to be a different one. In fact, we use one equivalence relation $\mathrel{\widehat{\simeq}}_{\kappa}$ on the unbounded space $\mathbb{R}^{m}$ and another equivalence relation $\simeq_{\kappa}$ on the subspace $(-\kappa-1,\kappa+1)^{m}$ for some positive integer $\kappa$. Our definition of the relations $\simeq_{\kappa}$ and $\mathrel{\widehat{\simeq}}_{\kappa}$ is inspired by the notion of clock equivalence used in the context of timed automata (see, e.g., [1]).

Definition 14** (bounded region equivalence $\simeq_{\kappa}$).**

Let $\kappa$ be a positive integer. We define the equivalence relation $\simeq_{\kappa}$ on $(-\kappa-1,\kappa+1)^{m}$ such that we get $\langle r_{1},\ldots,r_{m}\rangle\simeq_{\kappa}\langle s_{1},\ldots,s_{m}\rangle$ if and only if the following conditions are met:

(i) For every $i$ we have $\lfloor r_{i}\rfloor=\lfloor s_{i}\rfloor$, and $\text{fr}(r_{i})=0$ if and only if $\text{fr}(s_{i})=0$.

(ii) For all $i,j$ we have $\text{fr}(r_{i})\leq\text{fr}(r_{j})$ if and only if $\text{fr}(s_{i})\leq\text{fr}(s_{j})$.

The relation $\simeq_{\kappa}$ induces only a finite number of equivalence classes over $(-\kappa-1,\kappa+1)^{m}$. Over $\mathbb{R}^{m}$, on the other hand, an analogous equivalence relation $\simeq_{\infty}$ would lead to infinitely many equivalence classes. In order to overcome this problem and obtain an equivalence relation over $\mathbb{R}^{m}$ that induces only a finite number of equivalence classes, we use the following compromise.

Definition 15** (unbounded region equivalence $\mathrel{\widehat{\simeq}}_{\kappa}$).**

Let $\kappa$ be a positive integer. We define the equivalence relation $\mathrel{\widehat{\simeq}}_{\kappa}$ on $\mathbb{R}^{m}$ in such a way that

$\langle r_{1},\ldots,r_{m}\rangle\mathrel{\widehat{\simeq}}_{\kappa}\langle s_{1},\ldots,s_{m}\rangle$ holds if and only if

(i) for every $i$ either $r_{i}>\kappa$ and $s_{i}>\kappa$, or $r_{i}<-\kappa$ and $s_{i}<-\kappa$, or the following conditions are met: (i.i) $\lfloor r_{i}\rfloor=\lfloor s_{i}\rfloor$ and (i.ii) $\text{fr}(r_{i})=0$ if and only if $\text{fr}(s_{i})=0$, and (ii) for all $i,j$

(ii.i) if $r_{i},r_{j}>\kappa$ or $r_{i},r_{j}<-\kappa$, then $r_{i}\leq r_{j}$ if and only if $s_{i}\leq s_{j}$,

(ii.ii) if $-\kappa\leq r_{i},r_{j}\leq\kappa$, then $\text{fr}(r_{i})\leq\text{fr}(r_{j})$ if and only if $\text{fr}(s_{i})\leq\text{fr}(s_{j})$.

Obviously, the equivalence relations $\simeq_{\kappa}$ and $\mathrel{\widehat{\simeq}}_{\kappa}$ coincide on the subspace $(-\kappa,\kappa)^{m}$. Over $(-\kappa-1,\kappa+1)^{m}$ the relation $\simeq_{\kappa}$ constitutes a proper refinement of $\mathrel{\widehat{\simeq}}_{\kappa}$. Figure 1 depicts the equivalence classes induced by $\simeq_{\kappa}$ and $\mathrel{\widehat{\simeq}}_{\kappa}$ in a two-dimensional setting for $\kappa=1$. We need both relations in our approach.

Definition 16** ($\simeq_{\kappa}$-uniform and $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform interpretations).**

Let $\kappa$ be a positive integer. Consider a interpretation $\mathcal{A}$. We call $\mathcal{A}$ $\simeq_{\kappa}$-uniform if its corresponding coloring $\chi_{\mathcal{A}}$ (cf. Definition 8) colors each $\simeq_{\kappa}$-equivalence class over $(-\kappa-1,\kappa+1)^{m}$ uniformly, i.e. for all tuples $\bar{q},\bar{q}^{\prime}\in(-\kappa-1,\kappa+1)^{m}$ with $\bar{q}\simeq_{\kappa}\bar{q}^{\prime}$ we have $\chi_{\mathcal{A}}(\bar{q})=\chi_{\mathcal{A}}(\bar{q}^{\prime})$. We call $\mathcal{A}$ $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform if $\chi_{\mathcal{A}}$ colors each $\simeq_{\kappa}$-equivalence class over $\mathbb{R}^{m}$ uniformly.

The parameter $\kappa$ will be determined by the base-sort constant in $N$ with the largest absolute value. If $\kappa$ is defined in this way, one can show that the LA constraints occurring in $N$ cannot distinguish between two $\mathrel{\widehat{\simeq}}_{\kappa}$-equivalent $m$-tuples of reals. This observation is crucial for the proof of Lemma 17.

In order to prove the existence of $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform models for satisfiable $N$, we start from some model $\mathcal{A}$ of $N$ and rely on the existence of a certain finite set $Q\subseteq[0,1)$ of fractional parts. This set $Q$ can be extended to a set $\widehat{Q}\subseteq(-\kappa-1,\kappa+1)$ by addition of the fractional parts in $Q$ with integral parts $k$ from the range $-\kappa-1\leq k\leq\kappa$. Hence, $\widehat{Q}$ contains $2(\kappa+1)\cdot|Q|$ reals. We assume that all $\simeq_{\kappa}$-equivalent tuples $\bar{s},\bar{s}^{\prime}$ from $\widehat{Q}^{m}$ are treated uniformly by $\mathcal{A}$. Put differently, we require $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\bar{s}^{\prime})$. We choose to formulate this requirement with respect to $\simeq_{\kappa}$ because of the more regular structure of its equivalence classes, which facilitates a more convenient way of invoking Lemma 4. Due to the fact that $\simeq_{\kappa}$ constitutes a refinement of $\mathrel{\widehat{\simeq}}_{\kappa}$ on the subspace $(-\kappa-1,\kappa+1)^{m}$, and since for every $\mathrel{\widehat{\simeq}}_{\kappa}$-equivalence class $\widehat{S}$ over $\mathbb{R}^{m}$ there is some $\simeq_{\kappa}$-equivalence class $S\subseteq(-\kappa-1,\kappa+1)^{m}$ such that $S\subseteq\widehat{S}$, we can use the color $\chi_{\mathcal{A}}(\bar{r})$ of representative $m$-tuples $\bar{r}$ constructed from $\widehat{Q}$ to serve as a blueprint when constructing a $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform model $\mathcal{B}$.

Lemma 17**.**

Let $\lambda$ be the maximal number of distinct base-sort variables in any single clause in $N$; in case of $\lambda<m$, we set $\lambda:=m$. Let $\mathcal{A}$ be a model of $N$. Let $\kappa$ be the maximal absolute value of any rational occurring in $N$; in case this value is zero, we set $\kappa:=1$. Suppose we are given a finite set $Q\subseteq[0,1)$ of cardinality $\lambda+1$ such that $0\in Q$ and for all tuples $\bar{r},\bar{s}\in\widehat{Q}^{m}$, $\bar{r}\simeq_{\kappa}\bar{s}$ entails $\chi_{\mathcal{A}}(\bar{r})=\chi_{\mathcal{A}}(\bar{s})$, where

\widehat{Q}:=\bigl{\{}q+k\bigm{|}q\in Q\text{ and }k\in\{-\kappa-1,\ldots,0,\ldots,\kappa\}\bigr{\}}.

Then we can construct a model $\mathcal{B}$ of $N$ that is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform and that interprets the free sort $\mathcal{S}$ as a finite set.

Proof sketch.

The construction of $\mathcal{B}$ from $\mathcal{A}$ is similar to the construction of uniform models outlined in the proof of Lemma 10.

Claim I: Let $\mu$ be a positive integer with $\mu\leq\lambda$. For every $\mathrel{\widehat{\simeq}}_{\kappa}$-equivalence class $S$ over $\mathbb{R}^{\mu}$ and every $\bar{r}\in S$ there is some $\bar{q}\in S\cap\widehat{Q}^{\mu}$ such that $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}$ and for all $i_{1},i_{2},i_{3}$ with $r_{i_{1}}<-\kappa$ and $r_{i_{2}}>\kappa$ and $-\kappa\leq r_{i_{3}}\leq\kappa$ we have $\text{fr}(q_{i_{1}})<\text{fr}(q_{i_{2}})<\text{fr}(q_{i_{3}})$. $\Diamond$

Let $\widehat{\mathcal{S}}$ denote the set \{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}}$for some$c\in\text{{fconsts}}(N)}\}. We construct the interpretation $\mathcal{B}$ as follows: $\mathcal{S}^{\mathcal{B}}:=\widehat{\mathcal{S}}$; $c^{\mathcal{B}}:=c^{\mathcal{A}}$ for every constant symbol $c$; for every uninterpreted predicate symbol $P$ occurring in $N$ and for all tuples $\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$ and $\bar{r}\in\mathbb{R}^{m}$ we pick some tuple $\bar{q}\in\widehat{Q}^{m}$ in accordance with Claim I—i.e. $\bar{q}$ satisfies $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}$—and define $P^{\mathcal{B}}$ in such a way that $\langle\bar{a},\bar{r}\rangle\in P^{\mathcal{B}}$ if and only if $\langle\bar{a},\bar{q}\rangle\in P^{\mathcal{A}}$.

Claim II: The interpretation $\mathcal{B}$ is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform. $\Diamond$

It remains to show $\mathcal{B}\models N$. We use the same approach as in the proof for Lemma 10, this time based on the equivalence relation $\mathrel{\widehat{\simeq}}_{\kappa}$ instead of $\sim_{\mathcal{J}_{\mathcal{A}}}$. ∎

We employ Lemma 4 to prove the existence of the set $Q$ used in Lemma 17.

Lemma 18**.**

Let $\mathcal{A}$ be an interpretation and let $\kappa,\lambda$ be positive integers with $\lambda\geq m$. There exists a finite set $Q\subseteq[0,1)$ of cardinality $\lambda+1$ such that $0\in Q$ and for all tuples $\bar{s},\bar{s}^{\prime}\in\widehat{Q}^{m}$, $\bar{s}\simeq_{\kappa}\bar{s}^{\prime}$ entails $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\bar{s}^{\prime})$, where

\widehat{Q}:=\bigl{\{}q+k\bigm{|}q\in Q\text{ and }k\in\{-\kappa-1,\ldots,0,\ldots,\kappa\}\bigr{\}}.

Proof sketch.

One can show that every $\simeq_{\kappa}$-equivalence class $S$ over $(-\kappa-1,\kappa+1)^{m}$ can be represented by a pair of mappings $\varrho:[m]\to\{0,1,\ldots,m\}$ and $\sigma:[m]\to\{-\kappa-1,\ldots,0,\ldots,\kappa\}$ such that

(i) for any ascending tuple $\langle r_{0},r_{1},\ldots,r_{m}\rangle\in[0,1)^{m+1}$ with $r_{0}=0$ we have \bigl{\langle}r_{\varrho(1)}+\sigma(1),\ldots,r_{\varrho(m)}+\sigma(m)\bigr{\rangle}\in S, and

(ii) for every tuple $\langle s_{1},\ldots,s_{m}\rangle\in S$ there is an ascending tuple $\langle r_{0},r_{1},\ldots,r_{m}\rangle\in[0,1)^{m+1}$ with $r_{0}=0$ such that \bigl{\langle}s_{1},\ldots,s_{m}\bigr{\rangle}=\bigl{\langle}r_{\varrho(1)}+\sigma(1),\ldots,r_{\varrho(m)}+\sigma(m)\bigr{\rangle}.

Having an enumeration $\langle\varrho_{1},\sigma_{1}\rangle,\ldots,\langle\varrho_{k},\sigma_{k}\rangle$ of pairs of such mappings in which every $\simeq_{\kappa}$-equivalence class over $(-\kappa-1,\kappa+1)^{m}$ is represented, we construct a coloring \widehat{\chi}:\mathbb{R}^{m}\to\bigl{(}\mathcal{P}\{P_{i}\bar{a}\mid\text{\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$and$P_{i}$occurs in$N}\}\bigr{)}^{k} by setting

[TABLE]

for every tuple $\bar{r}=\langle r_{1},\ldots,r_{m}\rangle\in(0,1)^{m}$, where we define $r_{0}$ to be [math]. By virtue of Lemma 4, there is a set $Q^{\prime}\subseteq(0,1)$ of cardinality $\lambda$ such that all ascending tuples $\langle r_{1},\ldots,r_{m}\rangle\in{Q^{\prime}}^{m}$ are assigned the same color by $\chi$. Then $Q:=Q^{\prime}\cup\{0\}$ is the sought set. ∎

Lemmas 17 and 18 together entail the existence of $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform models for finite satisfiable BSR(BD) clause sets, where $\kappa$ is defined as in Lemma 17.

Corollary 19**.**

Let $\kappa$ be defined as in Lemma 17. If $N$ is satisfiable, then it has a model $\mathcal{A}$ that is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform and that interprets the sort $\mathcal{S}$ as some finite set.

By virtue of Corollary 19, we can devise a nondeterministic decision procedure for finite BSR(BD) clause sets $N$. We adapt the decision procedure for BSR(SLR) as follows. Since base-sort Skolem constants do not occur in $N$, Steps (1), (2), and 3(3.3) are skipped. Moreover, Step 3(3.4) has to be modified slightly. The interpretations of uninterpreted predicate symbols need to be constructed in such a way that the candidate interpretation $\mathcal{B}$ is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform for \kappa:=\max\bigl{(}\{1\}\cup\{|c|\bigm{|}c\in\text{{bconsts}}(N)\}\bigr{)}.

Theorem 20**.**

Satisfiability of finite BSR(BD) clause sets is decidable.

6 Formalizing reachability for timed automata

In this section we show that reachability for timed automata (cf. [1]) can be formalized using finite BSR(BD) clause sets. In what follows, we fix a finite sequence $\bar{x}$ of pairwise distinct clock variables that range over the reals. For convenience, we occasionally treat $\bar{x}$ as a set and use set notation such at $x\in\bar{x}$, $|\bar{x}|$, and $\mathcal{P}(\bar{x})$. A clock constraint over $\bar{x}$ is a finite conjunction of LA constraints of the form true, $x\mathrel{\triangleleft}c$, or $x-y\mathrel{\triangleleft}c$, where $x,y\in\bar{x}$, $c$ is an integer and $\mathrel{\triangleleft}{\in}\{<,\leq,=,\neq,\geq,>\}$. We denote the set of all clock constraints over $\bar{x}$ by $\text{{cc}}(\bar{x})$. A timed automaton is a tuple $\langle\text{{Loc}},\ell_{0},\bar{x},$ $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$, where Loc is a finite set of locations; $\ell_{0}\in\text{{Loc}}$ is the initial location; $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}}$ is a family of clock constraints from $\text{{cc}}(\bar{x})$ where each $\text{{inv}}_{\ell}$ describes the invariant at location $\ell$; $\mathcal{T}\subseteq\text{{Loc}}\times\text{{cc}}(\bar{x})\times\mathcal{P}(\bar{x})\times\text{{Loc}}$ is the location transition relation within the automaton, including guards with respect to clocks and the set of clocks that are being reset when the transition is taken.

Although the control flow of a timed automaton is described by finite means, the fact that clocks can assume uncountably many values yields an infinite state space, namely, $\text{{Loc}}\times[0,\infty)^{|\bar{x}|}$. Transitions between states fall into two categories:

delay transitions $\langle\ell,\bar{r}\rangle\hookrightarrow\langle\ell,\bar{r}^{\prime}\rangle$ with $\bar{r}^{\prime}=\bar{r}+t$ for some $t\geq 0$ and

$[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models\text{{inv}}_{\ell}[\bar{x}^{\prime}]$; and

location transitions $\langle\ell,\bar{r}\rangle\hookrightarrow\langle\ell^{\prime},\bar{r}^{\prime}\rangle$ for some $\langle\ell,g,Z,\ell^{\prime}\rangle\!\in\!\mathcal{T}$ with $[\bar{x}{\mathop{\mapsto}}\bar{r}]\models g[\bar{x}]$,

$\bar{r}^{\prime}=\bar{r}[Z\mapsto 0]$, and $[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models\text{{inv}}_{\ell^{\prime}}[\bar{x}^{\prime}]$.

The operation $\bar{r}^{\prime}:=\bar{r}+t$ is defined by setting $r^{\prime}_{i}:=r_{i}+t$ for every $i$, and $\bar{r}^{\prime}:=\bar{r}[Z\mapsto 0]$ means that $r^{\prime}_{i}=0$ for every $x_{i}\in Z$ and $r^{\prime}_{i}=r_{i}$ for every $x_{i}\not\in Z$.

In [6] Fietzke and Weidenbach present an encoding of reachability for a given timed automaton $\mathbf{A}$ in terms of first-order logic modulo linear arithmetic.

Definition 21** (FOL(LA) encoding of a timed automaton, [6]).**

Given a timed automaton $\mathbf{A}:=\langle\text{{Loc}},\ell_{0},\bar{x},\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$, the FOL(LA) encoding of $\mathbf{A}$ is the following clause set $N_{\mathbf{A}}$, where Reach is a $(1+|\bar{x}|)$-ary predicate symbol:

the initial clause \bigwedge_{x\in\bar{x}}x=0\;\;\wedge\;\;\text{{inv}}_{\ell_{0}}[\bar{x}]\;\bigm{\|}\;\rightarrow\text{{Reach}}(\ell_{0},\bar{x});

delay clauses $z\geq 0\;\;\wedge\;\;\bigwedge_{x\in\bar{x}}x^{\prime}=x+z\;\wedge\;\text{{inv}}_{\ell}[\bar{x}^{\prime}]$

                                      \bigm{\|}\;\text{{Reach}}(\ell,\bar{x})\rightarrow\text{{Reach}}(\ell,\bar{x}^{\prime})

for every location $\ell\in\text{{Loc}}$;

[TABLE]

Corollary 4.3 in [6] states that for any model of $N_{\mathbf{A}}$, every location $\ell\in\text{{Loc}}$, and every tuple $\bar{r}\in\mathbb{R}^{|\bar{x}|}$ we have $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r}]\models\text{{Reach}}(\ell,\bar{x})$ if and only if $\mathbf{A}$ can reach the state $\langle\ell,\bar{r}\rangle$ from its initial configuration.

Given any clock constraint $\psi\in\text{{cc}}(\bar{x})$ and some location $\ell$, the timed automaton $\mathbf{A}$ can reach at least one of the states $\langle\ell,\bar{r}\rangle$ with $[\bar{x}{\mathop{\mapsto}}\bar{r}]\models\psi[\bar{x}]$ from its initial configuration if and only if the clause set N_{\mathbf{A}}\cup\bigl{\{}\psi[\bar{x}]\,\|\,\text{{Reach}}(\ell,\bar{x})\rightarrow\Box\bigr{\}} is unsatisfiable (cf. Proposition 4.4 in [6]).

Next, we argue that the passage of time does not have to be formalized as a synchronous progression of all clocks. Instead, it is sufficient to require that clocks progress in such a way that their valuations do not drift apart excessively.

Lemma 22**.**

Consider any delay clause

C:=\quad z\geq 0\;\;\wedge\;\;\bigwedge_{x\in\bar{x}}x^{\prime}=x+z\;\;\wedge\;\;\text{{inv}}_{\ell}[\bar{x}^{\prime}]\;\bigm{\|}\;\text{{Reach}}(\ell,\bar{x})\rightarrow\text{{Reach}}(\ell,\bar{x}^{\prime})

that belongs to the FOL(LA) encoding of some timed automaton $\mathbf{A}:=\langle\text{{Loc}},\ell_{0},\bar{x},$ $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$. Let $\lambda$ be some positive integer. Let $M$ be a finite clause set corresponding to the following formula

[TABLE]

For every $\simeq_{\lambda}$-uniform interpretation $\mathcal{A}$ we have $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models C$ for all tuples $\bar{r},\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ if and only if $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]\models M$ holds for all tuples $\bar{q},\bar{q}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$.

Our approach to decidability of BSR(BD)-satisfiability exploits the observation that the allowed constraints cannot distinguish between tuples from one and the same equivalence class with respect to $\mathrel{\widehat{\simeq}}_{\lambda}$, which induces only a finite number of such classes. Decidability of the reachability problem for timed automata can be argued in a similar fashion, using a suitable equivalence relation on clock valuations [1]. We refer to the induced classes of indistinguishable clock valuations over $\mathbb{R}^{|x|}$, which are induced by a given timed automaton $\mathbf{A}=\langle\text{{Loc}},\ell_{0},\bar{x},$ $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$, as TA regions of $\mathbf{A}$.

In order to decide reachability for $\mathbf{A}$, it is sufficient to consider a bounded subspace of $\mathbb{R}^{|\bar{x}|}$. More precisely, there exists a computable integer $\lambda$, depending on the number of clocks $|\bar{x}|$ and the constants occurring in clock constraints in $\mathbf{A}$, such that any valuation $\bar{r}$ of $\mathbf{A}$’s clocks can be projected to some valuation $\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ that $\mathbf{A}$ cannot distinguish from $\bar{r}$ (see Section A.4). In the subspace $[0,\lambda+1)^{|\bar{x}|}$, $\mathbf{A}$’s TA regions coincide with (finite unions of) equivalence classes with respect to $\simeq_{\lambda}$. In fact, the quotient $[0,\lambda+1)^{|\bar{x}|}/_{\simeq_{\lambda}}$ constitutes a refinement of the division of $[0,\lambda+1)^{|\bar{x}|}$ into TA regions. Since any pair $\langle\ell,\bar{r}\rangle$ with $\bar{r}\in R$ for some TA region $R$ is reachable if and only if all pairs $\langle\ell,\bar{r}^{\prime}\rangle$ with $\bar{r}\in R$ are reachable, any minimal model $\mathcal{A}$ of the encoding $N_{\mathbf{A}}$ is $\simeq_{\lambda}$-uniform (where minimality of $\mathcal{A}$ refers to the minimality of the set $\text{{Reach}}^{\mathcal{A}}$ with respect to set inclusion). This is why Lemma 22 may focus on $\simeq_{\lambda}$-uniform models.

Theorem 23**.**

The reachability problem for a given timed automaton can be expressed in terms of satisfiability of a finite BSR(BD) clause set.

Appendix A Appendix

A.1 Details Concerning Section 3

Proof of Lemma 5

We start with two auxiliary results.

Lemma 24**.**

Let $n,m,p>0$ be positive integers and let $\chi:\mathbb{R}^{mp}\to\mathcal{C}$ be an arbitrary coloring. Let $R_{1},\ldots,R_{p}$ be sufficiently large but finite subsets of $\mathbb{R}$.

There exist subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p}\subseteq R_{p}$, each of cardinality $n$, such that for all ascending tuples $\bar{r}_{1}\in Q_{1}^{m},\ldots,\bar{r}_{p}\in Q_{p}^{m}$ the colors $\chi(\bar{r}_{1},\ldots,\bar{r}_{p})$ are the same.

adaptation of the proof of Theorem 5 on page 113 in [8].

As in the proof of Lemma 4, we assume $n\geq m$. We proceed by induction on $p\geq 1$.

The case $p=1$ is covered by Lemma 4.

Suppose $p>1$. We define an equivalence relation $\sim_{p}$ on the set $R_{p}^{m}$ so that $\bar{s}\sim_{p}\bar{s}^{\prime}$ holds if and only if for all ascending tuples $\bar{r}_{1}\in R_{1}^{m},\ldots,\bar{r}_{p-1}\in R_{p-1}^{m}$ the colors \chi\bigl{(}\bar{r}_{1},\ldots,\bar{r}_{p-1},\bar{s}\bigr{)} and \chi\bigl{(}\bar{r}_{1},\ldots,\bar{r}_{p-1},\bar{s}^{\prime}\bigr{)} are identical. This equivalence relation partitions $R_{p}^{m}$ into at most $|\mathcal{C}|^{{{|R_{1}|}\choose{m}}\cdot\ldots\cdot{{|R_{p-1}|}\choose{m}}}$ equivalence classes. It thus induces a coloring of $\chi^{\prime}:R_{p}^{m}\to\mathcal{C}^{\prime}_{p}$ with one color for each equivalence class.

By virtue of Lemma 4, we can construct a subset $Q_{p}\subseteq R_{p}$ with $n$ elements such that all ascending $m$-tuples $\bar{r}\in Q_{p}^{m}$ are colored identically by $\chi^{\prime}$.

Let the coloring $\chi^{\prime\prime}$ be defined by $\chi^{\prime\prime}(\bar{r}_{1},\ldots,\bar{r}_{p-1}):=\chi(\bar{r}_{1},\ldots,\bar{r}_{p-1},\bar{s})$ for some fixed ascending $m$-tuple $\bar{s}\in Q_{p}^{m}$. By induction, we find subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p-1}\subseteq R_{p-1}$, each containing $n$ elements, such that for all ascending $m$-tuples $\bar{r}_{1}\in R_{1}^{m},\ldots,\bar{r}_{p-1}\in R_{p-1}^{m}$ the colors $\chi^{\prime\prime}(\bar{r}_{1},\ldots,\bar{r}_{p-1})$ are identical.

But then the definition of $\chi^{\prime\prime}$ and $\chi^{\prime}$ entail that the sets $Q_{1},\ldots,Q_{p}$ satisfy the requirements posed by the lemma. ∎

Recall that we write $[k]$ to address the set $\{1,\ldots,k\}$ for any positive integer $k>0$.

Lemma 25**.**

Let $n,m,p>0$ be positive integers, let $\kappa\geq 0$ be a nonnegative integer and let $\chi:\mathbb{R}^{m}\to\mathcal{C}$ be an arbitrary coloring. Let $R_{1},\ldots,R_{p}$ be sufficiently large but finite subsets of $\mathbb{R}$. Let $q_{1},\ldots,q_{\kappa}$ be fixed reals. Let $\varrho:[m]\to[p+\kappa]\times[m]$ be some mapping such that $\varrho(i)=\langle k,\ell\rangle$ with $k>p$ implies $\ell=1$.

There exist subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p}\subseteq R_{p}$, each of cardinality $n$, such that for all ascending tuples

[TABLE]

and the reals $r_{\langle p+1,1\rangle}:=q_{1},\dots,r_{\langle p+\kappa,1\rangle}:=q_{\kappa}$ the colors $\chi(\bar{r}_{\varrho(1)},\ldots,\bar{r}_{\varrho(m)})$ are the same.

Proof.

We again assume $n\geq m$. We define a new coloring $\chi^{\prime}:\mathbb{R}^{mp}\to\mathcal{C}$ by

[TABLE]

for every $mp$-tuple $\langle\bar{r}_{1},\ldots,\bar{r}_{p}\rangle\in R_{1}^{m}\times\ldots\times R_{p}^{m}$ with ascending $\bar{r}_{1},\ldots,\bar{r}_{p}$. By Lemma 24, there exist subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p}\subseteq R_{p}$, each with $n$ elements, such that for all ascending tuples $\bar{r}_{1}\in Q_{1}^{m},\ldots,\bar{r}_{p}\in Q_{p}^{m}$ the colors $\chi^{\prime}(\bar{r}_{1},\ldots,\bar{r}_{p})$ are the same. By definition of $\chi^{\prime}$, the sets $Q_{1},\ldots,Q_{p}$ satisfy the requirements of the lemma. ∎

Now we have the right tools at hand to prove Lemma 5

Lemma**.**

Let $n,m,p>0$ be positive integers, let $K\geq 0$ be a nonnegative integer and let $\chi:\mathbb{R}^{m}\to\mathcal{C}$ be an arbitrary coloring. Let $R_{1},\ldots,R_{p}$ be sufficiently large but finite subsets of $\mathbb{R}$. Let $q_{1},\ldots,q_{K}$ be fixed reals. Let $\varrho_{1},\ldots,\varrho_{L}$ be some enumeration of all mappings $\varrho_{j}:[m]\to[p+K]\times[m]$ for which $\varrho_{j}(i)=\langle k,\ell\rangle$ with $k>p$ entails $\ell=1$. There exist subsets $Q_{1}\subseteq R_{1},\ldots,Q_{p}\subseteq R_{p}$, each of cardinality $n$, such that for all ascending tuples $\bar{r}_{1},\bar{r}^{\prime}_{1}\in Q_{1}^{m},\ldots,\bar{r}_{p},\bar{r}^{\prime}_{p}\in Q_{p}^{m}$ and the reals $r_{\langle p+1,1\rangle}:=q_{1},\dots,r_{\langle p+K,1\rangle}:=q_{K}$ and every index $j$, $1\leq j\leq L$, we have

\chi\bigl{(}r_{\varrho_{j}(1)},\ldots,r_{\varrho_{j}(m)}\bigr{)}=\chi\bigl{(}r^{\prime}_{\varrho_{j}(1)},\ldots,r^{\prime}_{\varrho_{j}(m)}\bigr{)}.

Proof.

We again assume $n\geq m$. We construct sequences of subsets $S_{\ell,0}\supseteq\ldots\supseteq S_{\ell,L}$ for every $\ell$, $1\leq\ell\leq p$, such that

• •

$S_{\ell,0}=R_{\ell}$, and

• •

$S_{\ell,j+1}\subseteq S_{\ell,j}$ is a subset of sufficient cardinality that is constructed by application of Lemma 25 for $\varrho:=\varrho_{j+1}$, i.e.  for all ascending tuples

[TABLE]

the colors $\chi(\bar{s}_{\varrho_{j+1}(1)},\ldots,\bar{s}_{\varrho_{j+1}(m)})$ are the same.

Then the sets $S_{1,L},\ldots,S_{p,L}$ are the sought $Q_{1},\ldots,Q_{p}$. ∎

A.2 Details Concerning Section 4

Proof of Lemma 10

Lemma**.**

Let $\lambda$ be the maximal number of distinct base-sort variables in any single clause in $N$ but at least $m$, i.e. \lambda:=\max\bigl{(}\{m\}\cup\bigl{\{}|\text{{vars}}(C)\cap V_{\mathcal{R}}|\bigm{|}C\in N\bigr{\}}\bigr{)}. Let $\mathcal{A}$ be a model of $N$. Let $J_{0},\ldots,J_{\kappa}$ be an enumeration of all open intervals in ${\mathcal{J}_{\mathcal{A}}}$ so that $J_{0}<\ldots<J_{\kappa}$. Suppose we are given a collection of finite sets $Q_{0},\ldots,Q_{\kappa}$ possessing the following properties,

1. (i)

$Q_{i}\subseteq J_{i}$ and $|Q_{i}|=\lambda$ for every $i$, $0\leq i\leq\kappa$. 2. (ii)

Let $Q:=\bigcup_{i}Q_{i}\cup\{c^{\mathcal{A}}\mid c\in\text{{bconsts}}(N)\}$. For all ${\mathcal{J}_{\mathcal{A}}}$-equivalent $m$-tuples $\bar{q},\bar{q}^{\prime}\in Q^{m}$ we have $\chi_{\mathcal{A}}(\bar{q})=\chi_{\mathcal{A}}(\bar{q}^{\prime})$.

Then we can construct a model $\mathcal{B}$ of $N$ that is ${\mathcal{J}_{\mathcal{B}}}$-uniform and that interprets the free sort $\mathcal{S}$ as a finite set. Moreover, $\mathcal{B}$ interprets all constant symbols in $N$ exactly as $\mathcal{A}$ does.

Proof.

Claim I: Let $\mu$, $1\leq\mu\leq,\lambda$ be a positive integer. For each of the finitely many equivalence classes in $\mathbb{R}^{\mu}/_{\sim_{\mathcal{J}_{\mathcal{A}}}}$, we find a representative lying in $Q^{\mu}$.

Proof: Given an equivalence class $[\bar{r}]_{\sim_{\mathcal{J}_{\mathcal{A}}}}\in\mathbb{R}^{\mu}/_{\sim_{\mathcal{J}_{\mathcal{A}}}}$, we define the following ascending sequences for every $i$, $0\leq i\leq\kappa$,

• •

$s_{i,1}<\ldots<s_{i,k_{i}}$, where the values $s_{i,j}$ are the reals in $\bar{r}$ that stem from $J_{i}$, enumerated in ascending order, and

• •

$q_{i,1}<\ldots<q_{i,\lambda}$, which comprises all reals in $Q_{i}$ in ascending order.

In every $Q_{i}\subseteq J_{i}$ we find $\lambda\geq\mu\geq k_{i}$ distinct reals.

We can now construct a tuple $\bar{q}^{\prime}\in[\bar{r}]_{\sim_{\mathcal{J}_{\mathcal{A}}}}\cap Q^{\mu}$ by setting

[TABLE]

for every $\ell$, $1\leq\ell\leq\mu$. Clearly, $\bar{r}$ and $\bar{q}^{\prime}$ are ${\mathcal{J}_{\mathcal{A}}}$-equivalent. $\Diamond$

We construct the interpretation $\mathcal{B}$ as follows, where $\widehat{\mathcal{S}}$ denotes the set \{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}} for some} $c\in\text{{fconsts}}(N)\}$:

• •

$\mathcal{S}^{\mathcal{B}}:=\widehat{\mathcal{S}}$,

• •

for every constant symbol $c$ occurring in $N$ we set $c^{\mathcal{B}}:=c^{\mathcal{A}}$,

• •

for every uninterpreted predicate symbol $P$ occurring in $N$ and for all tuples $\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$ and $\bar{r}\in\mathbb{R}^{m}$ we pick some tuple $\bar{q}\in Q^{m}$ which is ${\mathcal{J}_{\mathcal{A}}}$-equivalent to $\bar{r}$, and we define $P^{\mathcal{B}}$ so that

[TABLE]

Claim II: The interpretation $\mathcal{B}$ is ${\mathcal{J}_{\mathcal{B}}}$-uniform.

Proof: By construction of $\mathcal{B}$ and by requirement (ii). $\Diamond$

We next show $\mathcal{B}\models N$. Consider any clause $C=\Lambda\;\|\;\Gamma\to\Delta$ in $N$ and let $\beta$ be any variable assignment ranging over $\mathcal{S}^{\mathcal{B}}\cup\mathbb{R}$. Starting from $\beta$, we derive a special variable assignment $\widehat{\beta}_{C}$ as follows. Let $x_{1},\ldots,x_{\lambda_{C}}$ be an enumeration of all base-sort variables in $C$. By Claim I, there is some tuple $\langle q_{1},\ldots,q_{\lambda_{C}}\rangle\in Q^{\lambda_{C}}$ such that \langle q_{1},\ldots,q_{\lambda_{C}}\rangle\sim_{\mathcal{J}_{\mathcal{A}}}\bigl{\langle}\beta(x_{1}),\ldots,\beta(x_{\lambda_{C}})\bigr{\rangle}. We define $\widehat{\beta}_{C}(x_{i}):=q_{i}$ for every $i$, $1\leq i\leq\lambda_{C}$. For all other base-sort variables, $\widehat{\beta}_{C}$ can be defined arbitrarily. For every free-sort variable $u$ we set $\widehat{\beta}_{C}(u):=\beta(u)$. We observe

(*)\qquad\bigl{\langle}\beta(x_{1}),\ldots,\beta(x_{\lambda_{C}})\bigr{\rangle}\sim_{\mathcal{J}_{\mathcal{B}}}\bigl{\langle}\widehat{\beta}_{C}(x_{1}),\ldots,\widehat{\beta}_{C}(x_{\lambda_{C}})\bigr{\rangle}.

As $\mathcal{A}$ is a model of $N$, we get $\mathcal{A},\widehat{\beta}_{C}\models C$. By case distinction on why $\mathcal{A},\widehat{\beta}_{C}\models C$ holds, we can infer $\mathcal{B},\beta\models C$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models t\mathrel{\triangleleft}t^{\prime}$ for some atomic LA constraint $t\mathrel{\triangleleft}t^{\prime}$ in $\Lambda$, where $t,t^{\prime}$ are constant symbols or base-sort variables. Since $\mathcal{B}$ and $\mathcal{A}$ interpret constant symbols in the same way and due to $(*)$, we conclude $\mathcal{B},\beta\not\models t\mathrel{\triangleleft}t^{\prime}$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models t\approx t^{\prime}$ for some free-sort equation $t\approx t^{\prime}\in\Gamma$. In this case, $t$ and $t^{\prime}$ are either variables or constant symbols of the free sort, which means they do not contain subterms of the base sort. Since $\mathcal{B}$ and $\mathcal{A}$ behave identical on free-sort constant symbols and $\beta(u)=\widehat{\beta}_{C}(u)$ for every variable $u\in V_{\mathcal{S}}$, we have $\mathcal{B},\beta\not\models t\approx t^{\prime}$.

Case $\mathcal{A},\widehat{\beta}_{C}\models t\approx t^{\prime}$ for some $t\approx t^{\prime}\in\Delta$. Analogous to the above case, we get $\mathcal{B},\beta\models t\approx t^{\prime}$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$ for some non-equational atom

$P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})\in\Gamma$. This translates to

\bigl{\langle}\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{m^{\prime}}),\mathcal{A}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{A}}.

By definition of $\widehat{\beta}_{C}$, we have $\mathcal{A}(\widehat{\beta}_{C})(t_{j})\in Q$ for every $j$, $1\leq j\leq m$. Therefore, and by construction of $\mathcal{B}$,

\bigl{\langle}\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{m^{\prime}}),\mathcal{A}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

We observe the following properties:

• •

We have $\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{j})=\mathcal{B}(\beta)(t^{\prime}_{j})$ for every $j$, $1\leq j\leq m^{\prime}$, due to the definition of $\mathcal{B}$ and $\widehat{\beta}_{C}$.

• •

Since $\mathcal{A}$ and $\mathcal{B}$ interpret constant symbols in the same way, we get $\mathcal{A}(\widehat{\beta}_{C})(t_{j})=\mathcal{B}(\widehat{\beta}_{C})(t_{j})$ for every $j$, $1\leq j\leq m$.

• •

The definition of $\widehat{\beta}_{C}$ entails that \bigl{\langle}\mathcal{B}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{B}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle} and

\bigl{\langle}\mathcal{B}(\beta)(t_{1}),\ldots,\mathcal{B}(\beta)(t_{m})\bigr{\rangle} are ${\mathcal{J}_{\mathcal{B}}}$-equivalent.

The first two observations imply

\bigl{\langle}\mathcal{B}(\beta)(t^{\prime}_{1}),\ldots,\mathcal{B}(\beta)(t^{\prime}_{m^{\prime}}),\mathcal{B}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{B}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

Due to this result and the fact that $\mathcal{B}$ is ${\mathcal{J}_{\mathcal{B}}}$-uniform (Claim II), the third observation leads to \bigl{\langle}\mathcal{B}(\beta)(t^{\prime}_{1}),\ldots,\mathcal{B}(\beta)(t^{\prime}_{m^{\prime}}),\mathcal{B}(\beta)(t_{1}),\ldots,\mathcal{B}(\beta)(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

Put differently, we have $\mathcal{B},\beta\not\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$.

Case $\mathcal{A},\widehat{\beta}_{C}\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$ for some non-equational atom $P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})\in\Delta$. Analogous to the previous case we can infer $\mathcal{B},\beta\models P(t^{\prime}_{1},\ldots,$ $t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$.

Altogether, we have shown $\mathcal{B}\models N$. ∎

Proof of Lemma 11

As an auxiliary result, we first show a correspondence between the equivalence classes with respect to $\sim_{\mathcal{J}_{\mathcal{A}}}$ and mappings $\varrho:[m]\to[|{\mathcal{J}_{\mathcal{A}}}|]\times[m]$.

Lemma 26**.**

Let $\mathcal{A}$ be an interpretation. Let $\{q_{1}\},\ldots,\{q_{\kappa}\}$ be an enumeration of all point intervals in ${\mathcal{J}_{\mathcal{A}}}$ such that $q_{1}<\ldots<q_{\kappa}$ and let $J_{1},\ldots,J_{\kappa+1}$ be an enumeration of all open intervals in ${\mathcal{J}_{\mathcal{A}}}$ such that $J_{1}<\ldots<J_{\kappa+1}$. Let $S\in\mathbb{R}^{m}/_{\sim_{\mathcal{J}_{\mathcal{A}}}}$ be any equivalence class with respect to $\sim_{\mathcal{J}_{\mathcal{A}}}$. There is a mapping $\varrho:[m]\to[|{\mathcal{J}_{\mathcal{A}}}|]\times[m]$ such that

1. (i)

whenever $\varrho(i)=\langle k,\ell\rangle$ with $k>\kappa+1$ then $\ell=1$, and 2. (ii)

for all ascending tuples

[TABLE]

we have $\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle\in S$, and 3. (iii)

for every tuple $\langle s_{1},\ldots,s_{m}\rangle\in S$ there exist ascending tuples $\bar{r}_{1},\ldots,\bar{r}_{2K+1}$ defined as in (ii) such that $\langle s_{1},\ldots,s_{m}\rangle=\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle$.

Proof.

Let $\bar{s}^{\prime}$ be some representative taken from $S$, i.e. $S=[\bar{s}^{\prime}]_{\sim_{\mathcal{J}_{\mathcal{A}}}}$. Given $\bar{s}^{\prime}$, we construct $2K+1$ possibly empty sequences $\bar{s}^{\prime\prime}_{k}:=\langle s^{\prime\prime}_{k,1},s^{\prime\prime}_{k,2},\ldots\rangle$, such that every $\bar{s}^{\prime\prime}_{k}$ with $k\leq\kappa+1$ lists all elements of $\bar{s}^{\prime}$ in ascending order that lie in $J_{k}$, and every $\bar{s}^{\prime\prime}_{k}$ with $k>\kappa+1$ contains exactly the value $q_{k-\kappa-1}$. We construct the mapping $\varrho$ in such a way that $\varrho(i)=\langle k,\ell\rangle$ holds if and only if $s^{\prime}_{i}=s^{\prime\prime}_{k,\ell}$.

Let $\bar{r}_{1},\ldots,\bar{r}_{2K+1}$ be tuples of reals chosen in accordance with requirement (ii). It is easy to verify that $\bar{r}_{\varrho}:=\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle$ is ${\mathcal{J}_{\mathcal{A}}}$-equivalent to $\bar{s}^{\prime}$, i.e. $\bar{r}_{\varrho}$ belongs to $S$.

In order to show (iii), we construct the tuples $\bar{r}_{1},\ldots,\bar{r}_{2K+1}$ from $\langle s_{1},\ldots,s_{m}\rangle$ in the same way we have constructed the $\bar{s}^{\prime\prime}_{k}$ from $\bar{s}^{\prime}$ when constructing $\varrho$ in the beginning of this proof. In addition, we pad them with suitable values from the respective intervals $J_{k}$ to reach the length $m$ for every tuple. ∎

We can now prove Lemma 11.

Lemma**.**

Let $\mathcal{A}$ be an interpretation. Let $\{q_{1}\},\ldots,\{q_{\kappa}\}$ be an enumeration of all point intervals in ${\mathcal{J}_{\mathcal{A}}}$ such that $q_{1}<\ldots<q_{\kappa}$ and let $J_{1},\ldots,J_{\kappa+1}$ be an enumeration of all open intervals in ${\mathcal{J}_{\mathcal{A}}}$ such that $J_{1}<\ldots<J_{\kappa+1}$. Let $\lambda$ be a positive integer. There is a collection of finite sets $Q_{1},\ldots,Q_{\kappa+1}$ such that the following requirements are met.

1. (i)

For every $i$, $1\leq i\leq\kappa+1$, it holds $Q_{i}\subseteq J_{i}$ and $|Q_{i}|=\lambda$. 2. (ii)

Let $Q:=\bigcup_{i}Q_{i}\cup\{q_{1},\ldots,q_{\kappa}\}$. For all ${\mathcal{J}_{\mathcal{A}}}$-equivalent $m$-tuples $\bar{s},\bar{s}^{\prime}\in Q^{m}$ we have $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\bar{s}^{\prime})$.

Proof.

Let the sets $Q_{1},\ldots,Q_{\kappa+1}$ be the $Q_{1},\ldots,Q_{p}$ that we obtain by virtue of Lemma 5 when we set $n:=\lambda$, $p:=\kappa+1$, $\chi:=\chi_{\mathcal{A}}$, $R_{1}:=J_{1},\ldots,R_{\kappa+1}:=J_{\kappa+1}$.

Requirement (i) is obviously satisfied for $Q_{1},\ldots,Q_{\kappa+1}$.

By Lemma 26, the equivalence class to which any two given ${\mathcal{J}_{\mathcal{A}}}$-equivalent tuples $\bar{s},\bar{s}^{\prime}$ belong corresponds to some mapping $\varrho:[m]\to[2K+1]\times[m]$. Part (ii) of Lemma 26 states that $\bar{s}$ can be written in the form $\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle$ for appropriate values $r_{\langle k,\ell\rangle}$ and $\bar{s}^{\prime}$ can be represented in the form $\langle r^{\prime}_{\varrho(1)},\ldots,r^{\prime}_{\varrho(m)}\rangle$ for appropriate $r^{\prime}_{\langle k,\ell\rangle}$. We then know by Lemma 5 that $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\langle r_{\varrho(1)},\ldots,r_{\varrho(m)}\rangle)=\chi_{\mathcal{A}}(\langle r^{\prime}_{\varrho(1)},\ldots,r^{\prime}_{\varrho(m)}\rangle)=\chi_{\mathcal{A}}(\bar{s}^{\prime})$. ∎

A.3 Details Concerning Section 5

Proof of Lemma 17

Lemma**.**

Let \lambda:=\max\bigl{(}\{m\}\cup\bigl{\{}|\text{{vars}}(C)\cap V_{\mathcal{R}}|\bigm{|}C\in N\bigr{\}}\bigr{)}. Let $\mathcal{A}$ be a model of $N$ and let \kappa:=\max\bigl{(}\{1\}\cup\{|c|\bigm{|}c\in\text{{bconsts}}(N)\}\bigr{)}. Suppose we are given a finite set $Q\subset[0,1)$ of cardinality $\lambda+1$ such that $0\in Q$ and for all tuples $\bar{r},\bar{s}\in\widehat{Q}^{m}$, $\bar{r}\simeq_{\kappa}\bar{s}$ entails $\chi_{\mathcal{A}}(\bar{r})=\chi_{\mathcal{A}}(\bar{s})$, where

\widehat{Q}:=\bigl{\{}q+k\bigm{|}q\in Q\text{ and }k\in\{-\kappa-1,\ldots,0,\ldots,\kappa\}\bigr{\}}.

Then we can construct a model $\mathcal{B}$ of $N$ that is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform and that interprets the free sort $\mathcal{S}$ as a finite set.

Proof.

The construction of $\mathcal{B}$ from $\mathcal{A}$ is similar to the construction of uniform models outlined in the proof of Lemma 10.

Claim I: Let $\mu$ be a positive integer with $1\leq\mu\leq\lambda$. For each of the finitely many equivalence classes $S\in\mathbb{R}^{\mu}/_{\mathrel{\widehat{\simeq}}_{\kappa}}$ and every $\bar{r}\in S$, there is some $\bar{q}\in S\cap\widehat{Q}^{\mu}$ such that $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}$ and for all $i_{1},i_{2},i_{3}$ with $r_{i_{1}}<-\kappa$ and $r_{i_{2}}>\kappa$ and $-\kappa\leq r_{i_{3}}\leq\kappa$ we have $\text{fr}(q_{i_{1}})<\text{fr}(q_{i_{2}})<\text{fr}(q_{i_{3}})$.

Proof: Let $i_{1},i_{2},\ldots$ be all the indices from $\{1,\ldots,\mu\}$ for which we have $r_{i_{j}}>\kappa$ for every $j$. Analogously, let $\ell_{1},\ell_{2},\ldots$ be all the indices from $\{1,\ldots,\mu\}$ such that $r_{\ell_{j}}<-\kappa$ holds for every $j$. We define the real

\delta:=\min\bigl{\{}\text{fr}(r_{i})\bigm{|}\text{-\kappa\leq r_{i}\leq\kappa$and$\text{fr}(r_{i})>0$and$1\leq i\leq m}\bigr{\}}\cup\bigl{\{}\frac{1}{2}\bigr{\}}.

There must be some integer $t$ for which we get $0<\frac{1}{t}r_{i_{j}}<\frac{1}{2}\delta$ and $-\frac{1}{2}\delta<\frac{1}{t}r_{\ell_{j}}<0$ for every $j$. Let $\bar{r}^{\prime}$ be the tuple that we obtain from $\bar{r}$ by replacing every $r_{i_{j}}$ with $\frac{1}{t}r_{i_{j}}+\frac{1}{2}\delta+\kappa$ and every $r_{\ell_{j}}$ with $\frac{1}{t}r_{\ell_{j}}+\frac{1}{2}\delta-\kappa$. By construction, we observe $\bar{r}^{\prime}\in(-\kappa-1,\kappa+1)^{\mu}$ and $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{r}^{\prime}$. Moreover, we have $\frac{1}{2}\delta<\text{fr}(\bar{r}^{\prime}_{i_{j}})<\delta$ and $0<\text{fr}(\bar{r}^{\prime}_{\ell_{j}})<\frac{1}{2}\delta$ for every $j$.

Next, we define the following ascending sequences

• •

$s^{\prime}_{0}<s^{\prime}_{1}<\ldots<s^{\prime}_{k}$, where $s^{\prime}_{0}=0$ and the values $s^{\prime}_{j}$, $j\geq 1$, are the strictly positive fractional parts in ascending order that occur in $\text{fr}(\bar{r}^{\prime})$, and

• •

$q^{\prime}_{0}<q^{\prime}_{1}<\ldots<q^{\prime}_{\lambda}$, which comprises all reals in $Q$ in ascending order, including $q^{\prime}_{0}=0$.

We can now construct a tuple $\bar{q}\in S\cap\widehat{Q}^{\mu}$ by setting $q_{\ell}:=\lfloor r^{\prime}_{\ell}\rfloor+q^{\prime}_{j}$ for $j$ such that $\text{fr}(r^{\prime}_{\ell})=s^{\prime}_{j}$.

Clearly, $\bar{r}^{\prime}$ and $\bar{q}$ are $\simeq_{\kappa}$-equivalent. Since $\simeq_{\kappa}$ is a refinement of $\mathrel{\widehat{\simeq}}_{\kappa}$ on the subspace $(-\kappa-1,\kappa+1)^{\mu}$, this entails $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}$. $\Diamond$

Let $\widehat{\mathcal{S}}$ denote the set \{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}}$for some$c\in\text{{fconsts}}(N)}\}. The interpretation $\mathcal{B}$ can be constructed as follows:

• •

$\mathcal{S}^{\mathcal{B}}:=\widehat{\mathcal{S}}$,

• •

for every constant symbol $c$ occurring in $N$ we set $c^{\mathcal{B}}:=c^{\mathcal{A}}$,

• •

for every uninterpreted predicate symbol $P$ occurring in $N$ and for all tuples $\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$ and $\bar{r}\in\mathbb{R}^{m}$ we pick some tuple $\bar{q}\in\widehat{Q}^{m}$ in accordance with Claim I—i.e. $\bar{q}$ satisfies $\bar{r}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}$—and define $P^{\mathcal{B}}$ in such a way that

[TABLE]

Claim II: The interpretation $\mathcal{B}$ is $\mathrel{\widehat{\simeq}}_{\kappa}$-uniform.

Proof: Let $\bar{r}^{1},\bar{r}^{2}\in\mathbb{R}^{m}$ be two $\mathrel{\widehat{\simeq}}_{\kappa}$-equivalent tuples. By Claim I, there exist two tuples $\bar{q}^{1},\bar{q}^{2}$ such that $\bar{q}^{1}\mathrel{\widehat{\simeq}}_{\kappa}\bar{r}^{1}$ and $\bar{q}^{2}\mathrel{\widehat{\simeq}}_{\kappa}\bar{r}^{2}$. Clearly, by transitivity and symmetry of $\mathrel{\widehat{\simeq}}_{\kappa}$, we have $\bar{q}^{1}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}^{2}$. Even stronger, we can show $\bar{q}^{1}\simeq_{\kappa}\bar{q}^{2}$. Suppose, $\bar{q}^{1}\not\simeq_{\kappa}\bar{q}^{2}$. We observe the following properties, which follow from $\bar{q}^{1}\mathrel{\widehat{\simeq}}_{\kappa}\bar{q}^{2}$:

• •

$\lfloor\bar{q}^{1}\rfloor=\lfloor\bar{q}^{2}\rfloor$ and $\lceil\bar{q}^{1}\rceil=\lceil\bar{q}^{2}\rceil$.

• •

For all $i,j$, $1\leq i,j\leq m$, for which $-\kappa\leq q^{1}_{i},q^{1}_{j}\leq\kappa$, we have $\text{fr}(q^{1}_{i})\leq\text{fr}(q^{1}_{j})$ if and only if $\text{fr}(q^{2}_{i})\leq\text{fr}(q^{2}_{j})$.

• •

For all $i,j$, $1\leq i,j\leq m$, for which $\kappa<q^{1}_{i},q^{1}_{j}$ or $q^{1}_{i},q^{1}_{j}<-\kappa$, we have $q^{1}_{i}\leq q^{1}_{j}$ if and only if $q^{2}_{i}\leq q^{2}_{j}$. Because of $\bar{q}^{1},\bar{q}^{2}\in(-\kappa-1,\kappa+1)^{m}$, we even obtain $\text{fr}(q^{1}_{i})\leq\text{fr}(q^{1}_{j})$ if and only if $\text{fr}(q^{2}_{i})\leq\text{fr}(q^{2}_{j})$.

Hence, our assumption $\bar{q}^{1}\not\simeq_{\kappa}\bar{q}^{2}$ entails that there are two indices $i,j$ such that $\text{fr}(q^{1}_{i})\leq\text{fr}(q^{1}_{j})$ and $\text{fr}(q^{2}_{i})>\text{fr}(q^{2}_{j})$, and one of the following cases applies:

1. (1)

$q^{1}_{i},q^{2}_{i}>\kappa$ and $-\kappa\leq q^{1}_{j},q^{2}_{j}\leq\kappa$, or 2. (2)

$q^{1}_{i},q^{2}_{i}>\kappa$ and $q^{1}_{j},q^{2}_{j}<-\kappa$, or 3. (3)

$-\kappa\leq q^{1}_{i},q^{2}_{i}\leq\kappa$ and $q^{1}_{j},q^{2}_{j}>\kappa$, or 4. (4)

$-\kappa\leq q^{1}_{i},q^{2}_{i}\leq\kappa$ and $-\kappa<q^{1}_{j},q^{2}_{j}$, or 5. (5)

$q^{1}_{i},q^{2}_{i}<-\kappa$ and $-\kappa\leq q^{1}_{j},q^{2}_{j}$.

Ad (1). By Claim I, we have $\text{fr}(q^{1}_{i})<\text{fr}(q^{1}_{j})$ and $\text{fr}(q^{2}_{i})<\text{fr}(q^{2}_{j})$.

Ad (2). By Claim I, we have $\text{fr}(q^{1}_{j})<\text{fr}(q^{1}_{i})$ and $\text{fr}(q^{2}_{j})<\text{fr}(q^{2}_{i})$.

Ad (3). By Claim I, we have $\text{fr}(q^{1}_{i})<\text{fr}(q^{1}_{j})$ and $\text{fr}(q^{2}_{i})<\text{fr}(q^{2}_{j})$.

Ad (4). By Claim I, we have $\text{fr}(q^{1}_{j})<\text{fr}(q^{1}_{i})$ and $\text{fr}(q^{2}_{j})<\text{fr}(q^{2}_{i})$.

Ad (5). By Claim I, we have $\text{fr}(q^{1}_{i})<\text{fr}(q^{1}_{j})$ and $\text{fr}(q^{2}_{i})<\text{fr}(q^{2}_{j})$.

Since all cases lead to a contradiction, we must have $\bar{q}^{1}\simeq_{\kappa}\bar{q}^{2}$.

Because of $\bar{q}^{1},\bar{q}^{2}\in\widehat{Q}^{m}$ and due to our assumptions regarding $Q$ and $\widehat{Q}^{m}$, we have $\chi_{\mathcal{A}}(\bar{q}^{1})=\chi_{\mathcal{A}}(\bar{q}^{2})$. Moreover, by construction of $\mathcal{B}$, we have $\chi_{\mathcal{B}}(\bar{r}^{1})=\chi_{\mathcal{A}}(\bar{q}^{1})$ and $\chi_{\mathcal{B}}(\bar{r}^{2})=\chi_{\mathcal{A}}(\bar{q}^{2})$. Consequently, $\chi_{\mathcal{B}}(\bar{r}^{1})=\chi_{\mathcal{B}}(\bar{r}^{2})$. $\Diamond$

We next show $\mathcal{B}\models N$. Consider any clause $C=\Lambda\;\|\;\Gamma\to\Delta$ in $N$ and let $\beta$ be any variable assignment ranging over $\mathcal{S}^{\mathcal{B}}\cup\mathbb{R}$. Starting from $\beta$, we derive a special variable assignment $\widehat{\beta}_{C}$ as follows. Let $x_{1},\ldots,x_{\ell}$ be an enumeration of all base-sort variables in $C$. By Claim I, there exists some tuple $\bar{q}:=\langle q_{1},\ldots,q_{\ell}\rangle$ such that \langle q_{1},\ldots,q_{\ell}\rangle\mathrel{\widehat{\simeq}}_{\kappa}\bigl{\langle}\beta(x_{1}),\ldots,\beta(x_{\ell})\bigr{\rangle} and $\bar{q}\in\widehat{Q}^{\ell}$. We define $\widehat{\beta}_{C}(x_{i}):=q_{i}$ for every $i$, $1\leq i\leq\ell$. Hence, we have

[TABLE]

For all other base-sort variables $y\not\in\{x_{1},\ldots,x_{\ell}\}$, $\widehat{\beta}_{C}(y)$ can be defined arbitrarily. For every free-sort variable $u$ we set $\widehat{\beta}_{C}(u):=\beta(u)$.

As $\mathcal{A}$ is a model of $N$, we know $\mathcal{A},\widehat{\beta}_{C}\models C$. By case distinction on why $\mathcal{A},\widehat{\beta}_{C}\models C$ holds, we may use this result to obtain $\mathcal{B},\beta\models C$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models x\mathrel{\triangleleft}c$ for some constraint $x\mathrel{\triangleleft}c$ in $\Lambda$. Hence, $\beta_{C}(x)\not\mathrel{\triangleleft}c$. Due to $(*)$, the assumption $|c|\leq\kappa$, and the definition of $\mathrel{\widehat{\simeq}}_{\kappa}$, we know that $\widehat{\beta}_{C}(x)\mathrel{\triangleleft}c$ holds if and only if $\beta(x)\mathrel{\triangleleft}c$ holds. Consequently, we get $\beta(x)\not\mathrel{\triangleleft}c$ and thus $\mathcal{B},\beta\not\models x\mathrel{\triangleleft}c$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models x\mathrel{\triangleleft}y$ for some $x\mathrel{\triangleleft}y$ in $\Lambda$. By $(*)$ and the definition of $\mathrel{\widehat{\simeq}}_{\kappa}$, we know that $\widehat{\beta}_{C}(x)\mathrel{\triangleleft}\widehat{\beta}_{C}(y)$ if and only if $\beta(x)\mathrel{\triangleleft}\beta(y)$. Consequently, we get $\mathcal{B},\beta\not\models x\mathrel{\triangleleft}y$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models x-y\mathrel{\triangleleft}c$ for some constraint $x-y\mathrel{\triangleleft}c$ in $\Lambda$. By definition of BSR(BD) clause sets, $\Lambda$ must also contain constraints $c_{x}\leq x$, $x\leq d_{x}$, $c_{y}\leq y$, and $y\leq d_{y}$ for certain constants $c_{x},d_{x},c_{y},d_{y}$ whose absolute value is at most $\kappa$. If one of these constraints is violated by $\widehat{\beta}_{C}$, then the first case applies.

If all of these constraints are satisfied by $\widehat{\beta}_{C}$, then, by $(*)$, they are also satisfied by $\beta$. Moreover, $(*)$ and the definition of $\mathrel{\widehat{\simeq}}_{\kappa}$, entail $\lfloor\widehat{\beta}_{C}(x)\rfloor=\lfloor\beta(x)\rfloor$, $\lfloor\widehat{\beta}_{C}(y)\rfloor=\lfloor\beta(y)\rfloor$, $\lceil\widehat{\beta}_{C}(x)\rceil=\lceil\beta(x)\rceil$, $\lceil\widehat{\beta}_{C}(y)\rceil=\lceil\beta(y)\rceil$, $\text{fr}(\widehat{\beta}_{C}(x))\leq\text{fr}(\widehat{\beta}_{C}(y))$ if and only if $\text{fr}(\beta(x))\leq\text{fr}(\beta(y))$, and $\text{fr}(\widehat{\beta}_{C}(x))\geq\text{fr}(\widehat{\beta}_{C}(y))$ if and only if $\text{fr}(\beta(x))\geq\text{fr}(\beta(y))$. Hence, the following two observations hold:

[TABLE]

and

[TABLE]

Consequently, we have $\widehat{\beta}_{C}(x)-\widehat{\beta}_{C}(y)\mathrel{\triangleleft}c$ if and only if $\beta(x)-\beta(y)\mathrel{\triangleleft}c$. In other words, $\mathcal{A},\beta\not\models x-y\mathrel{\triangleleft}c$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models t\approx t^{\prime}$ for some free atom $t\approx t^{\prime}\in\Gamma$. Hence, $t$ and $t^{\prime}$ are either variables or constant symbols of the free sort, which means they do not contain subterms of the base sort. Since $\mathcal{B}$ and $\mathcal{A}$ behave identical on free-sort constant symbols and $\beta(u)=\widehat{\beta}_{C}(u)$ for every variable $u\in V_{\mathcal{S}}$, we get $\mathcal{B},\beta\not\models t\approx t^{\prime}$.

Case $\mathcal{A},\widehat{\beta}_{C}\models t\approx t^{\prime}$ for some $t\approx t^{\prime}\in\Delta$. Analogous to the above case, $\mathcal{B},\beta\models t\approx t^{\prime}$.

Case $\mathcal{A},\widehat{\beta}_{C}\not\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$ for some non-equational atom

$P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})\in\Gamma$. This translates to

\bigl{\langle}\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{m^{\prime}}),\mathcal{A}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{A}}.

By construction of $\widehat{\beta}_{C}$, we have $\mathcal{A}(\widehat{\beta}_{C})(t_{j})\in\widehat{Q}$ for every $j$, $1\leq j\leq m$. Due to our assumptions regarding $\widehat{Q}$ and by construction of $\mathcal{B}$, we therefore have

\bigl{\langle}\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{m^{\prime}}),\mathcal{A}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{A}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

We observe the following properties:

• •

We have $\mathcal{A}(\widehat{\beta}_{C})(t^{\prime}_{j})=\mathcal{B}(\beta)(t^{\prime}_{j})$ for every $j$, $1\leq j\leq m^{\prime}$, due to the definition of $\mathcal{B}$ and $\widehat{\beta}_{C}$.

• •

Since all the $t_{j}$ are base-sort variables, we get $\mathcal{A}(\widehat{\beta}_{C})(t_{j})=\mathcal{B}(\widehat{\beta}_{C})(t_{j})$ for every $j$, $1\leq j\leq m$.

These two observations yield

\bigl{\langle}\mathcal{B}(\beta)(t^{\prime}_{1}),\ldots,\mathcal{B}(\beta)(t^{\prime}_{m^{\prime}}),\mathcal{B}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{B}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

Because of this result, and due to $\mathrel{\widehat{\simeq}}_{\kappa}$-uniformity of $\mathcal{B}$,

\bigl{\langle}\mathcal{B}(\widehat{\beta}_{C})(t_{1}),\ldots,\mathcal{B}(\widehat{\beta}_{C})(t_{m})\bigr{\rangle}\mathrel{\widehat{\simeq}}_{\kappa}\bigl{\langle}\mathcal{B}(\beta)(t_{1}),\ldots,\mathcal{B}(\beta)(t_{m})\bigr{\rangle}

leads to

\bigl{\langle}\mathcal{B}(\beta)(t^{\prime}_{1}),\ldots,\mathcal{B}(\beta)(t^{\prime}_{m^{\prime}}),\mathcal{B}(\beta)(t_{1}),\ldots,\mathcal{B}(\beta)(t_{m})\bigr{\rangle}\not\in P^{\mathcal{B}}.

Put differently, we have $\mathcal{B},\beta\not\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$.

Case $\mathcal{A},\widehat{\beta}_{C}\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$ for some non-equational atom

$P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})\in\Delta$. Analogously to the previous case we can infer $\mathcal{B},\beta\models P(t^{\prime}_{1},\ldots,t^{\prime}_{m^{\prime}},t_{1},\ldots,t_{m})$.

Altogether, we have shown $\mathcal{B}\models N$. ∎

Proof of Lemma 18

We first need the following auxiliary result.

Lemma 27**.**

Let $S\in(-\kappa-1,\kappa+1)^{m}/_{\simeq_{\kappa}}$ be an equivalence class with respect to $\simeq_{\kappa}$. There are two mappings $\varrho:[m]\to\{0,1,\ldots,m\}$ and $\sigma:[m]\to\{-\kappa-1,\ldots,0,\ldots,\kappa\}$ such that

1. (i)

for any ascending tuple $\langle r_{0},r_{1},\ldots,r_{m}\rangle\in[0,1)^{m+1}$ with $r_{0}=0$ we have \bigl{\langle}r_{\varrho(1)}+\sigma(1),\ldots,r_{\varrho(m)}+\sigma(m)\bigr{\rangle}\in S, and 2. (ii)

for every tuple $\langle s_{1},\ldots,s_{m}\rangle\in S$ there is an ascending tuple $\langle r_{0},r_{1},\ldots,r_{m}\rangle\in[0,1)^{m+1}$ with $r_{0}=0$ such that \bigl{\langle}s_{1},\ldots,s_{m}\bigr{\rangle}=\bigl{\langle}r_{\varrho(1)}+\sigma(1),\ldots,r_{\varrho(m)}+\sigma(m)\bigr{\rangle}.

Proof.

Fix some tuple $\bar{q}$ taken from $S$. Given $\bar{q}$, we set $q^{\prime}_{0}:=0$ and further construct the sequence $q^{\prime}_{1},q^{\prime}_{2},\ldots$ in such a way that it lists all strictly positive fractional values in $\text{fr}(\bar{q})$ in ascending order.

We construct $\sigma$ by setting $\sigma(i):=\lfloor q_{i}\rfloor$ for every $i=1,\ldots,m$, and $\varrho$ such that $\varrho(i)=k$ holds if and only if $\text{fr}(q_{i})=q^{\prime}_{k}$. Consequently, we have

• ($*$)

\langle q_{1},\ldots,q_{m}\rangle=\bigl{\langle}\text{fr}(q_{1})+\lfloor q_{1}\rfloor,\ldots,\text{fr}(q_{m})+\lfloor q_{m}\rfloor\bigr{\rangle}=\bigl{\langle}q^{\prime}_{\varrho(1)}+\sigma(1),\ldots,q^{\prime}_{\varrho(m)}+\sigma(m)\bigr{\rangle}.

Let $\langle r_{0},r_{1},\ldots,r_{m}\rangle\in[0,1)^{m+1}$ be any ascending tuple with $r_{0}=0$. For all $i,j$, we observe the following properties:

1. (1)

$\lfloor r_{\varrho(i)}+\sigma(i)\rfloor=\sigma(i)=\lfloor q_{i}\rfloor$. 2. (2)

$\text{fr}(r_{\varrho(i)}+\sigma(i))=\text{fr}(r_{\varrho(i)})=r_{\varrho(i)}$. 3. (3)

$\varrho(i)=0$ if and only if $\text{fr}(q_{i})=q^{\prime}_{0}=0$, which entails that $\text{fr}(r_{\varrho(i)}+\sigma(i))=0$ holds if and only if we have $\text{fr}(q_{i})=0$. 4. (4)

$\text{fr}(q_{i})=q^{\prime}_{\varrho(i)}$. 5. (5)

We have $\text{fr}(r_{\varrho(i)}+\sigma(i))\;\leq\;\text{fr}(r_{\varrho(j)}+\sigma(j))$

if and only if $r_{\varrho(i)}\;\leq\;r_{\varrho(j)}$

if and only if $\varrho(i)\;\leq\;\varrho(j)$

if and only if $q^{\prime}_{\varrho(i)}\;\leq\;q^{\prime}_{\varrho(j)}$

if and only if $\text{fr}(q_{i})\;\leq\;\text{fr}(q_{j})$.

Taken together, these observations imply $\bar{q}\simeq_{\kappa}\langle r_{\varrho(1)}+\sigma(1),\ldots,r_{\varrho(m)}+\sigma(m)\rangle$. Hence, we have just proved (i).

In fact, we have also already proved (ii), by giving the construction of the sequence $q^{\prime}_{0},q^{\prime}_{1},q^{\prime}_{2},\ldots$ and by having derived ($*$). If the sequence $q^{\prime}_{1},q^{\prime}_{2},\ldots$ is shorter than $m$ elements, we can simply pad it in an ascending fashion with arbitrary values from $(0,1)$. ∎

We can now prove Lemma 18.

Lemma**.**

Let $\mathcal{A}$ be an interpretation and let $\kappa,\lambda$ be positive integers. There exists a finite set $Q\subset[0,1)$ of cardinality $\lambda+1$ such that $0\in Q$ and for all tuples $\bar{s},\bar{s}^{\prime}\in\widehat{Q}^{m}$, $\bar{s}\simeq_{\kappa}\bar{s}^{\prime}$ entails $\chi_{\mathcal{A}}(\bar{s})=\chi_{\mathcal{A}}(\bar{s}^{\prime})$, where

\widehat{Q}:=\bigl{\{}q+k\bigm{|}q\in Q\text{ and }k\in\{-\kappa-1,\ldots,0,\ldots,\kappa\}\bigr{\}}.

Proof.

Let $S_{1},\ldots,S_{k}$ be some enumeration of all equivalence classes in $(-\kappa-1,\kappa+1)^{m}/_{\simeq_{\kappa}}$. By Lemma 27, there is a (not necessarily unique) sequence $\langle\varrho_{1},\sigma_{1}\rangle,\ldots,\langle\varrho_{k},\sigma_{k}\rangle$ of pairs of functions such that each pair $\langle\varrho_{j},\sigma_{j}\rangle$ corresponds to the equivalence class $S_{j}$ in the sense of Lemma 27.

Let \widehat{\mathcal{S}}:=\{{a}\in\mathcal{S}^{\mathcal{A}}\mid\text{{a}=c^{\mathcal{A}}$for some$c\in\text{{fconsts}}(N)}\} be the set of all domain elements assigned to free-sort constant symbols by $\mathcal{A}$. We define a coloring \widehat{\chi}:\mathbb{R}^{m}\to\bigl{(}\mathcal{P}\{P_{i}\bar{a}\mid\text{\bar{a}\in\widehat{\mathcal{S}}^{m^{\prime}}$and$P_{i} occurs} \text{in N}\}\bigr{)}^{k} by setting

[TABLE]

for every tuple $\bar{r}=\langle r_{1},\ldots,r_{m}\rangle\in(0,1)^{m}$, where we define $r_{0}$ to be [math]. By virtue of Lemma 4, there is a set $Q^{\prime}\subseteq(0,1)$ of cardinality $\lambda$ such that all ascending tuples $\langle r_{1},\ldots,r_{m}\rangle\in{Q^{\prime}}^{m}$ are assigned the same color by $\chi$. We then set $Q:=Q^{\prime}\cup\{0\}$.

Consider any equivalence class $S_{j}$ and the corresponding pair $\langle\varrho_{j},\sigma_{j}\rangle$ and let $\bar{s},\bar{s}^{\prime}\in\widehat{Q}^{m}$ be two $\simeq_{\kappa}$-equivalent tuples. Let $q_{1},q_{2},\ldots$ be an enumeration of all the strictly positive fractional parts in $\text{fr}(\bar{s})$ in ascending order and let $q_{0}:=0$. Hence, $q_{0}<q_{1}<q_{2}<\ldots$.

By Lemma 27, there are two ascending tuples $\bar{q}:=\langle 0,q_{1},\ldots,q_{m}\rangle$ and $\bar{q}^{\prime}:=\langle 0,q^{\prime}_{1},\ldots,q^{\prime}_{m}\rangle$ in $[0,1)^{m+1}$ such that

$\bar{s}=\langle q_{\varrho_{j}(1)}+\sigma(1),\ldots,q_{\varrho_{j}(m)}+\sigma(m)\rangle$

and

$\bar{s}^{\prime}=\langle q^{\prime}_{\varrho_{j}(1)}+\sigma(1),\ldots,q^{\prime}_{\varrho_{j}(m)}+\sigma(m)\rangle$.

Because of $\bar{s},\bar{s}^{\prime}\in\widehat{Q}^{m}$, we know that $\langle q_{1},\ldots,q_{m}\rangle\in{Q^{\prime}}^{m}$ and $\langle q^{\prime}_{1},\ldots,q^{\prime}_{m}\rangle\in{Q^{\prime}}^{m}$. Then, $\widehat{\chi}(\langle q_{1},\ldots,q_{m}\rangle)=\widehat{\chi}(\langle q^{\prime}_{1},\ldots,q^{\prime}_{m}\rangle)$ entails

[TABLE]

A.4 Details Concerning Section 6

Proof of Lemma 22

We first need an auxiliary result.

Lemma 28**.**

Let $S\in[0,\lambda+1)^{|\bar{x}|}/_{\simeq_{\lambda}}$ be some equivalence class with respect to $\simeq_{\lambda}$. We define the two sets $\widehat{S}_{1},\widehat{S}_{2}$ as follows:

[TABLE]

and

[TABLE]

where $q_{0},q^{\prime}_{0}$ are some fixed reals in the tuples $\bar{q},\bar{q}^{\prime}$, respectively, that correspond to the same index. We observe $\widehat{S}_{1}=\widehat{S}_{2}$.

Proof.

We obviously have $\widehat{S}_{1}\subseteq\widehat{S}_{2}$.

In order to prove $\widehat{S}_{2}\subseteq\widehat{S}_{1}$, consider any $\bar{q}^{\prime}\in\widehat{S}_{2}$. Pick some $\bar{s}\in S$ for which $s_{i}\leq q^{\prime}_{i}$ for every $i$, $1\leq i\leq|\bar{x}|$. By construction of $\widehat{S}_{2}$, we observe $\lfloor s_{0}-s_{i}\rfloor=\lfloor q^{\prime}_{0}-q^{\prime}_{i}\rfloor$ and $\lceil s_{0}-s_{i}\rceil=\lceil q^{\prime}_{0}-q^{\prime}_{i}\rceil$ for every $i$, $1\leq i\leq|\bar{x}|$.

Claim III: For all indices $j_{1},j_{2}\in\{1,\ldots,|\bar{x}|\}$ we have $\text{fr}(s_{j_{1}})=\text{fr}(s_{j_{2}})$ if and only if $\text{fr}(q^{\prime}_{j_{1}})=\text{fr}(q^{\prime}_{j_{2}})$.

Proof: For all reals $r,t$ we have $\text{fr}(r)=\text{fr}(t)$ if and only if $\lfloor r-t\rfloor=\lceil r-t\rceil$. Using this fact, we get that $\text{fr}(s_{j_{1}})=\text{fr}(s_{j_{2}})$ entails $\lfloor q^{\prime}_{j_{1}}-q^{\prime}_{j_{2}}\rfloor=\lfloor s_{j_{1}}-s_{j_{2}}\rfloor=\lceil s_{j_{1}}-s_{j_{2}}\rceil=\lceil q^{\prime}_{j_{1}}-q^{\prime}_{j_{2}}\rceil$ which in turn implies $\text{fr}(q^{\prime}_{j_{1}})=\text{fr}(q^{\prime}_{j_{2}})$. Symmetrically, $\text{fr}(q^{\prime}_{j_{1}})=\text{fr}(q^{\prime}_{j_{2}})$ entails $\text{fr}(s_{j_{1}})=\text{fr}(s_{j_{2}})$. $\Diamond$

Claim IV: Let $k_{1},\ldots,k_{|\bar{x}|}$be some enumeration of the indices in $\{1,\ldots,|\bar{x}|\}$ such that $\text{fr}(s_{k_{1}})\leq\ldots\leq\text{fr}(s_{k_{|\bar{x}|}})$. There is some $\ell$ such that

$\text{fr}(q^{\prime}_{k_{\ell+1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{|\bar{x}|}})\leq\text{fr}(q^{\prime}_{k_{1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{\ell}})$.

Proof: Suppose Claim IV does not hold, while Claim III is respected. Hence, suppose there are indices $j_{1},j_{2},j_{3}\in\{1,\ldots,|\bar{x}|\}$ such that $\text{fr}(s_{j_{1}})<\text{fr}(s_{j_{2}})<\text{fr}(s_{j_{3}})$ and $\text{fr}(q^{\prime}_{j_{3}})<\text{fr}(q^{\prime}_{j_{2}})<\text{fr}(q^{\prime}_{j_{1}})$.111There are analogous arguments leading to contradictions in the cases where $\text{fr}(q^{\prime}_{j_{2}})<\text{fr}(q^{\prime}_{j_{1}})<\text{fr}(q^{\prime}_{j_{3}})$ and $\text{fr}(q^{\prime}_{j_{1}})<\text{fr}(q^{\prime}_{j_{3}})<\text{fr}(q^{\prime}_{j_{2}})$.

For all reals $r,t$ we have $\lfloor r-t\rfloor=\lfloor r\rfloor-\lfloor t\rfloor+\lfloor\text{fr}(r)-\text{fr}(t)\rfloor$, where

\lfloor\text{fr}(r)-\text{fr}(t)\rfloor=\begin{cases}0&\text{if \text{fr}(r)\geq\text{fr}(t)}\\ -1&\text{if \text{fr}(r)<\text{fr}(t).}\end{cases}

Hence, we get the following system of equations:

\begin{array}[]{r@{;;=;;}l@{\qquad=\qquad}r@{;;=;;}l}\lfloor s_{j_{1}}\rfloor-\lfloor s_{j_{2}}\rfloor-1&\lfloor s_{j_{1}}-s_{j_{2}}\rfloor&\lfloor q^{\prime}_{j_{1}}-q^{\prime}_{j_{2}}\rfloor&\lfloor q^{\prime}_{j_{1}}\rfloor-\lfloor q^{\prime}_{j_{2}}\rfloor\\ \lfloor s_{j_{1}}\rfloor-\lfloor s_{j_{3}}\rfloor-1&\lfloor s_{j_{1}}-s_{j_{3}}\rfloor&\lfloor q^{\prime}_{j_{1}}-q^{\prime}_{j_{3}}\rfloor&\lfloor q^{\prime}_{j_{1}}\rfloor-\lfloor q^{\prime}_{j_{3}}\rfloor\\ \lfloor s_{j_{2}}\rfloor-\lfloor s_{j_{3}}\rfloor-1&\lfloor s_{j_{2}}-s_{j_{3}}\rfloor&\lfloor q^{\prime}_{j_{2}}-q^{\prime}_{j_{3}}\rfloor&\lfloor q^{\prime}_{j_{2}}\rfloor-\lfloor q^{\prime}_{j_{3}}\rfloor\end{array}

As this system entails $0=1$, we obtain a contradiction. $\Diamond$

It remains to prove the existence of some tuple $\bar{q}$ that satisfies the following requirements:

1. (i)

$\lfloor\bar{q}\rfloor=\lfloor\bar{s}\rfloor$ and $\lceil\bar{q}\rceil=\lceil\bar{s}\rceil$. 2. (ii)

$\lfloor s_{0}-s_{i}\rfloor=\lfloor q_{0}-q_{i}\rfloor$ and $\lceil s_{0}-s_{i}\rceil=\lceil q_{0}-q_{i}\rceil$ for every $i$. 3. (iii)

$q_{0}-q_{i}=q^{\prime}_{0}-q^{\prime}_{i}$ for every $i$. 4. (iv)

$q_{i}\leq q^{\prime}_{i}$ for every $i$.

Notice that Requirement (ii) is entailed by Requirement (iii) and the definition of $S_{2}$.

Consider any $i$ with $1\leq i\leq|\bar{x}|$. Requirement (i) entails that $\bar{q}$ must satisfy $q_{i}=\lfloor s_{i}\rfloor+\text{fr}(q_{i})$. It follows that $q_{0}-q_{i}=\lfloor s_{0}\rfloor+\text{fr}(q_{0})-\lfloor s_{i}\rfloor-\text{fr}(q_{i})$ and $q^{\prime}_{0}-q^{\prime}_{i}=\lfloor q^{\prime}_{0}\rfloor+\text{fr}(q^{\prime}_{0})-\lfloor q^{\prime}_{i}\rfloor-\text{fr}(q^{\prime}_{i})$. Hence, Requirement (iii) entails

$\lfloor s_{0}\rfloor-\lfloor s_{i}\rfloor+\text{fr}(q_{0})-\text{fr}(q_{i})\;\;=\;\;\ \lfloor q^{\prime}_{0}\rfloor-\lfloor q^{\prime}_{i}\rfloor+\text{fr}(q^{\prime}_{0})-\text{fr}(q^{\prime}_{i})$,

which is equivalent to

[TABLE]

We distinguish several cases:

If $\bar{q}^{\prime}\in S$, then we set $\bar{q}:=\bar{q}^{\prime}$.

If there is some $j$ such that $\lfloor s_{j}\rfloor=\lceil s_{j}\rceil$, then, by Requirement (i), we must satisfy $\text{fr}(q_{j})=0$ and, therefore, for every $i$, $\text{fr}(q_{i})$ is determined by $(*)$.

If $\text{fr}(s_{1})=\ldots=\text{fr}(s_{|\bar{x}|})$, then we observe $\lfloor q^{\prime}_{0}-q^{\prime}_{i}\rfloor=\lfloor s_{0}-s_{i}\rfloor=\lceil s_{0}-s_{i}\rceil=\lceil q^{\prime}_{0}-q^{\prime}_{i}\rceil$ for every $i$. Hence, we have $\lfloor q^{\prime}_{0}-q^{\prime}_{i}\rfloor=\lceil q^{\prime}_{0}-q^{\prime}_{i}\rceil$, which implies $\text{fr}(q^{\prime}_{0})=\text{fr}(q^{\prime}_{i})$ for every $i$. As this entails $q^{\prime}_{0}-q^{\prime}_{i}=\lfloor q^{\prime}_{0}-q^{\prime}_{i}\rfloor=\lfloor s_{0}-s_{i}\rfloor=s_{0}-s_{i}$, Requirement (iii) is satisfied if we set $\bar{q}:=\bar{s}$.

If none of the above cases apply, we have $\lfloor s_{i}\rfloor=\lceil s_{i}\rceil-1$ for every $i$. Moreover, we know that there are indices $i_{1},i_{2}$ such that $\text{fr}(s_{i_{1}})<\text{fr}(s_{i_{2}})$.

Let $k_{1},\ldots,k_{|\bar{x}|}$be some enumeration of the indices in $\{1,\ldots,|\bar{x}|\}$ such that $\text{fr}(s_{k_{1}})\leq\ldots\leq\text{fr}(s_{k_{|\bar{x}|}})$. Notice that $\text{fr}(s_{k_{1}})<\text{fr}(s_{k_{|\bar{x}|}})$ holds due to our assumptions. By Claim IV, there is some $\ell$ such that

$\text{fr}(q^{\prime}_{k_{\ell+1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{|\bar{x}|}})\leq\text{fr}(q^{\prime}_{k_{1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{\ell}})$.

In fact, Claim III together with $\text{fr}(s_{k_{1}})<\text{fr}(s_{k_{|\bar{x}|}})$ entails that $\text{fr}(q^{\prime}_{k_{|\bar{x}|}})$ is strictly smaller than $\text{fr}(q^{\prime}_{k_{1}})$.

We pick some real $\varepsilon$ such that $0<\varepsilon<\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{|\bar{x}|}})$. For every $j$, $1\leq j\leq\ell$, we set \text{fr}(q_{k_{j}}):=\varepsilon+\bigl{(}\text{fr}(q^{\prime}_{k_{j}})-\text{fr}(q^{\prime}_{k_{1}})\bigr{)}. For every $j$, $\ell+1\leq j\leq|\bar{x}|$, we set \text{fr}(q_{k_{j}}):=\varepsilon+1-\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{j}})\bigr{)}.

Claim V: $0<\text{fr}(q_{k_{1}})\leq\ldots\leq\text{fr}(q_{k_{\ell}})\leq\text{fr}(q_{k_{\ell+1}})\leq\ldots\leq\text{fr}(q_{k_{|\bar{x}|}})<1$.

Proof:

We observe

• •

\text{fr}(q_{k_{1}})=\varepsilon+\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{1}})\bigr{)}=\varepsilon>0.

• •

\text{fr}(q_{k_{|\bar{x}|}})=\varepsilon+1-\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{|\bar{x}|}})\bigr{)}<\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{|\bar{x}|}})\bigr{)}+1-\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{|\bar{x}|}})\bigr{)}=1.

• •

Because of $\text{fr}(q^{\prime}_{k_{\ell}})\in[0,1)$ and $\text{fr}(q^{\prime}_{k_{\ell+1}})\in[0,1)$, we obtain $\text{fr}(q^{\prime}_{k_{\ell}})\leq\text{fr}(q^{\prime}_{k_{\ell+1}})+1$. Hence, we get \text{fr}(q_{k_{\ell}})=\varepsilon+\bigl{(}\text{fr}(q^{\prime}_{k_{\ell}})-\text{fr}(q^{\prime}_{k_{1}})\bigr{)}\leq\varepsilon+\text{fr}(q^{\prime}_{k_{\ell+1}})+1-\text{fr}(q^{\prime}_{k_{1}})=\varepsilon+1-\bigl{(}\text{fr}(q^{\prime}_{k_{1}})-\text{fr}(q^{\prime}_{k_{\ell+1}})\bigr{)}=\text{fr}(q_{k_{\ell+1}}).

The above observations entail $0<\text{fr}(q_{k_{1}})$, $\text{fr}(q_{k_{\ell}})\leq\text{fr}(q_{k_{\ell+1}})$, and $\text{fr}(q_{k_{|\bar{x}|}})<1$. By definition of the $\text{fr}(q_{k_{j}})$ and our assumptions $\text{fr}(q^{\prime}_{k_{1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{\ell}})$ and $\text{fr}(q^{\prime}_{k_{\ell+1}})\leq\ldots\leq\text{fr}(q^{\prime}_{k_{|\bar{x}|}})$, these observations imply Claim V. $\Diamond$

Claim VI: For every $j$ we have \bigl{(}\lfloor s_{k_{1}}\rfloor+\text{fr}(q_{k_{1}})\bigr{)}-\bigl{(}\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\bigr{)}=q^{\prime}_{k_{1}}-q^{\prime}_{k_{j}}.

Proof: If $1\leq j\leq\ell$, then we have

[TABLE]

where $\delta=0$ in case of $\text{fr}(q^{\prime}_{k_{1}})=\text{fr}(q^{\prime}_{k_{j}})$ (or $\text{fr}(s_{k_{1}})=\text{fr}(s_{k_{j}})$) and $\delta=1$ if $\text{fr}(q^{\prime}_{k_{1}})<\text{fr}(q^{\prime}_{k_{j}})$ (or $\text{fr}(s_{k_{1}})<\text{fr}(s_{k_{j}})$).

If $\ell+1\leq j\leq|\bar{x}|$, then we have

[TABLE]

Since $\text{fr}(q^{\prime}_{k_{|\bar{x}|}})$ is strictly smaller than $\text{fr}(q^{\prime}_{k_{1}})$, we get $\text{fr}(q^{\prime}_{k_{j}})<\text{fr}(q_{k_{1}})$. Moreover, Claim III together with $\text{fr}(s_{k_{1}})\leq\text{fr}(s_{k_{j}})$ entails $\text{fr}(s_{k_{1}})<\text{fr}(s_{k_{j}})$. Hence, $\lfloor s_{k_{1}}\rfloor-\lfloor s_{k_{j}}\rfloor=\lfloor s_{k_{1}}-s_{k_{j}}\rfloor+1$ and $\lfloor q^{\prime}_{k_{1}}-q^{\prime}_{k_{j}}\rfloor=\lfloor q^{\prime}_{k_{1}}\rfloor-\lfloor q^{\prime}_{k_{j}}\rfloor$. Consequently, we get

[TABLE]

$\Diamond$

Claim VII: For every $j$ we have $\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\leq q^{\prime}_{k_{j}}$.

Proof: As we assume $\bar{q}^{\prime}\not\in S$, there is at least one $i$ such that $\lfloor q^{\prime}_{k_{i}}\rfloor>\lfloor s_{k_{i}}\rfloor$. This entails $q^{\prime}_{k_{i}}\geq\lfloor q^{\prime}_{k_{i}}\rfloor>\lfloor s_{k_{i}}\rfloor+\text{fr}(q_{k_{i}})$. As one consequence of Claim VI, we get that \bigl{(}\lfloor s_{k_{i}}\rfloor+\text{fr}(q_{k_{i}})\bigr{)}-\bigl{(}\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\bigr{)}=q^{\prime}_{k_{i}}-q^{\prime}_{k_{j}} for every $j$. This can be rewritten into the equivalent equation q^{\prime}_{k_{j}}-\bigl{(}\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\bigr{)}=q^{\prime}_{k_{i}}-\bigl{(}\lfloor s_{k_{i}}\rfloor+\text{fr}(q_{k_{i}})\bigr{)}. In other words, we have q^{\prime}_{k_{j}}>\bigl{(}\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})\bigr{)} for every $j$. $\Diamond$

This means, if we set $q_{k_{j}}:=\lfloor s_{k_{j}}\rfloor+\text{fr}(q_{k_{j}})$ for every $j$, $1\leq j\leq|\bar{x}|$, then the stipulated requirements are satisfied. ∎

Using the above result, we can prove Lemma 22

Lemma**.**

Consider any delay clause

[TABLE]

that belongs to the FOL(LA) encoding of some timed automaton $\mathbf{A}:=\langle\text{{Loc}},\ell_{0},\bar{x},$ $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$. Let $\lambda$ be some positive integer. Let $M$ be a finite clause set corresponding to the following formula

[TABLE]

For every $\simeq_{\lambda}$-uniform interpretation $\mathcal{A}$ we have $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models C$ for all tuples $\bar{r},\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ if and only if $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]\models M$ holds for all tuples $\bar{q},\bar{q}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$.

Proof.

We first show that the clause $C$ is equivalent to the clause

[TABLE]

where $x_{0}$ is some fixed clock variable $x_{0}\in\bar{x}$. Although the variable $z$ in $C$ is universally quantified, the fact that $z$ does not occur on the right-hand side of the implication entails that $z$’s quantifier can be moved inside the premise of the implication $C$ represents, where universal quantification will turn into existential quantification (the quantifier moves into the scope of one implicit negation symbols). This transformation yields an equivalent clause with the constraint $\exists z.\;\bigwedge_{x\in\bar{x}}x^{\prime}-x=z\;\wedge\;z\geq 0\;\wedge\;\text{{inv}}_{\ell}[\bar{x}^{\prime}]$. In addition, we observe

[TABLE]

Consequently, the clauses $C$ and $C^{\prime}$ are equivalent.

Let $S\subseteq[0,\lambda+1)^{|\bar{x}|}$ be any equivalence class with respect to $\simeq_{\lambda}$. Since we assume $\mathcal{A}$ to be $\simeq_{\lambda}$-uniform, we have that, if $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r}]\models\text{{Reach}}(\ell,\bar{x})$ holds for one $\bar{r}\in S$, then $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q}]\models\text{{Reach}}(\ell,\bar{x})$ holds for every $\bar{q}\in S$.

Now suppose $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models C^{\prime}$ holds for all tuples $\bar{r},\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$. Moreover, suppose there is some pair of tuples $\bar{q},\bar{q}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ such that $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]\not\models\varphi$. Thus, we have that $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]$ satisfies the premises of $\varphi$—among them $\text{{inv}}_{\ell}[\bar{x}^{\prime}]$— but does not satisfy the consequent $\text{{Reach}}(\ell,\bar{x}^{\prime})$. As \mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]\models\bigwedge_{x_{1},x_{2}\in\bar{x}}\bigwedge_{-\lambda\leq k\leq\lambda}\bigl{(}x_{1}-x_{2}\leq k\;\leftrightarrow\;x^{\prime}_{1}-x^{\prime}_{2}\leq k\bigr{)}\;\wedge\;\bigl{(}x_{1}-x_{2}\geq k\leftrightarrow x^{\prime}_{1}-x^{\prime}_{2}\geq k\bigr{)}\;\wedge\;\bigwedge_{x\in\bar{x}}x^{\prime}\geq x, we know that $\bar{q}^{\prime}\in\widehat{S}_{2}$, where $S\subseteq[0,\lambda+1)^{|\bar{x}|}$ is the equivalence class with respect to $\simeq_{\lambda}$ to which $\bar{q}$ belongs and $\widehat{S}_{2}$ is defined as in Lemma 28. Moreover, we know that $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{s}]\models\text{{Reach}}(\ell,\bar{x})$ for every $\bar{s}\in S$, as $\mathcal{A}$ is $\simeq_{\lambda}$-uniform. The fact that $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{r},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{r}^{\prime}]\models C^{\prime}$ holds for all tuples $\bar{r},\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ entails $\mathcal{A},[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{s}^{\prime}]\models\text{{Reach}}(\ell,\bar{x}^{\prime})$ for every $\bar{s}^{\prime}\in\widehat{S}_{1}$ for which $[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{s}^{\prime}]\models\text{{inv}}_{\ell}[\bar{x}^{\prime}]$, where $\widehat{S}_{1}$ is defined as in Lemma 28. Hence, Lemma 28 entails $\mathcal{A},[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{s}^{\prime\prime}]\models\text{{Reach}}(\ell,\bar{x}^{\prime})$ for every $\bar{s}^{\prime\prime}\in\widehat{S}_{2}$ for which $[\bar{x}^{\prime}{\mathop{\mapsto}}\bar{s}^{\prime\prime}]\models\text{{inv}}_{\ell}[\bar{x}^{\prime}]$, in particular for $\bar{s}^{\prime\prime}=\bar{q}^{\prime}$. This contradiction implies that $\mathcal{A},[\bar{x}{\mathop{\mapsto}}\bar{q},\bar{x}^{\prime}{\mathop{\mapsto}}\bar{q}^{\prime}]\models\varphi$ holds for all tuples $\bar{q},\bar{q}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$.

The opposite direction can be argued analogously. ∎

Details regarding Theorem 23

Figure 2 illustrates the TA regions for some timed automaton with two clocks and in which all integer constants have an absolute value of at most $2$. For every TA region $R\subseteq\mathbb{R}^{2}$ of such an automaton, there is at least one representative $\bar{r}\in R$ which lies in $[0,5)^{2}$.

Let $\mathbf{A}:=\langle\text{{Loc}},\ell_{0},\bar{x},$ $\langle\text{{inv}}_{\ell}\rangle_{\ell\in\text{{Loc}}},\mathcal{T}\rangle$ be a timed automaton and let $k$ be the maximal absolute value of any integer constant occurring in the invariants and the transition guards of $\mathbf{A}$. Let $x_{1},\ldots,x_{\ell}$ be some enumeration of all the clock variables in $\bar{x}$. Consider a constraint of the form

$\psi:=\;\;x_{1}-x_{2}=k\;\wedge\;x_{2}-x_{3}=k\;\wedge\ldots\wedge\;x_{\ell-1}-x_{\ell}=k$.

We observe that $\psi$ entails $x_{1}-x_{\ell}=(\ell-1)\cdot k$. Of course, $\psi$ can also be conjoined with the constraint $x_{1}<-k$, say, which entails $x_{\ell}<-k-(\ell-1)\cdot k$. This example illustrates that one can combine several difference constraints $x-y\mathrel{\triangleleft}c$ over different clock variables in such a way that bounds are achieved which cannot be formulated with a single constraint $u-v\mathrel{\triangleleft}d$ with $|d|\leq k$. However, all of those combined constraints can be equivalently represented with atomic constraints $x-y\mathrel{\triangleleft}c$ or $x\mathrel{\triangleleft}c$, where $|c|\leq|\bar{x}|\cdot k$.

In the main text (in the discussion preceding Theorem 23 in Section 6), we mention that there exists a computable integer $\lambda$ such that any valuation $\bar{r}$ of $\mathbf{A}$’s clocks can be projected to some valuation $\bar{r}^{\prime}\in[0,\lambda+1)^{|\bar{x}|}$ which $\mathbf{A}$ cannot distinguish from $\bar{r}$. Due to the above observations, we find that $\lambda=|\bar{x}|\cdot k$ meets the stipulated requirements. Hence, in order to decide reachability for $\mathbf{A}$, it is sufficient to consider the bounded subspace $[0,\lambda+1)^{|\bar{x}|}\subseteq\mathbb{R}^{|\bar{x}|}$. This means, given the FOL(LA) encoding $N_{\mathbf{A}}$ of $\mathbf{A}$, we obtain a BSR(BD) encoding $N^{\prime}_{\mathbf{A}}$ of reachability with respect to $\mathbf{A}$ in the following two steps:

(1) Replace every delay clause in $N_{\mathbf{A}}$ with a corresponding finite set of clauses $M$ in accordance with Lemma 22, where we set $\lambda:=|\bar{x}|\cdot k$.

(2) Conjoin the constraints $0\leq x\;\wedge\;x<\kappa$ for $\kappa:=\lambda+1=|\bar{x}|\cdot k+1$ to every constraint in which a base-sort variable $x$ occurs.

Since any $\mathrel{\widehat{\simeq}}_{\lambda+1}$-uniform model of $N^{\prime}_{\mathbf{A}}$ is $\simeq_{\lambda}$-uniform over the subspace $(-\lambda-1,\lambda+1)^{|\bar{x}|}$, Lemma 22 entails that $N^{\prime}_{\mathbf{A}}$ faithfully encodes reachability with respect to $\mathbf{A}$.