11institutetext: M. Cristiá — corresponding author 22institutetext:
Universidad Nacional de Rosario and CIFASIS, Rosario, Argentina – 22email:
<EMAIL_ADDRESS>33institutetext: G. Rossi 44institutetext:
Università di Parma, Parma, Italy – 44email<EMAIL_ADDRESS>
∎

# A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages
Extended with Restricted Quantifiers

Maximiliano Cristiá  Gianfranco Rossi

###### Abstract

Let $\mathcal{L}_{\mathcal{X}}$ be the language of first-order, decidable
theory $\mathcal{X}$. Consider the language,
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$, that extends
$\mathcal{L}_{\mathcal{X}}$ with formulas of the form
$\mathop{\mathstrut{\forall}}\nolimits x\in A:\phi$ (restricted universal
quantifier, RUQ) and $\mathop{\mathstrut{\exists}}\nolimits x\in A:\phi$
(restricted existential quantifier, REQ), where $A$ is a finite set and $\phi$
is a formula made of $\mathcal{X}$-formulas, RUQ and REQ. That is,
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ admits nested restricted
quantifiers. In this paper we present a decision procedure for
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ based on the decision procedure
already defined for the Boolean algebra of finite sets extended with
restricted intensional sets ($\mathcal{L}_{\mathcal{RIS}}$). The
implementation of the decision procedure as part of the $\\{log\\}$ (‘setlog’)
tool is also introduced. The usefulness of the approach is shown through a
number of examples drawn from several real-world case studies.

##  1 Introduction

Restricted quantifiers (RQ) are formulas of the following forms:

$\displaystyle\mathop{\mathstrut{\forall}}\nolimits x\in A:\phi(x)$ (1)
$\displaystyle\mathop{\mathstrut{\exists}}\nolimits x\in A:\phi(x)$ (2)

where $A$ is a set called _quantification domain_. The first form is called
_restricted universal quantifier_ (RUQ), while the second is called
_restricted existential quantifier_ (REQ). The semantics of such formulas is,
respectively:

$\displaystyle\mathop{\mathstrut{\forall}}\nolimits x(x\in
A\Rightarrow\phi(x))$ (3) $\displaystyle\mathop{\mathstrut{\exists}}\nolimits
x(x\in A\mathrel{\wedge}\phi(x))$ (4)

RQ are present in formal notations such as B schneider2001b , TLA+
DBLP:books/aw/Lamport2002  and Z Woodcock00  making it important to be able to
automatically reason about RQ. In fact, RQ allow to express important program
or system properties. For example, one may need to express that some property,
$\phi$, holds for all the users ($U$) of a system. Then, it can be expressed
by means of a RUQ:

$I\mathrel{\widehat{=}}\mathop{\mathstrut{\forall}}\nolimits u\in U:\phi(u)$

Later, one might need to prove that $I$ is a state invariant of that system by
discharging proofs of the form:

$I\mathrel{\wedge}T\Rightarrow I^{\prime}$ (5)

where $T$ is a state transition and $I^{\prime}$ is the result of substituting
every state variable $v$ in $I$ by $v^{\prime}$—i.e., the next-state variable.
In this scenario it would be important if many (or all) of those proofs can be
performed automatically.

In a recent article DBLP:journals/jar/CristiaR21a  we have presented a
decision procedure for a language based on extensional and intensional sets
called $\mathcal{L}_{\mathcal{RIS}}(\mathcal{X})$, where $\mathcal{X}$ is a
first-order, decidable theory. $\mathcal{L}_{\mathcal{RIS}}$ can express RQ
where the inner formula does not contain other RQ. Then,
$\mathcal{L}_{\mathcal{RIS}}$ can automatically discharge a proof such as (5).
However, in general, $\mathcal{L}_{\mathcal{RIS}}$ does not allow for nested
RQ. For example, if $\psi$ is a formula depending on a user and a process, the
following:

$I_{2}\mathrel{\widehat{=}}\mathop{\mathstrut{\forall}}\nolimits u\in
U:(\mathop{\mathstrut{\forall}}\nolimits p\in P:\psi(u,p))$ (6)

where $P$ is the set of processes of the system, is a
$\mathcal{L}_{\mathcal{RIS}}$ formula only if $U$ is not part of $\psi$.
Consequently, the decision procedure defined for $\mathcal{L}_{\mathcal{RIS}}$
is unable to automatically reason about all formulas such as (5) where $I$ is
substituted by $I_{2}$. Therefore, finding a decision procedure for formulas
of the form (5) but involving predicates such as $I_{2}$ would be a valuable
contribution to the formal verification community.

In this paper we depart from $\mathcal{L}_{\mathcal{RIS}}(\mathcal{X})$ to
define a new language, $\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$, admitting
finitely nested RQ at any level, when $\mathcal{L}_{\mathcal{X}}$ is a
quantifier-free, first-order, decidable language111Although in
$\mathcal{L}_{\mathcal{RIS}}(\mathcal{X})$, $\mathcal{L}_{\mathcal{X}}$ can be
a quantified language it make little sense to extend such a language with RQ.
Hence, in this paper we focus on quantifier-free languages that need to be
extended to support at least a restricted form of quantification.. Then,
departing from the decision procedure defined for
$\mathcal{L}_{\mathcal{RIS}}$ we define a decision procedure for
$\mathcal{L}_{\mathcal{RQ}}$. In particular, we provide a precise condition
defining the class of decidable formulas where RUQ and REQ can be arbitrarily
nested. The implementation of these results as part of the $\\{log\\}$
(‘setlog’) tool setlog  is also briefly discussed. More space is committed to
show that the implementation works in practice by providing several examples
of non trivial properties and verification conditions, drawn from real-world
case studies, that $\\{log\\}$ is able to deal with.

The paper is structured as follows. Section 2 introduces
$\mathcal{L}_{\mathcal{RQ}}$ by first giving an informal presentation (2.1)
and then its formal syntax (2.2) and semantics (2.3). The solver for
$\mathcal{L}_{\mathcal{RQ}}$ is presented in Section 3. In Section 4 soundness
and completeness (4.1) and termination (4.2) of the solver are proved. Some
extensions to $\mathcal{L}_{\mathcal{RQ}}$, helping to avoid the introduction
of existential variables, are introduced in Section 5. The implementation of
$\mathcal{L}_{\mathcal{RQ}}$ and its solver as part of $\\{log\\}$ is shown in
Section 6. In that section we also comment on three case studies carried out
with $\\{log\\}$ involving RQ. Our results are discussed and compared with
similar works in Section 7. Section 8 gives our conclusions.

##  2 Formal Syntax and Semantics

This section describes the syntax and semantics of the set-theoretic language
of Restricted Quantifiers, $\mathcal{L}_{\mathcal{RQ}}$. In other words,
$\mathcal{L}_{\mathcal{RQ}}$ builds RQ from fundamental concepts drawn from
set theory. A gentle, informal introduction is provided in Section 2.1,
followed by the formal presentation of the language.

$\mathcal{L}_{\mathcal{RQ}}$ is a first-order predicate language with terms of
sort set and terms designating ur-elements222Ur-elements (also known as atoms
or individuals) are objects which contain no elements but are distinct from
the empty set.. The latter are provided by an external first-order theory
$\mathcal{X}$ (i.e., $\mathcal{L}_{\mathcal{RQ}}$ is parametric with respect
to $\mathcal{X}$). $\mathcal{X}$ must include: a class $\Phi_{\mathcal{X}}$ of
admissible $\mathcal{X}$-formulas based on a set of function symbols
$\mathcal{F}_{\mathcal{X}}$ and a set of predicate symbols $\Pi_{\mathcal{X}}$
(providing at least equality); an interpretation structure
$\mathcal{I}_{\mathcal{X}}$ with domain $\mathcal{D}_{\mathsf{X}}$ and
interpretation function ${(\cdot)}^{\mathcal{I}_{\mathcal{X}}}$; and a
decision procedure $SAT_{\mathcal{X}}$ for $\mathcal{X}$-formulas.
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ denotes the instance of
$\mathcal{L}_{\mathcal{RQ}}$ based on theory $\mathcal{X}$.

$\mathcal{L}_{\mathcal{RQ}}$ provides special set constructors, and a handful
of basic predicate symbols endowed with a pre-designated set-theoretic
meaning. Set constructors are used to construct both restricted intensional
sets (RIS) and extensional sets. Set elements are the objects provided by
$\mathcal{X}$, which are manipulated through the primitive operators that
$\mathcal{X}$ offers. Hence, $\mathcal{L}_{\mathcal{RQ}}$ sets represent
_untyped unbounded finite hybrid sets_ , i.e., unbounded finite sets whose
elements are of arbitrary sorts. $\mathcal{L}_{\mathcal{RQ}}$ formulas are
built in the usual way by using conjunction and disjunction of atomic
formulas.

###  2.1 $\mathcal{L}_{\mathcal{RQ}}$ in a Nutshell

$\mathcal{L}_{\mathcal{RQ}}$ provides three kinds of set terms: , the empty
set; $\\{x\mathbin{\scriptstyle\sqcup}A\\}$, called _extensional set_ whose
interpretation is $\\{x\\}\cup A$; and $\\{c:D|\phi\\}$, called _restricted
intensional set_ (RIS) whose interpretation is $\\{c:c\in
D\mathrel{\wedge}\phi(c)\\}$, where $D$ is called _domain_ and $\phi$ is
called _filter_. At the same time, $\mathcal{L}_{\mathcal{RQ}}$ is a
parametric language w.r.t. the language of some theory $\mathcal{X}$. The
elements of sets are $\mathcal{X}$ elements and the filters of RIS can be
either $\mathcal{X}$ formulas or a very specific kind of
$\mathcal{L}_{\mathcal{RQ}}$ formulas. $\mathcal{X}$ is expected to be a
decidable theory providing at least equality. For example, if $\mathcal{X}$ is
the theory of linear integer arithmetic (LIA) then
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ will allow to reason about formulas
combining RQ over integer formulas.

In $\mathcal{L}_{\mathcal{RQ}}$ formulas are conjunctions and disjunctions of
$\mathcal{L}_{\mathcal{RQ}}$ and $\mathcal{X}$ constraints. In turn,
$\mathcal{L}_{\mathcal{RQ}}$ provides the set equality ($=$), membership
($\in$) and subset ($\subseteq$) relations, as constraints.

###### Example 1

If $\mathcal{X}$ is the theory of LIA then the following is a
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ formula:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr min \in\\{y \mathbin{\scriptstyle\sqcup}S\\} \mathrel{\wedge}\\{y \mathbin{\scriptstyle\sqcup}S\\} \subseteq\\{x:\\{y \mathbin{\scriptstyle\sqcup}S\\} | min \leq x\\} \crcr}$

where $min\leq x$ is a $\mathcal{X}$ constraint. ∎

$\mathcal{L}_{\mathcal{RQ}}$ allows the definition of RUQ in set-theoretic
terms by exploiting the following identity:

$\mathop{\mathstrut{\forall}}\nolimits x\in A:\phi(x)\Leftrightarrow
A\subseteq\\{x:x\in A\mathrel{\wedge}\phi(x)\\}$ (7)

In this way, in $\mathcal{L}_{\mathcal{RQ}}$ we can define a constraint for
RUQ as follows:

$foreach(x\in A,\phi)\mathrel{\widehat{=}}A\subseteq\\{x:A|\phi\\}$ (8)

Then, the formula of Example 1 can be written more compactly as follows:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr min \in\\{y
\mathbin{\scriptstyle\sqcup}S\\} \mathrel{\wedge}foreach(x \in\\{y
\mathbin{\scriptstyle\sqcup}S\\}, min \leq x) \crcr}$

Likewise, REQ can also be defined as constraints:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr exists(x \in A,
\phi) \mathrel{\widehat{=}}n \in A \mathrel{\wedge}\phi(n) \crcr}$

where $n$ is a new variable.

Furthermore, in $\mathcal{L}_{\mathcal{RQ}}$, the filter of a RIS can be a
conjunction of $\mathcal{X}$, $foreach$ and $exists$ constraints. This is an
important difference w.r.t. $\mathcal{L}_{\mathcal{RIS}}$
DBLP:journals/jar/CristiaR21a  because there, RIS filters can only be
$\mathcal{X}$ formulas. The possibility of including $foreach$ and $exists$
constraints in RIS filters allows for the definition of nested RQ (what is not
possible in $\mathcal{L}_{\mathcal{RIS}}$). For example:

$\displaystyle\mathop{\mathstrut{\forall}}\nolimits x\in
X:(\mathop{\mathstrut{\forall}}\nolimits y\in Y:\phi(x,y)))\Leftrightarrow
X\subseteq\\{x:x\in X\mathrel{\wedge}(\mathop{\mathstrut{\forall}}\nolimits
y\in Y:\phi(x,y))\\}$ $\displaystyle\Leftrightarrow X\subseteq\\{x:x\in
X\mathrel{\wedge}(Y\subseteq\\{y:(y\in Y:\phi(x,y))\\})\\}$

The latter being equivalent to the following $\mathcal{L}_{\mathcal{RQ}}$
formula:

$foreach(x\in X,foreach(y\in Y,\phi(x,y)))$

which can be further simplified by introducing some syntactic sugar:

$foreach([x\in X,y\in Y],\phi(x,y))$

In the next two subsections a formal presentation of
$\mathcal{L}_{\mathcal{RQ}}$ is made and in later sections its decidability is
analyzed.

###  2.2 Syntax

The $\mathcal{L}_{\mathcal{RQ}}$ syntax is defined primarily by giving the
signature upon which terms and formulas of the language are built.

######  Definition 1 (Signature)

The signature $\Sigma_{\mathcal{RQ}}$ of $\mathcal{L}_{\mathcal{RQ}}$ is a
triple $\langle\mathcal{F},\Pi,\mathcal{V}\rangle$ where:

  * •

$\mathcal{F}$ is the set of function symbols, partitioned as
$\mathcal{F}=\mathcal{F}_{\mathcal{S}}\cup\mathcal{F}_{\mathcal{X}}$, where
$\mathcal{F}_{\mathcal{S}}$ contains ,
$\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$ and $\\{\cdot:\cdot|\cdot\\}$,
while $\mathcal{F}_{\mathcal{X}}$ contains the function symbols provided by
the theory $\mathcal{X}$ (at least, a constant and the binary function symbol
$(\cdot,\cdot)$).

  * •

$\Pi$ is the set of _primitive_ predicate symbols, partitioned as
$\Pi=\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}\cup\Pi_{\mathcal{X}}$ where
$\Pi_{\mathcal{S}}\mathrel{\widehat{=}}\\{=_{\mathcal{S}},\in,\subseteq\\}$
and $\Pi_{\mathcal{T}}\mathrel{\widehat{=}}\\{set,\mathit{isX}\\}$, while
$\Pi_{\mathcal{X}}$ contains the predicate symbols provided by the theory
$\mathcal{X}$ (at least $=_{\mathcal{X}}$).

  * •

$\mathcal{V}$ is a denumerable set of variables, partitioned as
$\mathcal{V}=\mathcal{V}_{\mathcal{S}}\cup\mathcal{V}_{\mathcal{X}}$. ∎

Intuitively, , $\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$ and
$\\{\cdot:\cdot|\cdot\\}$ are interpreted as outlined at the beginning of
Section 2.1. $=_{\mathcal{X}}$ is interpreted as the identity in
$\mathcal{D}_{\mathsf{X}}$, while $(\cdot,\cdot)$ will be used to represent
ordered pairs.

Sorts of function and predicate symbols are specified as follows: if $f$
(resp., $\pi$) is a function (resp., a predicate) symbol of arity $n$, then
its sort is an $n+1$-tuple $\langle s_{1},\ldots,s_{n+1}\rangle$ (resp., an
$n$-tuple $\langle s_{1},\ldots,s_{n}\rangle$) of non-empty subsets of the set
$\\{\mathsf{Set},\mathsf{X}\\}$ of sorts. This notion is denoted by $f:\langle
s_{1},\ldots,s_{n+1}\rangle$ (resp., by $\pi:\langle
s_{1},\ldots,s_{n}\rangle$). Specifically, the sorts of the elements of
$\mathcal{F}$ and $\mathcal{V}$ are the following.

######  Definition 2 (Sorts of function symbols and variables)

The sorts of the symbols in $\mathcal{F}$ are as follows:

$\displaystyle\varnothing:\langle\\{\mathsf{Set}\\}\rangle$
$\displaystyle\mathsf{\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}:\langle\\{\mathsf{X}\\},\\{\mathsf{Set}\\},\\{\mathsf{Set}\\}\rangle}$
$\displaystyle\mathsf{\\{\cdot:\cdot|\cdot\\}:\langle\\{\mathsf{X}\\},\\{\mathsf{Set}\\},}\\{\Phi_{\mathcal{RQ}}\\},\mathsf{\\{\mathsf{Set}\\}\rangle}$
$\displaystyle
f:\langle\underbrace{\\{\mathsf{X}\\},\ldots,\\{\mathsf{X}\\}}_{n},\\{{\sf\mathsf{X}}\\}\rangle\text{,
if $f\in\mathcal{F}_{\mathcal{X}}$ is of arity $n\geq 0$}.$

where $\Phi_{\mathcal{RQ}}$ represents the set of $\mathcal{RQ}$-formulas
defined in Definition 6. The sorts of variables are as follows:

$\displaystyle v:\langle\\{\mathsf{Set}\\}\rangle\text{, if
$v\in\mathcal{V}_{\mathcal{S}}$}$ $\displaystyle
v:\langle\\{\mathsf{X}\\}\rangle\text{, if $v\in\mathcal{V}_{\mathcal{X}}$}$ ∎

######  Definition 3 (Sorts of predicate symbols)

The sorts of the predicate symbols in $\Pi$ are as follows:

$\displaystyle=_{\mathcal{S}}:\langle\\{\mathsf{Set}\\},\\{\mathsf{Set}\\}\rangle$
$\displaystyle=_{\mathcal{X}}:\langle\\{\mathsf{X}\\},\\{\mathsf{X}\\}\rangle$
$\displaystyle\in:\langle\\{\mathsf{X}\\},\\{\mathsf{Set}\\}\rangle$
$\displaystyle\subseteq:\langle\\{\mathsf{Set}\\},\\{\mathsf{Set}\\}\rangle$
$\displaystyle set,\mathit{isX}:\langle\\{\mathsf{Set},\mathsf{X}\\}\rangle$ ∎

Whenever it is clear from context we will write $=$ instead of
$=_{\mathcal{S}}$ or $=_{\mathcal{X}}$.

######  Definition 4 ($\mathcal{RQ}$-terms)

Let $\mathcal{T}_{\mathcal{RQ}}^{0}$ be the set of terms generated by the
following grammar:

$\displaystyle\mathcal{T}_{\mathcal{RQ}}^{0}::=\mathit{Elem}\quad|\quad\mathit{Set}$
$\displaystyle\mathit{Elem}::=\mathcal{T}_{\mathcal{X}}\quad|\quad\mathcal{V}_{\mathcal{X}}$
$\displaystyle\mathit{Ctrl}::=\mathcal{V}_{\mathcal{X}}\hskip 2.0pt|\hskip
5.0pt\text{\'{}}(\text{\'{}}\,\,\mathit{Ctrl}\,\,\hskip
5.0pt\text{\'{}},\text{\'{}}\,\,\mathit{Ctrl}\hskip
5.0pt\text{\'{}})\text{\'{}}$ $\displaystyle
Ext::=\text{\'{}}\varnothing\text{\'{}}\quad|\quad\mathcal{V}_{\mathcal{S}}\quad|\quad\text{\'{}}\\{\text{\'{}}\hskip
5.0ptElem\hskip 5.0pt\text{\'{}}\mathbin{\scriptstyle\sqcup}\text{\'{}}\hskip
5.0ptExt\hskip 5.0pt\text{\'{}}\\}\text{\'{}}$
$\displaystyle\mathit{Ris}::=\hskip 5.0pt\text{\'{}}\\{\text{\'{}}\hskip
5.0pt\mathit{Ctrl}\hskip 5.0pt\text{\'{}}:\text{\'{}}\hskip
5.0pt\mathit{Ext}\hskip 5.0pt\text{\'{}}|\text{\'{}}\hskip
5.0pt\Phi_{\mathcal{RQ}}\hskip 5.0pt\text{\'{}}\\}\text{\'{}}\hskip 5.0pt$
$\displaystyle Set::=Ris\quad|\quad Ext$

where $\mathcal{T}_{\mathcal{X}}$ represents the set of non-variable
$\mathcal{X}$-terms; $\Phi_{\mathcal{RQ}}$ is the set of
$\mathcal{RQ}$-formulas defined in Definition 6; and variables occurring in a
$Ctrl$-term must all be distinct from each other.

The set of _$\mathcal{RQ}$ -terms_, denoted by $\mathcal{T}_{\mathcal{RQ}}$,
is the maximal subset of $\mathcal{T}_{\mathcal{RQ}}^{0}$ complying with the
sorts as given in Definition 2. ∎

If $t$ is a term $f(t_{1},\dots,t_{n})$, $f\in\mathcal{F},n\geq 0$, and
$\langle s_{1},\ldots,s_{n+1}\rangle$ is the sort of $f$, then we say that $t$
is of sort $\langle s_{n+1}\rangle$. The sort of any $\mathcal{RQ}$-term $t$
is always $\langle\\{\mathsf{Set}\\}\rangle$ or
$\langle\\{\mathsf{X}\\}\rangle$. For the sake of simplicity, we simply say
that $t$ is of sort $\mathsf{Set}$ or $\mathsf{X}$, respectively. In
particular, we say that a $\mathcal{RQ}$-term of sort $\mathsf{Set}$ is a _set
term_ , that set terms of the form
$\\{t_{1}\mathbin{\scriptstyle\sqcup}t_{2}\\}$ are _extensional_ set terms,
and that terms of the form $\\{t_{1}:t_{2}|\phi\\}$ are RIS terms. The first
argument of an extensional set term is called _element part_ and the second is
called _set part_. In turn, the first argument of a RIS term is called
_control term_ , the second is the _domain_ and the third one is the _filter_.

As can be seen in Definition 4, control terms can be either variables or
nested ordered pairs. The utility of the latter will be precisely motivated
and discussed in Section 5. Note that the domain of a RIS term can be the
empty set, a set variable or an extensional set.

Hereafter, we will use the following notation for extensional set terms:
$\\{t_{1},t_{2},\dots,t_{n}\mathbin{\scriptstyle\sqcup}t\\}$, $n\geq 1$, is a
shorthand for
$\\{t_{1}\mathbin{\scriptstyle\sqcup}\\{t_{2}\,\mathbin{\scriptstyle\sqcup}\,\cdots\\{t_{n}\mathbin{\scriptstyle\sqcup}t\\}\cdots\\}\\}$,
while $\\{t_{1},t_{2},\dots,t_{n}\\}$ is a shorthand for
$\\{t_{1},t_{2},\dots,t_{n}\mathbin{\scriptstyle\sqcup}\varnothing\\}$.

######  Definition 5 ($\mathcal{RQ}$-constraints)

If $\pi\in\Pi$ is a predicate symbol of sort $\langle
s_{1},\ldots,s_{n}\rangle$, and for each $i=1,\ldots,n$, $t_{i}$ is a
$\mathcal{RQ}$-term of sort $\langle s^{\prime}_{i}\rangle$ with
$s^{\prime}_{i}\subseteq s_{i}$, then:

  1. 1.

If $\pi$ is $\subseteq$, then $\pi(t_{1},t_{2})$ is a
$\mathcal{RQ}$-constraint if
$t_{2}\equiv\\{Ctrl:t_{1}|\Phi_{\mathcal{RQ}}\\}$, where $Ctrl$ and
$\Phi_{\mathcal{RQ}}$ are as in Definition 4.

  2. 2.

If $\pi$ is $\in$, then $\pi(t_{1},t_{2})$ is a $\mathcal{RQ}$-constraint if
$t_{2}$ is an $Ext$ term as in Definition 4.

  3. 3.

If $\pi$ is $=_{\mathcal{S}}$, then $\pi(t_{1},t_{2})$ is a
$\mathcal{RQ}$-constraint if $t_{1}$ and $t_{2}$ are $Ext$ terms as in
Definition 4.

  4. 4.

If $\pi$ is any other element of $\Pi$, then $\pi(t_{1},\ldots,t_{n})$ a
$\mathcal{RQ}$-constraint.

The set of $\mathcal{RQ}$-constraints is denoted by
$\mathcal{C}_{\mathcal{RQ}}$. ∎

The $\mathcal{RQ}$-constraints based on symbols in $\Pi_{\mathcal{S}}$ will be
called _set constraints_. Note that the conditions on $\subseteq$-constraints
forces them to be RUQ as in (7).

Finally, we define the set of $\mathcal{RQ}$-formulas as follows.

######  Definition 6 ($\mathcal{RQ}$-formulas)

The set of $\mathcal{RQ}$-formulas, denoted by $\Phi_{\mathcal{RQ}}$, is given
by the following grammar:

$\displaystyle\Phi_{\mathcal{RQ}}::=true\mid
false\mid\Phi_{\mathcal{X}}\mid\mathcal{C}_{\mathcal{RQ}}\mid\Phi_{\mathcal{RQ}}\mathrel{\wedge}\Phi_{\mathcal{RQ}}\mid\Phi_{\mathcal{RQ}}\mathrel{\vee}\Phi_{\mathcal{RQ}}$

where $\Phi_{\mathcal{X}}$ and $\mathcal{C}_{\mathcal{RQ}}$ represent any
element belonging to the class of $\mathcal{X}$-formulas and
$\mathcal{RQ}$-constraints, respectively. ∎

As can be seen, $\mathcal{L}_{\mathcal{RQ}}$ is based solely on fundamental
concepts of set theory.

######  Remark 1 (Notation)

We will use the following naming conventions, unless stated differently:
$A,B,C,D$ stand for terms of sort $\mathsf{Set}$; $a,b,c,d,x,y,z$ stand for
terms of sort $\mathsf{X}$; and $t,u,v$ stand for terms of any of the two
sorts. A symbol such as $\dot{A}$ states that $A\in\mathcal{V}$. Finally,
$n,n_{i}$ stand for new variables of sort $\mathsf{X}$; and $N,N_{i}$ for new
variables of sort $\mathsf{Set}$; no dot above them will be used. ∎

######  Remark 2 ($\mathcal{L}_{\mathcal{RQ}}$ vs.
$\mathcal{L}_{\mathcal{RIS}}$)

As we have pointed out in Section 1, $\mathcal{L}_{\mathcal{RQ}}$ departs from
$\mathcal{L}_{\mathcal{RIS}}$ DBLP:journals/jar/CristiaR21a .
$\mathcal{L}_{\mathcal{RQ}}$ is a sublanguage of $\mathcal{L}_{\mathcal{RIS}}$
except for one modification which extends $\mathcal{L}_{\mathcal{RIS}}$.
Indeed, $\mathcal{L}_{\mathcal{RIS}}$ admits the same function and predicate
symbols than $\mathcal{L}_{\mathcal{RQ}}$, plus some other or more complex
versions of them. For example, in $\mathcal{L}_{\mathcal{RIS}}$ RIS terms have
a more complex structure and union, intersection, etc. of RIS terms are
available.

However, in $\mathcal{L}_{\mathcal{RIS}}$ filters can only be
$\mathcal{L}_{\mathcal{X}}$ formulas. In $\mathcal{L}_{\mathcal{RQ}}$ filters
can be nested RQ ending in an $\mathcal{L}_{\mathcal{X}}$ formula. This
extension is crucial to extend the expressiveness of the language (cf. formula
(6)). The restriction on filters to $\mathcal{L}_{\mathcal{X}}$ formulas in
$\mathcal{L}_{\mathcal{RIS}}$ is key to define a decision procedure for it. If
this restriction is lifted, termination of the decision algorithm is
compromised. As we will shown in Section 4, there are subclasses of formulas
admitting nested RQ that do not compromise termination. ∎

###  2.3 Semantics

Sorts and symbols in $\Sigma_{\mathcal{RQ}}$ are interpreted according to the
interpretation structure
$\mathcal{R}\mathrel{\widehat{=}}\langle\mathcal{D},(\cdot)^{\mathcal{R}}\rangle$,
where $\mathcal{D}$ and $(\cdot)^{\mathcal{R}}$ are defined as follows.

######  Definition 7 (Interpretation domain)

The interpretation domain $D$ is partitioned as
$\mathcal{D}\mathrel{\widehat{=}}\mathcal{D}_{\mathsf{Set}}\cup\mathcal{D}_{\mathsf{X}}$
where:

  * •

$\mathcal{D}_{\mathsf{Set}}$ is the set of all hereditarily finite hybrid sets
built from elements in $\mathcal{D}$. Hereditarily finite sets are those sets
that admit (hereditarily finite) sets as their elements, that is sets of sets.

  * •

$\mathcal{D}_{\mathsf{X}}$ is a collection of other objects. ∎

######  Definition 8 (Interpretation function)

The interpretation function $(\cdot)^{\mathcal{R}}$ is defined as follows:

  * •

Each sort $\mathsf{S}\in\\{\mathsf{Set},\mathsf{X}\\}$ is mapped to the domain
$\mathcal{D}_{\mathsf{S}}$.

  * •

For each sort $\mathsf{S}$, each variable $x$ of sort $\mathsf{S}$ is mapped
to an element $x^{\mathcal{R}}$ in $\mathcal{D}_{\mathsf{S}}$.

  * •

The constant and function symbols in $\mathcal{F}_{\mathcal{S}}$ are mapped to
elements in $\mathcal{D}_{\mathsf{S}}$ as follows:

    * –

is interpreted as the empty set, namely ${}^{\mathcal{R}}=\emptyset$

    * –

$\\{x\mathbin{\scriptstyle\sqcup}A\\}$ is interpreted as the set
$\\{x^{\mathcal{R}}\\}\cup A^{\mathcal{R}}$.

    * –

Let $\vec{x}$ be a vector of variables occurring in $c$ and $\vec{v}$ a vector
of other variables, then the set $\\{c(\vec{x}):X|\phi(\vec{x},\vec{v})\\}$ is
interpreted as the set:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr\\{y :
\mathop{\mathstrut{\exists}}\nolimits\vec{x} (c(\vec{x}) \in_\mathcal{X}X
\mathrel{\wedge}\phi(\vec{x},\vec{v}))\\} \crcr}$

Note that in RIS terms, $\vec{x}$ are “local” variables whose scope is the RIS
itself, while $\vec{v}$ are “non-local” variables whose scope is the formula
where the RIS is participating in.

  * •

The predicate symbols in $\Pi$ are interpreted as follows:

    * –

$A=_{\mathcal{S}}B$ is interpreted as $A^{\mathcal{R}}=B^{\mathcal{R}}$, where
$=$ is the identity relation in $\mathcal{D}_{\mathsf{Set}}$

    * –

$x=_{\mathcal{X}}y$ is interpreted as $x^{\mathcal{R}}=y^{\mathcal{R}}$, where
$=$ is the identity relation in $\mathcal{D}_{\mathsf{X}}$

    * –

$x\in A$ is interpreted as $x^{\mathcal{R}}\in A^{\mathcal{R}}$

    * –

$A\subseteq B$ is interpreted as $A^{\mathcal{R}}\subseteq B^{\mathcal{R}}$

    * –

$\mathit{isX}(t)$ is interpreted as
$t^{\mathcal{R}}\in\mathcal{D}_{\mathsf{X}}$

    * –

$set(t)$ is interpreted as $t^{\mathcal{R}}\in\mathcal{D}_{\mathsf{Set}}$. ∎

The interpretation structure $\mathcal{R}$ is used to map each
$\mathcal{RQ}$-formula $\Phi$ to a truth value
$\Phi^{\mathcal{R}}=\\{true,false\\}$ in the following way: set constraints
(resp., $\mathcal{X}$ constraints) are evaluated by $(\cdot)^{\mathcal{R}}$
according to the meaning of the corresponding predicates in set theory (resp.,
in theory $\mathcal{X}$) as defined above; $\mathcal{RQ}$-formulas are
evaluated by $(\cdot)^{\mathcal{R}}$ according to the rules of propositional
logic. A $\mathcal{L}_{\mathcal{RQ}}$-formula $\Phi$ is _satisfiable_ iff
there exists an assignment $\sigma$ of values from $\mathcal{D}$ to the free
variables of $\Phi$, respecting the sorts of the variables, such that
$\Phi[\sigma]$ is true in $\mathcal{R}$, i.e.,
$\mathcal{R}\models\Phi[\sigma]$. In this case, we say that $\sigma$ is a
_successful valuation_ (or, simply, a _solution_) of $\Phi$.

##  3 A Solver for $\mathcal{L}_{\mathcal{RQ}}$

In this section we present a constraint solver for
$\mathcal{L}_{\mathcal{RQ}}$, called $SAT_{\mathcal{RQ}}$. The solver provides
a collection of rewrite rules for rewriting $\mathcal{L}_{\mathcal{RQ}}$
formulas that are proved to be a decision procedure for some subclasses of
$\mathcal{L}_{\mathcal{RQ}}$ formulas (see Section 4). As already observed,
however, checking the satisfiability of $\mathcal{RQ}$-formulas depends on the
existence of a decision procedure for $\mathcal{X}$-formulas (i.e., formulas
over $\mathcal{L}_{\mathcal{X}}$).

###  3.1 The Solver

$SAT_{\mathcal{RQ}}$ is a rewriting system whose global organization is shown
in Algorithm 1, where STEP is the core of the algorithm.

sort  infer is used to automatically add $\Pi_{\mathcal{T}}$-constraints to
the input formula $\Phi$ to force arguments of $\mathcal{RQ}$-constraints in
$\Phi$ to be of the proper sorts (see Remark 3 below). sort  infer is called
twice in Algorithm 1: first, at the beginning of the algorithm, and second,
within procedure STEP for the constraints that are generated during constraint
processing. sort  check checks $\Pi_{\mathcal{T}}$-constraints occurring in
$\Phi$: if they are satisfiable, then $\Phi$ is returned unchanged; otherwise,
$\Phi$ is rewritten to $false$.

procedure $\mathsf{STEP}$($\Phi$)  for all $\pi\in\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}:\Phi\leftarrow\mathsf{rw}_{\pi}(\Phi)$;  $\Phi\leftarrow\mathsf{sort\leavevmode\vbox{\hrule width=5.0pt}check}(\mathsf{sort\leavevmode\vbox{\hrule width=5.0pt}infer}(\Phi))$ return $\Phi$ procedure $\mathsf{rw}_{\pi}$($\Phi$)  if $\Phi=\mbox{}\dots\mathrel{\wedge}false\mathrel{\wedge}\cdots$ then return $false$ else repeat let  $\Phi$ be  $c_{1}\mathrel{\wedge}\dots\mathrel{\wedge}c_{m}$ select a $\pi$-constraint $c_{i}$ in $\Phi$ apply any applicable rule to $c_{i}$ until no rule applies to any $\pi$-constraint  return $\Phi$ |  procedure $SAT_{\mathcal{RQ}}$($\Phi$)  $\Phi\leftarrow\textsf{sort\leavevmode\kern 0.59998pt\vbox{\hrule width=5.0pt}infer}(\Phi)$ repeat $\Phi^{\prime}\leftarrow\Phi$ $\Phi\leftarrow\textsf{STEP}(\Phi)$ until $\Phi=\Phi^{\prime}$ $\Phi\textbf{ is }\Phi_{\mathcal{S}}\mathrel{\wedge}\Phi_{\mathcal{X}}$ $\Phi\leftarrow\Phi_{\mathcal{S}}\mathrel{\wedge}SAT_{\mathcal{X}}(\Phi_{\mathcal{X}})$ return $\Phi$
---|---
Algorithm 1 The $SAT_{\mathcal{RQ}}$ solver. $\Phi$ is the input formula.

STEP applies specialized rewriting procedures to the current formula $\Phi$
and returns either $false$ or the modified formula. Each rewriting procedure
applies a few non-deterministic rewrite rules which reduce the syntactic
complexity of $\mathcal{RQ}$-constraints of one kind. Procedure
$\mathsf{rw}_{\pi}$ in Algorithm 1 represents the rewriting procedure for
($\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$)-constraints. The execution of STEP
is iterated until a fixpoint is reached—i.e., the formula cannot be simplified
any further. STEP returns $false$ whenever (at least) one of the procedures in
it rewrites $\Phi$ to $false$. In this case, a fixpoint is immediately
detected, since $\textsf{STEP}(false)$ returns $false$.

$SAT_{\mathcal{X}}$ is the constraint solver for $\mathcal{X}$-formulas. The
formula $\Phi$ can be seen, without loss of generality, as
$\Phi_{\mathcal{S}}\mathrel{\wedge}\Phi_{\mathcal{X}}$, where
$\Phi_{\mathcal{S}}$ is a pure $\mathcal{RQ}$-formula (basically, a
$\mathcal{RQ}$-formula with with no $\mathcal{X}$-formula in it—see Definition
12) and $\Phi_{\mathcal{X}}$ is an $\mathcal{X}$-formula. $SAT_{\mathcal{X}}$
is applied only to the $\Phi_{\mathcal{X}}$ conjunct of $\Phi$. Note that,
conversely, STEP rewrites only $\mathcal{RQ}$-constraints, while it leaves all
other atoms unchanged. Nonetheless, as the rewrite rules show,
$SAT_{\mathcal{RQ}}$ generates $\mathcal{X}$-formulas that are conjoined to
$\Phi_{\mathcal{X}}$ so they are later solved by $SAT_{\mathcal{X}}$.

As we will show in Section 4, when all the non-deterministic computations of
$SAT_{\mathcal{RQ}}(\Phi)$ return $false$, then we can conclude that $\Phi$ is
unsatisfiable; otherwise, we can conclude that $\Phi$ is satisfiable and each
solution of the formulas returned by $SAT_{\mathcal{RQ}}$ is a solution of
$\Phi$, and vice versa.

###### Remark 3

$\mathcal{L}_{\mathcal{RQ}}$ does not provide variable declarations. The sort
of variables are enforced by adding suitable _sort constraints_ to the formula
to be processed. Sort constraints are automatically added by the solver.
Specifically, a constraint $set(y)$ (resp., $\mathit{isX}(y)$) is added for
each variable $y$ which is required to be of sort $set$ (resp., $\mathsf{X}$).
For example, given $B=\\{y\mathbin{\scriptstyle\sqcup}A\\}$, sort  infer
conjoins the sort constraints $set(B)$, $\mathit{isX}(y)$ and $set(A)$. If the
set of function and predicate symbols of $\mathcal{L}_{\mathcal{RQ}}$ and
$\mathcal{L}_{\mathcal{X}}$ are disjoint, there is a unique sort constraint
for each variable in the formula. ∎

###  3.2 Rewrite Rules

The rewrite rules used by $SAT_{\mathcal{RQ}}$ are defined as follows.

######  Definition 9 (Rewrite rules)

If $\pi$ is a symbol in $\Pi_{\mathcal{S}}\cup\Pi_{\mathcal{T}}$ and $p$ is a
$\mathcal{RQ}$-constraint based on $\pi$, then a _rewrite rule for
$\pi$-constraints_ is a rule of the form
$p\longrightarrow\Phi_{1}\mathrel{\vee}\dots\mathrel{\vee}\Phi_{n}$, where
$\Phi_{i}$, $i\geq 1$, are $\mathcal{RQ}$-formulas. Each atom matching $p$ is
non-deterministically rewritten to one of the $\Phi_{i}$. Variables appearing
in the right-hand side but not in the left-hand side are assumed to be fresh
variables, implicitly existentially quantified over each $\Phi_{i}$.
Conjunction has higher precedence than disjunction. ∎

A _rewriting procedure_ for $\pi$-constraints consists of the collection of
all the rewrite rules for $\pi$-constraints. For each rewriting procedure,
STEP selects rules in the order they are listed in Figure 1. The first rule
whose left-hand side matches the input $\pi$-constraint is used to rewrite it.

Subset $\displaystyle\varnothing\subseteq\\{x:A|\phi(x)\\}\longrightarrow
true$ (9) $\displaystyle\\{a\sqcup A\\}\subseteq\\{x:\\{a\sqcup
A\\}|\phi(x)\\}\longrightarrow\phi(a)\mathrel{\wedge}A\subseteq\\{x:A|\phi(x)\\}$
(10)
$\displaystyle\dot{A}\subseteq\\{x:\dot{A}|\phi(x)\\}\longrightarrow\textsc{irreducible}$
(11) Membership $\displaystyle a\in\varnothing\longrightarrow false$ (12)
$\displaystyle a\in\\{b\sqcup A\\}\longrightarrow
a=_{\mathcal{X}}b\mathrel{\vee}a\in A$ (13) $\displaystyle
a\in\dot{A}\longrightarrow\dot{A}=\\{a\sqcup N\\}$ (14) Equality
$\displaystyle\varnothing=\varnothing\longrightarrow true$ (15)
$\displaystyle\dot{A}=\dot{A}\longrightarrow true$ (16) $\displaystyle
B=\dot{A}\longrightarrow\dot{A}=B\text{, if $B\notin\mathcal{V}$}$ (17)
$\displaystyle\dot{A}=B\longrightarrow\dot{A}=B\text{, and substitute $A$ by
$B$ in the rest of the formula}$ (18) $\displaystyle\\{a\sqcup
A\\}=\varnothing\longrightarrow false$ (19)
$\displaystyle\varnothing=\\{a\sqcup A\\}\longrightarrow false$ (20)
$\displaystyle\\{a\sqcup A\\}=\\{b\sqcup B\\}\longrightarrow$ (21)
$\displaystyle\qquad a=_{\mathcal{X}}b\mathrel{\wedge}A=B$
$\displaystyle\qquad\mathrel{\vee}a=_{\mathcal{X}}b\mathrel{\wedge}\\{a\sqcup
A\\}=B\mathrel{\vee}a=_{\mathcal{X}}b\mathrel{\wedge}A=\\{b\sqcup
B\\}\mathrel{\vee}A=\\{b\sqcup N\\}\mathrel{\wedge}B=\\{a\sqcup N\\}$
$\displaystyle\dot{A}=B\longrightarrow\text{{irreducible}, if $\dot{A}$ does
not occur elsewhere in the formula}$ (22)

Figure 1: Rewrite rules for $\mathcal{RQ}$-constraints

Rules whose right-hand side is irreducible indicate that the constraint at the
left-hand side is not rewritten and will remain as it is all the way to the
final answer returned by Algorithm 1. In Figure 1, we have made explicit
equality in $\mathcal{L}_{\mathcal{X}}$ by means of $=_{\mathcal{X}}$. All
other instances of $=$ correspond to equality in $\mathcal{L}_{\mathcal{RQ}}$
(i.e., set equality).

As shown in Figure 1, there are rewriting procedures for
$\subseteq$-constraints (Subset), $\in$-constraints (Membership) and
$=$-constraints (Equality). The Membership and Equality rules deal only with
extensional sets due to the restrictions given in Definition 5. Observe that
all other constraints generated by the rules of Figure 1 are
$\mathcal{X}$-constraints which are dealt with by $SAT_{\mathcal{X}}$. All the
rules in the figure are borrowed from the $\mathcal{L}_{\mathcal{RIS}}$ solver
DBLP:journals/jar/CristiaR21a . This is important because it simplifies the
proof of some important properties of $SAT_{\mathcal{RQ}}$ (Section 4).

As can be seen, most of the rules are straightforward. Rule (21) is the main
rule of set unification Dovier2006 . Set unification is pervasive in other
logics developed by the authors DBLP:journals/jar/CristiaR20 ;
DBLP:journals/jar/CristiaR21a . This rule states when two non-empty, non-
variable sets are equal by non-deterministically and recursively computing
four cases. These cases implement the _Absorption_ and _Commutativity on the
left_ properties of set theory Dovier00 . As an example, by applying rule (21)
to $\\{1\\}=\\{1,1\\}$ we get:
($1=1\mathrel{\wedge}\varnothing=\\{1\\})\mathrel{\vee}(1=1\mathrel{\wedge}\\{1\\}=\\{1\\})\mathrel{\vee}(1=1\mathrel{\wedge}\varnothing=\\{1,1\\})\mathrel{\vee}(\varnothing=\\{1\mathbin{\scriptstyle\sqcup}\dot{N}\\}\mathrel{\wedge}\\{1\mathbin{\scriptstyle\sqcup}\dot{N}\\}=\\{1\\})$,
which turns out to be true (due to the second disjunct).

Rules (9)-(11) process RUQ by implementing (7). Rule (10) iterates over all
the elements of the domain of the RIS until it becomes the empty set or a
variable. In each iteration one of the elements of the domain is proved to
verify the filter (if not, the rule fails), and a new iteration is fired. If
the domain becomes a variable the constraint is not processed any more. Note
that a constraint such as $\dot{A}\subseteq\\{x:\dot{A}|\phi(x)\\}$ is
trivially satisfied by substituting $\dot{A}$ by the empty set.

As $\mathcal{L}_{\mathcal{RQ}}$, $SAT_{\mathcal{RQ}}$ is based solely on
fundamental concepts of set theory.

###### Remark 4

Observe that when $\subseteq$ are rewritten only the following are generated:

  * •

$\phi\in\Phi_{\mathcal{X}}$

  * •

$A\subseteq\\{x:A|\phi(x)\\}$

∎

###  3.3 Irreducible Constraints

When no rewrite rule is applicable to the current $\mathcal{RQ}$-formula
$\Phi$ and $\Phi$ is not $false$, the main loop of $SAT_{\mathcal{RQ}}$
terminates returning $\Phi$ as its result. This formula can be seen, without
loss of generality, as $\Phi_{\mathcal{S}}\mathrel{\wedge}\Phi_{\mathcal{X}}$,
where $\Phi_{\mathcal{X}}$ contains all (and only) $\mathcal{X}$ constraints
and $\Phi_{\mathcal{S}}$ contains all other constraints occurring in $\Phi$.

The following definition precisely characterizes the form of atomic
constraints in $\Phi_{\mathcal{S}}$.

######  Definition 10 (Irreducible formula)

Let $\Phi$ and $\phi$ be $\mathcal{RQ}$-formulas,
$A\in\mathcal{V}_{\mathcal{S}}$, $x$ a control term (thus it is a term of sort
$\mathsf{X}$) and $t$ a term of sort $\mathsf{Set}$. A
$\mathcal{RQ}$-constraint $p$ occurring in $\Phi$ is _irreducible_ if it has
one of the following forms:

  1. 1.

$A=t$, and neither $t$ nor $\Phi\setminus\\{A=t\\}$ contain $A$

  2. 2.

$A\subseteq\\{x:A|\phi(x)\\}$

A $\mathcal{RQ}$-formula $\Phi$ is irreducible if it is $true$ or if all of
its $\mathcal{RQ}$-constraints are irreducible. ∎

$\Phi_{\mathcal{S}}$, as returned by $SAT_{\mathcal{RQ}}$’s main loop, is an
irreducible formula. This fact can be checked by inspecting the rewrite rules
presented in Figure 1. This inspection is straightforward as there are no
rules rewriting irreducible constraints and all non-irreducible form
constraints are rewritten by some rule.

It is important to observe that the atomic constraints occurring in
$\Phi_{\mathcal{S}}$ are indeed quite simple. In particular, all non-variable
set terms occurring in the input formula have been removed, except those
occurring as right-hand side of $=$ constraints.

##  4 Decidability of $\mathcal{L}_{\mathcal{RQ}}$ Formulas

In this section we analyze the soundness, completeness and termination
properties of $SAT_{\mathcal{RQ}}$ for different subclasses of
$\mathcal{RQ}$-formulas.

As we have explained in Remark 2, $\mathcal{L}_{\mathcal{RQ}}$ is a
sublanguage of $\mathcal{L}_{\mathcal{RIS}}$ except for the fact that
$\mathcal{L}_{\mathcal{RQ}}$ admits RQ in filters. We also pointed out that
accepting RQ in filters poses termination problems; soundness and completeness
are not affected. Actually, as noted in Section 3, all the rules of Figure 1
are rules borrowed from the $\mathcal{L}_{\mathcal{RIS}}$ solver. Hence, we
will briefly analyze soundness and completeness of $SAT_{\mathcal{RQ}}$ and
will spend more time analyzing its termination.

As RUQ and REQ play a central role in this work, we provide some syntactic
sugar for them.

######  Definition 11 (Restricted Quantifiers)

Given a control term $x$, an extensional set term $A$ and a formula $\phi$, a
_restricted universal quantifier_ (RUQ), noted $foreach(x\in A,\phi)$, is
defined as:

$foreach(x\in A,\phi)\mathrel{\widehat{=}}A\subseteq\\{x:A|\phi(x)\\}$ (23)

Under the same terms, a _restricted existential quantifier_ (REQ), noted
$exists(x\in A,\phi)$, is defined as:

$exists(x\in A,\phi)\mathrel{\widehat{=}}n\in A\mathrel{\wedge}\phi(n)$ (24)

where all variables occurring in $n$ are fresh variables not occurring
elsewhere in the formula of which the REQ is a part. ∎

In a RQ: $x$ is called _control term_ or _quantified variable_ , $A$ is called
_domain_ and $\phi$ is called _filter_ (following the vocabulary of RIS
terms). Note that in both RUQ and REQ, $\phi$ must depend on $x$.

######  Definition 12 (Subclasses of $\Phi_{\mathcal{RQ}}$)

The following are the subclasses of $\Phi_{\mathcal{RQ}}$-formulas for which
decidability will be analyzed:

  * •

$\Phi_{nrq}$ is the subclass of $\Phi_{\mathcal{RQ}}$ whose elements are
nested RQ. The subclasses of formulas to be analyzed will be subclasses of
$\Phi_{nrq}$.

$\displaystyle\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{\mathcal{X}}::=foreach(Ctrl\in
Ext,\Phi_{\mathcal{X}})$
$\displaystyle\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{\mathcal{X}}::=exists(Ctrl\in
Ext,\Phi_{\mathcal{X}})$
$\displaystyle\Phi_{mix}::=\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{\mathcal{X}}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{\mathcal{X}}\mid
foreach(Ctrl\in Ext,\Phi_{mix})\mid exists(Ctrl\in Ext,\Phi_{mix})$
$\displaystyle\Phi_{nrq}::=true\mid
false\mid\Phi_{\mathcal{X}}\mid\Phi_{mix}\mid\Phi_{\mathcal{RQ}}\mathrel{\wedge}\Phi_{\mathcal{RQ}}\mid\Phi_{\mathcal{RQ}}\mathrel{\vee}\Phi_{\mathcal{RQ}}$

  * •

$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$ is the subclass of $\Phi_{nrq}$
whose elements are built from $\Phi_{\mathcal{X}}$ and nested RUQ.

$\displaystyle\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{p}::=\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{\mathcal{X}}\mid
foreach(Ctrl\in Ext,\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{p})$
$\displaystyle\Phi_{\mathop{\mathstrut{\forall}}\nolimits}::=\Phi_{\mathcal{X}}\mid\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{p}\mid\Phi_{\mathop{\mathstrut{\forall}}\nolimits}\mathrel{\wedge}\Phi_{\mathop{\mathstrut{\forall}}\nolimits}\mid\Phi_{\mathop{\mathstrut{\forall}}\nolimits}\mathrel{\vee}\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$

  * •

$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ is the subclass of $\Phi_{nrq}$
whose elements are built from $\Phi_{\mathcal{X}}$ and nested REQ.

$\displaystyle\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{p}::=\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{\mathcal{X}}\mid
exists(Ctrl\in Ext,\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{p})$
$\displaystyle\Phi_{\mathop{\mathstrut{\exists}}\nolimits}::=\Phi_{\mathcal{X}}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{p}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits}\mathrel{\wedge}\Phi_{\mathop{\mathstrut{\exists}}\nolimits}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits}\mathrel{\vee}\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$

  * •

$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
is the subclass of $\Phi_{nrq}$ whose elements are built from
$\Phi_{\mathcal{X}}$ and nested RQ where all REQ are _before_ all RUQ (if
any).

$\displaystyle\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}::=\Phi_{\mathcal{X}}\mid
exists(Ctrl\in
Ext,Filter)\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}\mathrel{\wedge}\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}\mathrel{\vee}\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
$\displaystyle
Filter::=\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{p}\mid\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}^{p}$

  * •

$\Phi_{\mathcal{RQ}}^{p}$ is the subclass of $\Phi_{nrq}$ whose elements are
pure $\mathcal{RQ}$-formulas.

$\displaystyle\Phi_{\mathcal{RQ}}^{p}::=true\mid
false\mid\Phi_{mix}\mid\Phi_{\mathcal{RQ}}^{p}\mathrel{\wedge}\Phi_{\mathcal{RQ}}^{p}\mid\Phi_{\mathcal{RQ}}^{p}\mathrel{\vee}\Phi_{\mathcal{RQ}}^{p}$

Similar definitions can be given for pure
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$,
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ and
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
formulas. ∎

###### Example 2

Different classes of formulas.

  * •

$foreach(x\in A,foreach(y\in B,x=y))$ is a
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$ formula.

  * •

$exists(x\in A,exists(y\in B,\neg\;x=y))$ is a
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ formula.

  * •

$exists(x\in A,foreach(y\in B,x=y))$ is a
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
formula.

  * •

$foreach(x\in A,exists(y\in B,x=y))$ is a $\Phi_{\mathcal{RQ}}^{p}$ formula. ∎

As can be seen, formulas in $\Phi_{nrq}$ are conjunctions and disjunctions of
$\mathcal{X}$-formulas and nested RQ; the filter of the innermost RQ is an
$\mathcal{X}$-formula. Note that not every $\mathcal{RQ}$-constraint can be
part of a formula in $\Phi_{nrq}$; the idea is to restrict them to be RQ.
Hence, basically, we analyze the decidability of $\mathcal{RQ}$-formulas
strictly encoding RQ. However, note that when $SAT_{\mathcal{RQ}}$ processes a
$\Phi_{nrq}$-formula it may generate a formula outside $\Phi_{nrq}$. For
example, $exists(x\in\dot{A},\phi(x))$ is rewritten into
$n\in\dot{A}\mathrel{\wedge}\phi(n)$ which then is rewritten into
$A=\\{n\mathbin{\scriptstyle\sqcup}N\\}\mathrel{\wedge}\phi(n)$, which is not
a $\Phi_{nrq}$-formula due to the presence of
$A=\\{n\mathbin{\scriptstyle\sqcup}N\\}$.

######  Remark 5 (Notation)

From now on, we will write $foreach([x\in A,y\in B],\phi)$ as a shorthand for
$foreach(x\in A,foreach(y\in B,\phi))$, and $exists([x\in A,y\in B],\phi)$ as
a shorthand for $exists(x\in A,exists(y\in B,\phi))$. Besides,
$foreach(\vec{x}_{n}\in\vec{A}_{n},\phi)$ denotes $foreach([x_{1}\in
A_{1},\dots x_{n}\in A_{n}],\phi)$ and
$exists(\vec{x}_{n}\in\vec{A}_{n},\phi)$ denotes $exists([x_{1}\in A_{1},\dots
x_{n}\in A_{n}],\phi)$, $0\leq n$ (if $n=0$ we take $\phi$ as the resulting
formula). ∎

With this notation it is easy to see that: in pure
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}^{p}$ formulas there are only
constraints of the form $foreach(\vec{x}_{n}\in\vec{A}_{n},\phi)$ for some
$\mathcal{X}$-formula $\phi$; in pure
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}^{p}$ formulas there are only
constraints of the form $exists(\vec{x}_{n}\in\vec{A}_{n},\phi)$ for some
$\mathcal{X}$-formula $\phi$; and in pure
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}^{p}$
formulas there are only constraints of the form
$exists(\vec{x}_{n}\in\vec{A}_{n},foreach(\vec{y}_{m}\in\vec{B}_{m},\phi))$
for some $\mathcal{X}$-formula $\phi$ ($0<n,0\leq m$).

###  4.1 Soundness and Completeness

The following theorem ensures that, after termination, the rewriting process
implemented by $SAT_{\mathcal{RQ}}$ preserves the set of solutions of the
input formula.

######  Theorem 1 (Equisatisfiability)

Let $\Phi$ be a $\Phi_{nrq}$-formula and $\Phi^{1},\Phi^{2},\dots,\Phi^{n}$ be
the collection of $\mathcal{RQ}$-formulas returned by
$SAT_{\mathcal{RQ}}(\Phi)$. Then
$\Phi^{1}\mathrel{\vee}\Phi^{2}\mathrel{\vee}\dots\mathrel{\vee}\Phi^{n}$ is
equisatisfiable to $\Phi$, that is, every possible solution333More precisely,
each solution of $\Phi$ expanded to the variables occurring in $\Phi^{i}$ but
not in $\Phi$, so as to account for the possible fresh variables introduced
into $\Phi^{i}$. of $\Phi$ is a solution of one of the $\Phi^{i}$s and, vice
versa, every solution of one of these formulas is a solution for $\Phi$.

###### Proof

The proof rests on a series of lemmas each showing that the set of solutions
of left and right-hand sides of each rewrite rule are the same. Given that the
rewrite rules of Figure 1 are those used to define the solver for
$\mathcal{L}_{\mathcal{RIS}}$, then the lemmas proved for
$\mathcal{L}_{\mathcal{RIS}}$ still apply (DBLP:journals/jar/CristiaR21a, ,
Appendix C.4). The only concern with those lemmas might be the fact that they
were proved under the assumption that RIS filters do not admit RQ. However, it
is trivial to see that all the Membership and Equality rules and rules (9) and
(11) are unaffected by the fact that filters admit RQ. For the remaining rule,
i.e. (10), we reproduce in Appendix A the proof made for
$\mathcal{L}_{\mathcal{RIS}}$ so readers can check that it do not depend on
any limitation over RIS filters. ∎

######  Theorem 2 (Satisfiability of the output formula)

Any $\mathcal{RQ}$-formula different from $false$ returned by
$SAT_{\mathcal{RQ}}$ is satisfiable w.r.t. the underlying interpretation
structure $\mathcal{R}$.

###### Proof

As we have explained, each disjunct of the formula returned by
$SAT_{\mathcal{RQ}}$ can be written as
$\Phi_{\mathcal{S}}\mathrel{\wedge}\Phi_{\mathcal{X}}$, where
$\Phi_{\mathcal{S}}$ is a pure $\mathcal{RQ}$-formula and $\Phi_{\mathcal{X}}$
is an $\mathcal{X}$-formula.

Since $SAT_{\mathcal{X}}$ is called on $\Phi_{\mathcal{X}}$ we know that it is
satisfiable (under the assumption that $SAT_{\mathcal{RQ}}$ has not returned
$false$).

Now we prove that $\Phi_{\mathcal{S}}$ is satisfiable, too. We know that
$\Phi_{\mathcal{S}}$ is an irreducible formula (Definition 10). Then, we have
to prove that an irreducible formula is always satisfiable. Given that an
irreducible formula is a conjunction of irreducible constraints, we have to
prove that all these constraints can be simultaneously satisfied. Constraints
of the form $\dot{A}=t$ are satisfied by binding $\dot{A}$ to $t$ (recall from
Definition 10 that $\dot{A}$ does not occur 3in the rest of an irreducible
formula); constraints of the form $\dot{A}\subseteq\\{x:\dot{A}|\phi(x)\\}$
are satisfied by substituting the domain of the RIS by the empty set. Hence,
there is always a solution for an irreducible $\mathcal{RQ}$-formula.

Finally, we prove that $\Phi_{\mathcal{S}}\mathrel{\wedge}\Phi_{\mathcal{X}}$
can be satisfied. Indeed, observe that the solution for $\Phi_{\mathcal{S}}$
do not bind variables of sort $\mathsf{X}$ and that $\Phi_{\mathcal{X}}$ do
not contain variables of sort $\mathsf{Set}$. So the values of the solution
for $\Phi_{\mathcal{X}}$ do no conflict with the values of the solution for
$\Phi_{\mathcal{S}}$. ∎

The following example shows how Theorem 2 works in practice.

###### Example 3

Consider the following nested RUQ where $\phi$ is an $\mathcal{X}$-formula:

$foreach([x\in\\{a\mathbin{\scriptstyle\sqcup}\dot{A}\\},y\in\\{b\mathbin{\scriptstyle\sqcup}\dot{B}\\}],\phi(x,y))$
(25)

$SAT_{\mathcal{RQ}}$ applies (23) and rule (10) twice yielding:

$\phi(a,b)\mathrel{\wedge}foreach(y\in\dot{B},\phi(a,y))\mathrel{\wedge}foreach([x\in\dot{A},y\in\\{b\mathbin{\scriptstyle\sqcup}\dot{B}\\}],\phi(x,y))$

Now, it calls $SAT_{\mathcal{X}}(\phi(a,b))$ because both $foreach$
constraints are irreducible. Thus, determining the satisfiability of (25) is
reduced to determining the satisfiability of $\phi(a,b)$ because
satisfiability of the two $foreach$ constraints is guaranteed by Theorem 2
(with $A\leftarrow\varnothing,B\leftarrow\varnothing$). ∎

Thanks to Theorems 1 and 2 we can conclude that, given a $\Phi_{nrq}$-formula
$\Phi$, then $\Phi$ is satisfiable with respect to the intended interpretation
structure $\mathcal{R}$ if and only if there is a non-deterministic choice in
$SAT_{\mathcal{RQ}}(\Phi)$ that returns a $\mathcal{RQ}$-formula different
from $false$. Conversely, if all the non-deterministic computations of
$SAT_{\mathcal{RQ}}(\Phi)$ terminate with $false$, then $\Phi$ is surely
unsatisfiable. Note that these theorems have been proved for any
$\Phi_{nrq}$-formula.

###  4.2 Termination

The problem is that termination of $SAT_{\mathcal{RQ}}$ cannot be proved for
every $\Phi_{nrq}$-formula, as shown by the following example.

###### Example 4

The following nested RQ where $\phi$ is an $\mathcal{X}$-formula, is rewritten
as indicated.

$\displaystyle
foreach(x\in\\{a\mathbin{\scriptstyle\sqcup}A\\},exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\},\phi(x,y)))$
[by rule (10)] $\displaystyle\longrightarrow
exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\},\phi(a,y))$
$\displaystyle\qquad{}\mathrel{\wedge}foreach(x\in
A,exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\}:\phi(x,y)))$ [by Def. 11,
(24)] $\displaystyle\longrightarrow
n\in\\{b\mathbin{\scriptstyle\sqcup}A\\}\mathrel{\wedge}\phi(a,n)\mathrel{\wedge}foreach(x\in
A,exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\}:\phi(x,y)))$

Now there are two cases from $n\in\\{b\mathbin{\scriptstyle\sqcup}A\\}$: $n=b$
and $n\in A$ (rule (13)). Let us see the second one:

$\displaystyle n\in A\mathrel{\wedge}\phi(a,n)\mathrel{\wedge}foreach(x\in
A,exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\}:\phi(x,y)))$ [by rule (14)]
$\displaystyle\longrightarrow
A=\\{n\mathbin{\scriptstyle\sqcup}N\\}\mathrel{\wedge}\phi(a,n)$
$\displaystyle\qquad{}\mathrel{\wedge}foreach(x\in
A,exists(y\in\\{b\mathbin{\scriptstyle\sqcup}A\\}:\phi(x,y)))$ [by rule (18)]
$\displaystyle\longrightarrow
A=\\{n\mathbin{\scriptstyle\sqcup}N\\}\mathrel{\wedge}\phi(a,n)\mathrel{\wedge}foreach(x\in\\{n\mathbin{\scriptstyle\sqcup}N\\},exists(y\in\\{b,n\mathbin{\scriptstyle\sqcup}N\\}:\phi(x,y)))$

It is clear that the last $foreach$ is structurally equal to the initial
formula. Without more information about $\phi$ this could potentially cause an
infinite loop making $SAT_{\mathcal{RQ}}$ not to terminate. ∎

Before presenting the theorems stating termination on different subclasses of
$\Phi_{nrq}$-formulas, consider the following analysis. Let $\phi$ be a
$\Phi_{nrq}$-formula. If $\phi=\phi_{1}\mathrel{\vee}\phi_{2}$, then we prove
$SAT_{\mathcal{RQ}}$ terminates on $\phi_{1}$ and then on $\phi_{2}$. Hence,
as concerns termination, we can consider $\phi$ to be a conjunction of
$\Phi_{nrq}$-formulas. In this case $\phi$ can be written as
$\phi_{\mathcal{S}}\mathrel{\wedge}\phi_{\mathcal{X}}$ where
$\phi_{\mathcal{S}}$ is a pure $\Phi_{nrq}$-formula and $\phi_{\mathcal{X}}$
is a $\mathcal{X}$-formula. We need to prove termination of
$SAT_{\mathcal{RQ}}$ on $\phi_{\mathcal{S}}$, as termination of
$SAT_{\mathcal{X}}$ on $\phi_{\mathcal{X}}$ is guaranteed by the assumption
that $SAT_{\mathcal{X}}$ is a decision procedure for
$\mathcal{L}_{\mathcal{X}}$. Now, if $\phi_{\mathcal{S}}$ is a disjunction, we
prove termination for each disjunct. Hence, in the following theorems we prove
termination of $SAT_{\mathcal{RQ}}$ on conjunctions of pure
$\mathcal{RQ}$-constraints belonging to different subclasses of formulas.

######  Theorem 3 (Termination on
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$ formulas)

The $SAT_{\mathcal{RQ}}$ procedure can be implemented as to ensure termination
for every conjunction of pure $\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$
constraints.

###### Proof

Recall that the only constraint in pure
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$ formulas is of the form
$foreach(\vec{x}_{n}\in\vec{A}_{n},\phi)$, $0<n$ and
$\phi\in\Phi_{\mathcal{X}}$. First we will prove that $SAT_{\mathcal{RQ}}$
terminates on these constraints. The proof is by induction on $n$.

  * •

Base case. Let $\phi$ be a $\mathcal{L}_{\mathcal{X}}$ formula. We will show
that $SAT_{\mathcal{RQ}}$ terminates on the following RUQ:

$foreach(x\in A,\phi(x))$ (26)

    * –

$A=\varnothing$, this case is trivial as rule (9) terminates immediately.

    * –

$A\in\mathcal{V}_{\mathcal{S}}$, this case is trivial as rule (11) terminates
immediately.

    * –

$A=\\{b\mathbin{\scriptstyle\sqcup}B\\}$, rule (10) is applied to (26)
yielding:

$\phi(b)\mathrel{\wedge}foreach(x\in B,\phi(x))$

The recursive call to $foreach$ is made with a domain strictly smaller than
$A$. This is so because the call is made with $B$ and because $\phi(b)$ cannot
bind a value to $B$ since $\phi$ is $\mathcal{X}$-formula and $B$ is of sort
$\mathsf{Set}$ (the only way of binding a value to $B$ is by means of $t\in B$
or $B=t$, for some term $t$, which are not generated during
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits}$ processing, Remark 4). Then,
$SAT_{\mathcal{RQ}}$ will terminate when the ‘end’ of $B$ is reached (i.e.,
when a variable or the empty set is found).

  * •

Induction hypothesis. $SAT_{\mathcal{RQ}}$ terminates on every constraint of
the form $foreach(\vec{x}_{k}\in\vec{A}_{k},\phi)$ with $k\leq n$, for any
$\mathcal{X}$-formula $\phi$.

  * •

Induction step. Let $\phi$ be any $\mathcal{X}$-formula. We will prove that
$SAT_{\mathcal{RQ}}$ terminates on the following constraint:

$foreach(x\in A,foreach(\vec{x}_{n}\in\vec{A}_{n},\phi(x,\vec{x})))$ (27)

    * –

$A=\varnothing$, this case is trivial as rule (9) terminates immediately.

    * –

$A\in\mathcal{V}_{\mathcal{S}}$, this case is trivial as rule (11) terminates
immediately.

    * –

$A=\\{b\mathbin{\scriptstyle\sqcup}B\\}$, rule (10) is applied to (27)
yielding:

$foreach(\vec{x}_{n}\in\vec{A}_{n},\phi(b,\vec{x}))\mathrel{\wedge}foreach(x\in
B,foreach(\vec{x}_{n}\in\vec{A}_{n},\phi(x,\vec{x})))$

$SAT_{\mathcal{RQ}}$ terminates on the first conjunct by the induction
hypothesis. Besides, the recursive call in the second conjunct is made with a
domain strictly smaller than $A$. This is so because the call is made with $B$
and because the first conjunct cannot bind a value to $B$ since it is a RUQ or
an $\mathcal{X}$-formula and $B$ is of sort $\mathsf{Set}$. Then,
$SAT_{\mathcal{RQ}}$ will terminate when the ‘end’ of $B$ is reached (i.e.,
when a variable or the empty set are found).

Observe that termination depends solely on the size of the domain of the RUQ.
If $\phi_{\mathcal{S}}$ is a conjunction of RUQ, then termination of
$SAT_{\mathcal{RQ}}$ on each RUQ implies termination of $SAT_{\mathcal{RQ}}$
for the whole formula. Indeed, when a given RUQ is processed it can only
generate a shorter RUQ or a $\mathcal{L}_{\mathcal{X}}$ formula. In either
case, nothing is generated that can bind a value to a domain. Then, the domain
of a RUQ in $\phi_{\mathcal{S}}$ is not affected by the processing of the
other RUQ in the formula. ∎

Before proving termination of $SAT_{\mathcal{RQ}}$ on
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ formulas we need the following
lemma.

###### Lemma 1

$SAT_{\mathcal{RQ}}$ terminates on any $\mathcal{RQ}$-formula without RQ.

###### Proof

Let $\phi$ be a $\mathcal{RQ}$-formula without RQ. Write $\phi$ as
$\phi_{\mathcal{S}}\mathrel{\wedge}\phi_{\mathcal{X}}$. Hence,
$\phi_{\mathcal{S}}$ is comprised solely of membership and equality
constraints. Then, only the Membership and Equality rules of Figure 1 will be
used by $SAT_{\mathcal{RQ}}$. These rules have been proved to constitute a
terminating rewriting system elsewhere (Dovier00, , Theorem 10.10). ∎

######  Theorem 4 (Termination on
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ formulas)

The $SAT_{\mathcal{RQ}}$ procedure can be implemented as to ensure termination
for every conjunction of pure $\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$
constraints.

###### Proof

Let $\phi$ be an $\mathcal{X}$-formula. Consider the following rewriting:

$\displaystyle exists([x\in A,y\in B],\phi(x,y))$ [by Def. 11, (24)]
$\displaystyle\longrightarrow n_{1}\in A\mathrel{\wedge}exists(y\in
B,\phi(n_{1},y))$ [by Def. 11, (24)] $\displaystyle\longrightarrow n_{1}\in
A\mathrel{\wedge}n_{2}\in B\mathrel{\wedge}\phi(n_{1},n_{2})$

Then, all REQ are quickly eliminated from the formula. This can be easily
generalized to $exists(\mathbf{x}_{n}\in\mathbf{A}_{n},\phi)$ for any
$\mathcal{X}$-formula $\phi$ and any $0<n$. The resulting non-$\mathcal{X}$
subformula is a $\mathcal{RQ}$-formula without RQ. Hence, by Lemma 1,
$SAT_{\mathcal{RQ}}$ terminates on that formula. Given that conjunctions of
REQ are rewritten into conjunctions of formulas such as the last one above,
$SAT_{\mathcal{RQ}}$ terminates on every conjunction of pure
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits}$ formulas. ∎

######  Theorem 5 (Termination on
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
formulas)

The $SAT_{\mathcal{RQ}}$ procedure can be implemented as to ensure termination
for every conjunction of pure
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
constraints.

###### Proof

Recall that the only constraints in pure
$\Phi_{\mathop{\mathstrut{\exists}}\nolimits\mathop{\mathstrut{\forall}}\nolimits}$
formulas are of the form:

$exists(\vec{x}_{k}\in\vec{A}_{k},foreach(\vec{y}_{m}\in\vec{B}_{m},\phi))$
(28)

for some $\mathcal{X}$-formula $\phi$, $0<k$ and $0\leq m$ (if $m=0$, then
$\phi$ is the innermost filter).

First we prove termination on such a constraint. By using the same reasoning
of Theorem 4, (28) is rewritten into:

$n_{1}\in A_{1}\mathrel{\wedge}\dots\mathrel{\wedge}n_{k}\in
A_{k}\mathrel{\wedge}foreach(\vec{y}_{m}\in\vec{B}_{m},\phi)$ (29)

Then, $SAT_{\mathcal{RQ}}$ process $n_{1}\in
A_{1}\mathrel{\wedge}\dots\mathrel{\wedge}n_{k}\in A_{k}$. By Lemma 1,
$SAT_{\mathcal{RQ}}$ terminates on that conjunction. The processing of this
conjunction either terminates in $false$, and so $SAT_{\mathcal{RQ}}$ stops,
or it yields a conjunction of the form:

$(\bigwedge_{i=1}^{v}X_{i}=t_{i})\mathrel{\wedge}(\bigwedge_{i=1}^{w}Y_{i}=u_{i})$
(30)

where $X_{i}\in\mathcal{V}_{\mathcal{S}}$,
$Y_{i}\in\mathcal{V}_{\mathcal{X}}$, $t_{i}$ are set terms and $u_{i}$ are
$\mathcal{X}$ terms.

If some $B_{j}$ in $\vec{B}$ is either $X_{i}$ or
$\\{\dots\mathbin{\scriptstyle\sqcup}X_{i}\\}$, then $X_{i}$ is substituted by
$t_{i}$. This rewrites $foreach(\vec{y}_{m}\in\vec{B}_{m},\phi)$ into
$foreach(\vec{y}_{m}\in\vec{B}^{\prime}_{m},\phi)$. Then we have the following
formula:

$(\bigwedge_{i=1}^{v}X_{i}=t_{i})\mathrel{\wedge}(\bigwedge_{i=1}^{w}Y_{i}=u_{i})\mathrel{\wedge}foreach(\vec{y}_{m}\in\vec{B}^{\prime}_{m},\phi)$
(31)

By Theorem 3 $SAT_{\mathcal{RQ}}$ terminates on
$foreach(\vec{y}_{m}\in\vec{B}^{\prime}_{m},\phi)$. While processing the RUQ,
$SAT_{\mathcal{RQ}}$ can only generate either RUQ or $\mathcal{X}$-formulas
(Remark 4). Then, the main loop of $SAT_{\mathcal{RQ}}$ terminates. It only
remains to call $SAT_{\mathcal{X}}$ on the $\mathcal{X}$-subformula, which
will terminate under the assumption that it is a decision procedure. Hence,
$SAT_{\mathcal{RQ}}$ terminates on (28).

Now we prove that $SAT_{\mathcal{RQ}}$ terminates on a conjunction of
constraints such as (28). We can think that $SAT_{\mathcal{RQ}}$ will process
each such constraint by going through formulas (29)-(31). Processing each
final RUQ can only generate either RUQ or $\mathcal{X}$-formulas. Then, the
main loop of $SAT_{\mathcal{RQ}}$ terminates. ∎

Now we consider a more general subclass of $\Phi_{nrq}$-formulas which,
however, must obey a restriction concerning the domains of REQ that go _after_
RUQ in mixed RQ (some times called _alternating quantifiers_
DBLP:journals/lmcs/FeldmanPISS19 ).

We say that an RQ has a _variable domain_ if its domain is either a variable
or an extensional set whose set part is a variable. Moreover, we say that the
variable of the domain is the domain itself (if it is a variable) or its set
part. For example, in:

$foreach(x\in\\{h\mathbin{\scriptstyle\sqcup}\dot{A}\\},exists(y\in\dot{B},\phi(x,y)))$
(32)

$\\{h\mathbin{\scriptstyle\sqcup}\dot{A}\\}$ is a variable domain whose
variable is $A$, and $\dot{B}$ is variable domain whose variable is $B$.

The class of formulas we are about to define will avoid formulas such as the
one in Example 4. The problem with that formula is that there is an $exists$
constraint _after_ a $foreach$ constraint with the same domain variable ($A$).
In this situation when the $foreach$ constraint picks an element ($a$) of its
domain the $exists$ constraint hypothesizes the existence of a new element
($n$) in $A$ as to satisfy $\phi$. As now $n\in A$, the $foreach$ constraint
must pick $n$ making the $exists$ constraint to hypothesize the existence of
another new element in $A$. This behavior may produce an infinite rewriting
loop. In a sense, the $exists$ constraint feeds back the $foreach$ constraint
with new elements _if they have the same domain variable_. This problem can be
generalized to conjunctions of RQ.

###### Example 5

The following formula:

$\displaystyle
foreach(x\in\\{h\mathbin{\scriptstyle\sqcup}\dot{A}\\},exists(y\in\dot{B},\phi(x,y)))$
$\displaystyle{}\mathrel{\wedge}foreach(z\in\dot{B},exists(w\in\\{b\mathbin{\scriptstyle\sqcup}\dot{A}\\},\psi(z,w)))$

may produce an infinite loop even though the $foreach$ and $exists$
constraints sharing the same domain variable ($A$) are in different RUQ.
Still, in a sense, the $exists$ constraint with domain variable $A$ is _after_
the $foreach$ constraint with the same domain variable: from the $A$ in the
$foreach$ we go to the $B$ in the $exists$, from this we go to the $B$ in the
$foreach$ which leads us to the $A$ in the $exists$. ∎

Therefore, the mathematics we are going to define are meant to characterize
formulas such as those in Examples 4 and 5.

Let $\phi_{1}\mathrel{\wedge}\dots\mathrel{\wedge}\phi_{n}$ be a conjunction
of nested RQ. Each RQ in a nested RQ is indexed by its position in the chain.
For instance, in (32) the $foreach$ constraint has index 1 while the $exists$
constraint has index 2. For each $\phi_{i}$ build the function, called _domain
function of $\phi_{i}$_, whose ordered pairs are of the form
$((i,j),(\mathsf{Q}_{j}^{i},D_{j}^{i}))$ where:

  * •

A pair with first component $(i,j)$ is in the domain function of $\phi_{i}$
iff the RQ with index $j$ in $\phi_{i}$ has a variable domain.

  * •

$D_{j}^{i}$ is the domain variable of the RQ with index $j$ in $\phi_{i}$.

  * •

$\mathsf{Q}_{j}^{i}$ is $\mathop{\mathstrut{\forall}}\nolimits$ if the $j$ RQ
is a $foreach$ constraint and is $\mathop{\mathstrut{\exists}}\nolimits$ if
the RQ is an $exists$ constraint, in $\phi_{i}$.

Hence, the domain function of the formula of Example 5 is:

$\\{((1,1),(\mathop{\mathstrut{\forall}}\nolimits,A)),((1,2),(\mathop{\mathstrut{\exists}}\nolimits,B)),((2,1),(\mathop{\mathstrut{\forall}}\nolimits,B)),((2,2),(\mathop{\mathstrut{\exists}}\nolimits,A))\\}$

From the domain functions build a directed graph, called _domain graph_ ,
whose nodes are the ordered pairs of the domain functions. The edges are built
as follows:

  1. 1.

If $((i,j),(\mathop{\mathstrut{\forall}}\nolimits,D_{j}^{i}))$ and
$((i,k),(\mathop{\mathstrut{\exists}}\nolimits,D_{k}^{i}))$, with $j<k$, are
in a domain function, then
$((i,j),(\mathop{\mathstrut{\forall}}\nolimits,D_{j}^{i}))\rightarrow((i,k),(\mathop{\mathstrut{\exists}}\nolimits,D_{k}^{i}))$
is an edge of the domain graph.

  2. 2.

If $((i,j),(\mathop{\mathstrut{\exists}}\nolimits,D))$ and
$((b,a),(\mathop{\mathstrut{\forall}}\nolimits,D))$ are in domain functions
with $i\neq b$, then
$((i,j),(\mathop{\mathstrut{\exists}}\nolimits,D))\rightarrow((b,a),(\mathop{\mathstrut{\forall}}\nolimits,D))$
is an edge of the domain graph.

Hence, the domain graph of the formula of Example 5 is:

$\displaystyle((1,1),(\mathop{\mathstrut{\forall}}\nolimits,A))\rightarrow((1,2),(\mathop{\mathstrut{\exists}}\nolimits,B)),((2,1),(\mathop{\mathstrut{\forall}}\nolimits,B))\rightarrow((2,2),(\mathop{\mathstrut{\exists}}\nolimits,A)),$
$\displaystyle((1,2),(\mathop{\mathstrut{\exists}}\nolimits,B))\rightarrow((2,1),(\mathop{\mathstrut{\forall}}\nolimits,B)),((2,2),(\mathop{\mathstrut{\exists}}\nolimits,A))\rightarrow((1,1),(\mathop{\mathstrut{\forall}}\nolimits,A))$

Consider the domain graph of a conjunction of pure $\mathcal{RQ}$-constraints.
A path in the graph such as:

$\displaystyle((i_{1},j_{11}),(\mathop{\mathstrut{\forall}}\nolimits,D))\rightarrow((i_{1},j_{12}),(\mathop{\mathstrut{\exists}}\nolimits,D_{1}))\;\rightarrow$
$\displaystyle((i_{2},j_{21}),(\mathop{\mathstrut{\forall}}\nolimits,D_{1}))\rightarrow((i_{2},j_{22}),(\mathop{\mathstrut{\exists}}\nolimits,D_{2}))\rightarrow$
$\displaystyle\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdot\cdot\rightarrow$
$\displaystyle((i_{n},j_{n1}),(\mathop{\mathstrut{\forall}}\nolimits,D_{n-1}))\rightarrow((i_{n},j_{n2}),(\mathop{\mathstrut{\exists}}\nolimits,D))$

where $i_{a}\neq i_{b}$ if $a\neq b$ for all $a,b\in[1,n]$, is called a
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
_loop_. Note that the first and last domain variables in a
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loop are the same ($D$).

We say that a conjunction of RQ is free of
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops if there are no
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loop in its domain graph.
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
is the set of conjunctions of RQ free of
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops. Note that
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
includes all the $\Phi_{nrq}$-formulas where there are no variable domains.

######  Theorem 6 (Termination on
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
formulas)

The $SAT_{\mathcal{RQ}}$ procedure can be implemented as to ensure termination
for every formula in
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$.

###### Proof

First we prove that $SAT_{\mathcal{RQ}}$ terminates on an atomic formula,
$\psi$. It starts by removing from $\psi$ all the leading $exists$ constraints
(if any) and then proceeding as in Theorem 5. Hence, we get a formula such as
(31):

$(\bigwedge_{i=1}^{v}X_{i}=t_{i})\mathrel{\wedge}(\bigwedge_{i=1}^{w}Y_{i}=u_{i})\mathrel{\wedge}foreach(\vec{y}_{m}\in\vec{B}^{\prime}_{m},\Phi)$

but where $\Phi$ is a mixed RQ (eventually ending in a $\mathcal{X}$-formula)
whose domains might have been changed during the substitution step (see proof
of Theorem 5).

Now, $SAT_{\mathcal{RQ}}$ processes the $foreach$ constraint as in Theorem 3.
Here, though, we cannot easily conclude that RUQ processing cannot bind a
value to $\vec{B}^{\prime}$ because after the leading RUQ there might be some
REQ. The problem with REQ is that they generate constraints of the form $n\in
A$, for some domain $A$. Then, if the variable of $A$ happens to be a variable
in $\vec{B}^{\prime}$ (or in some RUQ in $\Phi$) we will have an infinite loop
as in Examples 4 and 5. However, since $\psi$ belongs to
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$,
we know that there is no domain variable shared between a RUQ and a REQ ahead
of it because $\psi$ is free from
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops. Hence, we can arrive at the same conclusion of Theorem 3 meaning that
$SAT_{\mathcal{RQ}}$ terminates on $\psi$.

Now we prove that $SAT_{\mathcal{RQ}}$ terminates on a conjunction of
constraints such as $\psi$. Again, all the leading $exists$ constraints (if
any) are removed from each $\psi_{i}$ thus generating a formula such as (31)
but with a conjunction of $foreach$ constraints444$foreach_{i}$ means that all
its elements are renamed accordingly: $\vec{y}_{i,m_{i}}$,
$\vec{B}^{\prime}_{i,m_{i}}$, $\Phi_{i}$.:

$(\bigwedge_{i=1}^{v}X_{i}=t_{i})\mathrel{\wedge}(\bigwedge_{i=1}^{w}Y_{i}=u_{i})\mathrel{\wedge}(\bigwedge_{i=1}^{q}foreach_{i}(\vec{y}_{m}\in\vec{B}^{\prime}_{m},\Phi))$

with $0\leq v,w,q$.

As above, $SAT_{\mathcal{RQ}}$ processes all the $foreach_{i}$ (as in Theorem
3) and, again, the problem are the $n\in A$ constraints ($A$ a variable
domain) that might be generated by the possible REQ present in each
$\Phi_{i}$. Differently from the base case, here a $n\in A$ constraint
generated when $foreach_{a}$ is processed might affect a domain variable of a
$foreach$ constraint present in $foreach_{b}$ with $a\neq b$, as shown in
Example 5. However, since the formula belongs to
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
we know is free from
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops. This includes loops starting with a $foreach$ domain variable in
$foreach_{a}$ and ending with the same domain variable in an $exists$
constraint present in $foreach_{b}$. Then, no $n\in A$ constraint can affect a
$foreach$ domain variable. Therefore, $SAT_{\mathcal{RQ}}$ terminates. ∎

We close this section with the following two observations.

###### Remark 6

$SAT_{\mathcal{RQ}}$ terminates for some formulas in
$\Phi_{nrq}\setminus\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$.
For example, the following is a slight variation of the formula of Example 4:

$foreach(x\in\dot{A},exists(y\in\\{b\mathbin{\scriptstyle\sqcup}\dot{A}\\},\phi(x,y)))$

for which $SAT_{\mathcal{RQ}}$ trivially terminates because the formula is
irreducible given that the domain is a variable (rule (11) applies). We could
have tighten the definition of
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
as to include this kind of formulas. However, we consider that these formulas
do not constitute a proper subclass as termination depends on whether or not
some RUQ remain irreducible throughout the constraint solving procedure. ∎

###### Remark 7

$\mathcal{L}_{\mathcal{RQ}}$ has been designed by imposing some restrictions
on its fundamental elements, namely:
$\mathcal{V}_{\mathcal{S}}\cap\mathcal{V}_{\mathcal{X}}=\emptyset$ and
$\Pi_{\mathcal{S}}\cap\Pi_{\mathcal{X}}=\emptyset$. These restrictions are
used to prove Theorems 2-6. However, they can be relaxed to some extent as to
accept a wider class of theories as the parameter for
$\mathcal{L}_{\mathcal{RQ}}$.

It is possible to accept an $\mathcal{L}_{\mathcal{X}}$ such that
$\mathcal{V}_{\mathcal{S}}\cap\mathcal{V}_{\mathcal{X}}\neq\emptyset$ and
$\Pi_{\mathcal{S}}\cap\Pi_{\mathcal{X}}\neq\emptyset$ provided the solutions
returned by $SAT_{\mathcal{X}}$ are compatible with the irreducible form of
Definition 3.3. That is, if $SAT_{\mathcal{X}}$ returns, as part of its
solutions, a conjunction of constraints including set variables, this
conjunction must be satisfiable by substituting all set variables by the empty
set. This would be enough as to prove Theorem 2.

Along the same lines, if $\Pi_{\mathcal{X}}$ contains $\in$ then termination
of $SAT_{\mathcal{RQ}}$ might be compromised as $SAT_{\mathcal{X}}$ might
generate $\in$-constraints where the right term is the domain of a $foreach$
(much as when an $exists$ is after a $foreach$). This can be generalized to
any predicate symbol in $\Pi_{\mathcal{X}}$ that can bind values to set terms.
In this case Theorems 3-6 can be proved if $foreach$ domains are not affected
by the constraints generated by $SAT_{\mathcal{X}}$.

As we will shown in Section 6 there are expressive $\mathcal{L}_{\mathcal{X}}$
such that
$\mathcal{V}_{\mathcal{S}}\cap\mathcal{V}_{\mathcal{X}}\neq\emptyset$ and
$\Pi_{\mathcal{S}}\cap\Pi_{\mathcal{X}}\neq\emptyset$ for which
$SAT_{\mathcal{RQ}}$ is still an effective solver. ∎

##  5 Avoiding Existential Variables Inside RQ

All the considerations made in this section concerning RUQ apply equally to
REQ. The concepts introduced here are adapted from those developed by us for
RIS (DBLP:journals/jar/CristiaR21a, , Section 6).

Assume $R$ is a set of ordered pairs. We can try to write a formula stating
that $R$ is the identity relation:

$foreach(x\in R,x=(e,e))$ (33)

where $e$ is intended to be a variable existentially quantified inside the
RUQ. As defined in Section 2, $\mathcal{L}_{\mathcal{RQ}}$ does not allow to
introduce these variables and so (33) would not be one of its formulas.
Besides, it is not clear what a quantification domain could be for $e$.
However, the following is an $\mathcal{RQ}$-formula stating the same property:

$foreach((x,y)\in R,x=y)$

Note that we use an ordered pair as the control term (see Definition 4).
Precisely, allowing (nested) ordered pairs as control terms makes it possible
to avoid many existential variables inside RUQ. As binary relations are a
fundamental concept in Computer Science DBLP:journals/jar/Givant06 ;
DBLP:conf/RelMiCS/BerghammerHS14 , the introduction of ordered pairs as
control terms is sensible as it enables to quantify over binary relations,
without introducing existential variables.

Even if we allow (unrestricted) existential variables inside RQ, it is
important to avoid them because the negation of such a RQ would not be a
$\mathcal{L}_{\mathcal{RQ}}$ formula. Indeed, if there are existential
variables inside the RQ the negation will introduce a universally quantified
formula, which is not a $\mathcal{L}_{\mathcal{RQ}}$ formula. For instance,
assuming $R$ is a set of numeric ordered pairs, the following is a predicate
stating that the sum of any of its elements is greater than $z$:

$foreach((x,y)\in R,sum(x,y,n)\mathrel{\wedge}z<n)$ (34)

where $sum(x,y,n)$ is interpreted as $n=x+y$, and $n$ is intended to be a
variable existentially quantified inside the RUQ. Here, control terms do not
help and, again, we do not have a quantification domain for $n$. Then, the
negation of this formula would inevitably introduce a universal
quantification. Furthermore, it would negate $sum(x,y,n)$ for all $n$ which
would mean that there is no result for $x+y$.

Hence, the language is extended by introducing a $foreach$ constraint of arity
4:

$foreach(x\in
A,[e_{1},\dots,e_{n}],\phi(x,e_{1},\dots,e_{n}),\psi(x,e_{1},\dots,e_{n}))$
(35)

where $e_{1},\dots,e_{n}$ are variables implicitly existentially quantified
inside the RUQ and $\psi$ is a conjunction of so-called _functional
predicates_. A predicate $p$ of artity $n+1$ ($0<n$) is a functional predicate
iff for each $x_{1},\dots,x_{n}$ there exists exactly one $y$ such that
$p(x_{1},\dots,x_{n},y)$ holds; $y$ is called the _result_ of $p$. For
instance, $sum$ is a functional predicate. In an extended RUQ,
$e_{1},\dots,e_{n}$ must be the results of the functional predicates in
$\psi$.

The semantics of (35) is:

$\mathop{\mathstrut{\forall}}\nolimits x(x\in
A\Rightarrow(\mathop{\mathstrut{\exists}}\nolimits
e_{1},\dots,e_{n}(\psi(x,e_{1},\dots,e_{n})\mathrel{\wedge}\phi(x,e_{1},\dots,e_{n}))))$

whereas its negation is:

$\mathop{\mathstrut{\exists}}\nolimits x(x\in
A\mathrel{\wedge}(\mathop{\mathstrut{\exists}}\nolimits
e_{1},\dots,e_{n}(\psi(x,e_{1},\dots,e_{n})\mathrel{\wedge}\neg\;\phi(x,e_{1},\dots,e_{n}))))$

given the functional character of $\psi$ (DBLP:journals/jar/CristiaR21a, ,
Section 6.2). By means of functional predicates the introduction of
existential variables inside RUQ is harmless while the expressiveness of the
language is widened.

###### Example 6

Formula (34) should be written by means of an extended RUQ:

$foreach((x,y)\in R,[n],z<n,sum(x,y,n))$

Note that $n$ is the result of $sum$. The negation of the above formula is:

$exists((x,y)\in R,[n],z\geq n,sum(x,y,n))$

which is consistent with the intended meaning of the original formula. ∎

##  6 $\mathcal{L}_{\mathcal{RQ}}$ in Practice

$\mathcal{L}_{\mathcal{RQ}}$ and $SAT_{\mathcal{RQ}}$ have been implemented as
part of the $\\{log\\}$ (‘setlog’) tool setlog . $\\{log\\}$ is a constraint
logic programming (CLP) language implemented in Prolog. It also works as a
satisfiability solver (and thus as an automated theorem prover) for a few
theories rooted in the theory of finite sets. $\\{log\\}$ and the theories
underlying it have been thoroughly described elsewhere Dovier00 ;
DBLP:journals/tplp/CristiaRF15 ; DBLP:journals/jar/CristiaR20 ;
DBLP:journals/jar/CristiaR21a ; cristia_rossi_2021 ; zbMATH07552282 ;
DBLP:journals/corr/abs-2105-03005 . Empirical evidence of the practical
capabilities of $\\{log\\}$ has been provided as well CristiaRossiSEFM13 ;
DBLP:journals/jar/CristiaR21 ; DBLP:journals/jar/CristiaR21b ;
10.1093/comjnl/bxab030 ; DBLP:journals/corr/abs-2112-15147 .

Theory $\mathcal{X}$ in $\\{log\\}$ is the combination between the theories
known as $\mathcal{LIA}$ and $\mathcal{BR}$. $\mathcal{LIA}$ stands for
_linear integer arithmetic_ and implements a decision procedure for systems of
linear equations and disequations over the integer numbers. $\mathcal{BR}$
stands for _binary relations_ and implements a decision procedure for an
expressive fragment of finite set relation algebra (RA)
DBLP:journals/jar/CristiaR20 . In $\mathcal{BR}$, binary relations are sets of
ordered pairs and all the RA operators are available as constraints, namely:
union ($C=A\cup B\rightarrow$ `un(A,B,C)`), intersection ($C=A\cap
B\rightarrow$ `inters(A,B,C)`), identity relation over a set
($\mathop{\mathrm{id}}(A)=R\rightarrow$`id(A,R)`), converse of a binary
relation ($R^{\smile}=S\rightarrow$ `inv(R,S)`) and composition ($T=R\circ
S\rightarrow$ `comp(R,S,T)`). These operators can be combined in
$\mathcal{BR}$-formulas to define many other operators such as: domain
($\mathop{\mathrm{dom}}R=A\rightarrow$ `dom(R,A)`) and range
($\mathop{\mathrm{ran}}R=A\rightarrow$ `ran(R,A)`) of a binary relation, a
predicate constraining a binary relation to be a function (`pfun(R)`),
function application ($F(X)=Y\rightarrow$ `applyTo(F,X,Y)`), etc.

$\mathcal{LIA}$ satisfies all the restrictions discussed in Remark 7, but
$\mathcal{BR}$ does not. However, the solutions returned by $\\{log\\}$ when
solving $\mathcal{BR}$-formulas are compatible with the irreducible form of
Definition 10 (DBLP:journals/jar/CristiaR20, , Definition 15 and Theorem 3).
That is, irreducible formulas in $\mathcal{BR}$ are satisfied by substituting
all the set and relational variables by the empty set. However, when a
$\mathcal{BR}$-formula is processed, RQ domains may be affected. As discussed
in Remark 7 this may compromise termination;
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ decidability is
discussed more deeply in Section 7. Nevertheless, as the following case
studies show, $\\{log\\}$ is still an effective and efficient tool to
automatically reason about
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ formulas. Termination
do not seem to be an issue for many classes of practical problems expressible
in $\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$.

$\\{log\\}$’s concrete syntax is a slight variation of the syntax used in this
paper: $\\{\leavevmode\vbox{\hrule
width=5.0pt}\mathbin{\scriptstyle\sqcup}\leavevmode\vbox{\hrule
width=5.0pt}\\}$ is `{_/_}`; $(\leavevmode\vbox{\hrule
width=5.0pt},\leavevmode\vbox{\hrule width=5.0pt})$ is `[_,_]`; $\in$ is `in`;
$\mathrel{\wedge}$ is `&`; $A\subseteq B$ is `subset(A,B)`; variables begin
with a capital letter.

The following simple example shows $\\{log\\}$ syntax and how to use it to
prove invariance lemmas.

###### Example 7

Let `Usr` and `Admin` be the sets of users and administrators of some system.
Let us say that the security policy requires these sets to be disjoint. We can
express that in $\\{log\\}$ as follows555Other encodings are possible; we
deliberately choose to use a RUQ.:

    inv(Usr,Adm) :- foreach([U in Usr,A in Adm], U neq A).

We can model the operation adding user `X` to `Usr` yielding `Usr_` as the new
set:

    addUsr(Usr,Adm,X,Usr_,Adm_) :- Usr_ = {X / Usr} & Adm_ = Adm.

We would like to know if `addUsr` preserves `inv`, so we run the following
query666Given that $\\{log\\}$ is a satisfiability solver we call it on the
negation of the lemma waiting for a no (i.e., $false$) answer.:

    neg(inv(Usr,Adm) & addUsr(Usr,Adm,X,Usr_,Adm_) implies inv(Usr_,Adm_)).

As `addUsr` fails to preserve `inv`, $\\{log\\}$ provides a counterexample
(`N` new variable):

    Admin = {X / N}, Usr_ = {X / Usr}, Admin_ = {X / N}

So we can fix `addUsr` by adding a pre-condition:

    addUsr(Usr,Adm,X,Usr_,Adm_) :- X nin Usr & Usr_ = {X / Usr} & Adm_ = Adm.

Now the answer to the query is `no` meaning that the formula is unsatisfiable.
∎

The next three subsections present real-world case studies where $\\{log\\}$
is used as a CLP language and as an automated verifier. The focus in on how RQ
are used.

###  6.1 The Landing Gear System

In the fourth edition of the ABZ Conference held in Toulouse (France) in 2014,
Boniol and Wiels proposed a real-life, industrial-strength case study, known
as the Landing Gear System (LGS) DBLP:conf/asm/BoniolW14 . Mammar and Laleau
DBLP:conf/asm/MammarL14  developed an Event-B Abrial:2010:MES:1855020
specification of the LGS, formally verified using Rodin
DBLP:journals/sttt/AbrialBHHMV10 , ProB Leuschel00  and
AnimB777http://www.animb.org. Basically, we encoded in $\\{log\\}$ the Event-B
specification and used $\\{log\\}$ to automatically discharge all the proof
obligations generated by Rodin. This work is thoroughly described elsewhere
DBLP:journals/corr/abs-2112-15147 888$\\{log\\}$ code of the LGS:
http://www.clpset.unipr.it/SETLOG/APPLICATIONS/lgs.zip..

This is the simplest model in terms of RQ as it does not require nested RQ. A
typical use of RQ in the LGS is the following999Some variable names are
changed to save some space.:

    ta_inv5(Positions,DULDC) :-
      pfun(DULDC) &
      dompf(DULDC,Positions) &
      foreach([X,Y] in DULDC, 0 =< Y).

That is, `ta_inv5` defines a state invariant corresponding to the Event-B
machine named TimedAspects. In mathematical notation the invariant states
$DULDC\in Positions\mathrel{\ooalign{\hfil$\mapstochar\mkern
5.0mu$\hfil\cr$\rightarrow$}}{\bbold N}$. As in $\\{log\\}$ we cannot express
${\bbold N}$ we use a RUQ to ascertain that the second component of each
element in $DULDC$ is non-negative. Then, invariance lemmas such as:

    neg(di_inv1(Positions,Dcp) &
        ta_inv1(CT) &
        ta_inv5(Positions,DULDC) &
        ta_make_DoorClosed(...,Dcp,...,CT,...,DULDC,...,Dcp_,...,DULDC_)
        implies   ta_inv5(Positions,DULDC_)).

are automatically discharged by $\\{log\\}$. `di_inv1(Positions,Dcp)` and
`ta_inv1(CT)` are other invariants that are needed as hypothesis and
`ta_make_DoorClosed` is one of the state transitions of the LGS model
(ellipses stand for variables). Hence, `ta_make_DoorClosed` changes the value
of `DULDC` during the state transition and so we need to check that `ta_inv5`
is still valid in the new state.

$\\{log\\}$ discharges all the 465 proof obligations in less than 5 minutes.

###  6.2 The Bell-LaPadula Security Model

Around 1973 D.E. Bell and L. LaPadula published the first formal model of a
secure operating system BLP1 ; BLP2 . Today this model is known as the Bell-
LaPadula model, abbreviated as BLP. BLP is described as a state machine by
means of first-order logic and set theory. The model also formalizes two state
invariants known as _security condition_ and _*-property_. We encoded BLP and
its properties in $\\{log\\}$ and used it to automatically discharge all the
invariance lemmas. This work is presented with detail elsewhere
DBLP:journals/jar/CristiaR21 101010$\\{log\\}$ code of BLP:
http://www.clpset.unipr.it/SETLOG/APPLICATIONS/blp2.zip..

The following is the $\\{log\\}$ encoding of the *-property:

    starProp(State) :-
      State = [[br,Br],[bw,Bw],[fo,Fo],[fs,Fs],[m,M]] &
      foreach([[S1,O1] in Br, [S2,O2] in Bw], [Sco1,Sco2],
        S1 = S2 implies dominates(Sco1,Sco2),
        applyTo(Fo,O1,Sco1) & applyTo(Fo,O2,Sco2)).

As can be seen it requires the use of the extended version of nested RUQ
(Section 5). That is, it declares two existential variables inside the RUQ
(`Sco1` and `Sco2`) and uses the functional predicate section
(`applyTo(Fo,O1,Sco1) & ...`). Extended RUQ are also used in the state
transitions, for instance:

    getRead(State,S,O,State_) :-
      State = [[br,Br],[bw,Bw],[fo,Fo],[fs,Fs],[m,M]] &
      [O,[S,read]] in M & [S,O] nin Br &
      applyTo(Fo,O,Sco) & applyTo(Fs,S,Scs) &
      dominates(Sco,Scs) &
      foreach([Si,Oi] in Bw,[Scoi],
        Si = S implies dominates(Sco,Scoi),applyTo(Fo,Oi,Scoi)) &
      Br_ = {[S,O]/Br} &
      State_ = [[br,Br_],[bw,Bw],[fo,Fo],[fs,Fs],[m,M]].

`getRead` grants `read` permission to subject `S` on object `O` in which case
changes the value of variable `Br`. Then, the following invariance lemma must
be proved:

    neg(starProp(State) & getRead(State,S,O,State_) implies starProp(State_)).

Due to an optimization introduced since our first experiments with BLP, now
$\\{log\\}$ proves all the 60 invariance lemmas in less than 2 seconds instead
of the 11.5 seconds reported previously DBLP:journals/jar/CristiaR21 .

###  6.3 Android’s Permission System

In a series of articles a group of Uruguayan and Argentinian researchers and
students developed a certified Coq model and implementation of Android’s
permission system DBLP:conf/ictac/BetarteCLR15 ;
DBLP:journals/cuza/BetarteCLR16 ; DBLP:journals/cleiej/LunaBCSCG18 ;
DBLP:conf/types/Luca020 . They model the system as a state machine, then
propose a number of properties and use Coq to verify them against the model.
Properties are classified in two classes: valid state properties and security
properties. The first class ensures the state machine preserves some well-
formedness properties of the state variables, while the second ensures Android
behaves as expected in some security-related scenarios. As with the previous
case studies, we translated the Coq model into $\\{log\\}$ and used it to
automatically prove properties111111$\\{log\\}$ code of Android 10’s
permission system: http://www.clpset.unipr.it/SETLOG/APPLICATIONS/android.zip.

This is the most challenging case study we have developed so far. It takes
$\\{log\\}$ to its limits concerning reasonable computing times to discharge
proof obligations121212Actually, $\\{log\\}$ is unable to prove only three of
the properties proposed in the Coq model.. It also uses the most complex
nested RQ we have used so far, as the following one which formalizes one of
the valid state properties131313In the following formulas some simplifications
are introduced to save some space..

    notDupPerm(DP) :-
      foreach([[A1,SP1] in DP, [A2,SP2] in DP],
        foreach([P1 in SP1, P2 in SP2],[IP1,IP2],
          IP1 = IP2 implies P1 = P2 & A1 = A2,
          idP(P1,IP1) & idP(P2,IP2))).

Note that there is one nested RUQ whose filter is an extended nested RUQ.
Furthermore, in the innermost RUQ `SP1` and `SP2` are domains whereas they are
part of the outermost control term. That is, first `[A1,SP1]` quantifies over
`DP` and then `P1` quantifies over `SP1`.

The following is another state consistency property fitting in the
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
subclass.

    permsDom(PR,Apps,SS) :-
      foreach([A,P] in PR,
        A in Apps or exists(SI in SS, [IA], IA = A, idSI(SI,IA))).

As can be seen, the domain of the RUQ does not appear inside the REQ, thus
making the formula free of
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops. The REQ uses a functional predicate.

$\\{log\\}$ automatically discharges 801 proof obligations in around 22
minutes.

##  7 Discussion and Related Work

The problem of deciding the satisfiability of quantified formulas is obviously
undecidable. Hence, we can only hope to find expressive fragments that are
decidable. A possible path for this is to restrict the form of the quantifiers
and another is to allow only certain quantifier-free formulas. A class of
quantified formulas that has been studied for many years is that of restricted
quantifiers. However, the full fragment of restricted quantifiers as well as
some of its sub-fragments are undecidable (e.g.
https://doi.org/10.1002/cpa.3160340203 ;
https://doi.org/10.1002/cpa.3160460104 ; DBLP:journals/lmcs/FeldmanPISS19 ).
Hence, further restrictions must be imposed. One of such restrictions is to
deal with formulas where RUQ are after REQ. This fragment has been proved to
be decidable in different contexts https://doi.org/10.1002/cpa.3160340203 ;
DBLP:journals/jsyml/OmodeoP12 ; DBLP:journals/lmcs/FeldmanPISS19 . We started
by working with quantifier-free formulas that do not affect quantification
domains (Definition 1, Remark 7). We have not seen other works taking this
path. Then, we relaxed that restriction loosing termination but nonetheless
gaining expressiveness. This combination seems to be useful in practice
(Section 6).

We identify Computable Set Theory (CST) 10.5555/92143 ;
DBLP:series/mcs/CantoneOP01  as the main and closest source of works related
to the one presented in this paper. However, there are works outside CST
dealing with similar problems, specially in the realm of STM solvers. We start
with the latter.

The STM solving community deals with unrestricted quantifiers. The usual
practical technique employed in SMT solvers to deal with quantified formulas
is heuristics-based quantifier instantiation Flanagan2003 ; Dutertre01 ;
Moura2007 ; Ge2009 . In particular, Simplify’s E-matching algorithm
Detlefs2005  is used by some of these tools. Heuristic instantiation manages
to solve problems of software verification. However, it suffers from some
shortcomings as stated by Ge and de Moura DBLP:conf/cav/GeM09 . For this
reason, Ge and de Moura propose some decidable fragments of first order logic
modulo theories. The proposed decision procedures can solve complex quantified
array properties. The authors show how to construct models for satisfiable
quantified formulas in these fragments.

In a more recent work, Feldman et al. DBLP:journals/lmcs/FeldmanPISS19  study
the problem of discharging inductive invariants with quantifier alternation
using SMT solvers. They depart from formulas belonging to the Effectively
Propositional logic (EPR), also known as the Bernays-Schönfinkel-Ramsey class.
In this logic, formulas are of the form
$\mathop{\mathstrut{\exists}}\nolimits^{*}\mathop{\mathstrut{\forall}}\nolimits^{*}(\delta)$,
where $\delta$ is a quantifier-free formula over some first-order vocabulary.
This logic has been proved to be decidable and useful in automatically
discharging verification conditions of software involving linked-lists,
distributed protocols, etc. Feldman and his colleagues then go to extend EPR
with formulas of the form
$\mathop{\mathstrut{\forall}}\nolimits^{*}\mathop{\mathstrut{\exists}}\nolimits^{*}(\delta)$.
The first conclusion they get is that this fragment is undecidable. However, a
second conclusion is that some techniques can be put to work as to solve many
interesting problems in that fragment. The main technique is instantiations
that are bounded in the depth of terms. However, bounded instantiations
guarantee termination a-priori even when the invariant is not correct. In
these cases the algorithm returns an approximated counterexample. The
invariants approached by Feldman at al. are of the same form of most of the
proof obligations present in our case studies.

As can bee seen, the SMT solving community approaches the problem of finding
decision procedures for quantified fragments of logic languages in a quite
different way as we do. They do not use RQ nor a theory of sets. RQ have an
interesting property: $\mathop{\mathstrut{\forall}}\nolimits x\in A:\phi$,
with $A$ a variable, is satisfied with $A=\emptyset$. If this is combined with
a set constructor such as $\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$, it
is possible to iterate over the elements of the quantification domain until
the ‘end’ is reached: if it is $\emptyset$, then the quantifier can be
eliminated; it if is a variable, then the iteration can be stopped because we
know that we have a good candidate solution for the quantification domain.
Quantification domains are crucial to find out a decision procedure for
formulas where REQ are after RUQ. As we have shown in Theorem 6, REQ with the
same domain variable than a preceding RUQ, in general, generate infinite
feedback loops. These loops can be easily detected by following the flow of
hypothesized elements through quantification domains. We believe all this is
harder to see when the language admits general quantifiers and is not based on
a theory of sets. At the same time, RQ do not pose a threat on expressiveness
when it comes to software verification. Finally, concerning counterexample
generation, within the decidable fragments presented in this paper,
$\\{log\\}$ is not only always able to generate a counterexample of any given
satisfiable formula but it (interactively) generates a finite representation
of all its solutions (Theorem 1).

Our work is closer to CST. CST has been looking for decidability results on
quantified fragments of set theory since at least forty years ago. In many
cases, CST is interested in proving decidability results (in the form of
satisfiability tests) but not so much in providing efficient algorithms or in
implementing them in some software tool. Brevan et al
https://doi.org/10.1002/cpa.3160340203  present a semi-decision algorithm for
a wide class of quantified formulas where the quantifier-free theory is
decidable. In this work, quantifiers are RQ but no quantified variable can be
a quantified domain of a deeper RQ (see ($\dagger$) below). For some theories
the algorithm becomes complete. In general, the quantifier-free theories are
sub-languages of set theory. In particular they consider a language based on
$\\{=,\in\\}$. The resulting quantified language allows to express many set-
theoretic operators (e.g. union). From that article, several researchers of
the CST community have found a number of (un)decidability results about
different fragments of quantified languages of set theory
DBLP:journals/mlq/ParlamentoP92 ; https://doi.org/10.1002/cpa.3160460104 ;
DBLP:journals/mlq/OmodeoPP96 ; DBLP:journals/jsyml/BelleP06 ;
DBLP:journals/jsyml/OmodeoP12 .

As can be seen, the decidability results represented by Theorems 1-5 have
already been proved. On the contrary, we believe the result of Theorem 6 is
new. Besides, as far as we understand, all of our results are new in terms of
the algorithm we use and in particular the set of rewrite rules we use, not to
mention the fact that we put these results to work in a software tool that is
able to solve real-world problems (Section 6).

More recently, Cantone and Longo DBLP:journals/tcs/CantoneL14 ; Cantone2011
worked on the language $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$,
part of Cantone’s long work on CST.
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ helps to analyze the
decidability and expressiveness of
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$141414The same could
be achieved by using as a reference the work on CST by Breban et al.
https://doi.org/10.1002/cpa.3160340203 . We opted by Cantone’s because is
newer. Nonetheless, Breban’s is also duly referenced..
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ is a two-sorted quantified
fragment of set theory allowing the following literals: $x\in y$, $(x,y)\in
R$, $x=y$ and $R=S$, where $x$ and $y$ are set variables and $R$ and $S$ are
variables ranging over binary relations. Note that in
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ sets are _pure_ meaning
that their elements are sets where the empty set is the base element
(semantics of $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ is given in
terms of the von Neumann standard cumulative hierarchy of sets). Formulas in
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ are Boolean combinations
of expressions of the following two forms:
$\mathop{\mathstrut{\forall}}\nolimits x_{1}\in
z_{1}:\dots\mathop{\mathstrut{\forall}}\nolimits x_{h}\in
z_{h}:\mathop{\mathstrut{\forall}}\nolimits(x_{h+1},y_{h+1})\in
R_{h+1}:\dots\mathop{\mathstrut{\forall}}\nolimits(x_{n},y_{n})\in
R_{n}:\delta$, and the same expression where
$\mathop{\mathstrut{\forall}}\nolimits$ is replaced by
$\mathop{\mathstrut{\exists}}\nolimits$. In these expressions: $\delta$ is a
propositional combination of
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$-literals;
$x_{i},y_{i},z_{i}$ are set variables; $R_{i}$ are binary relation variables;
and ($\dagger$) no $x_{i}$ or $y_{i}$ can also occur as a $z_{j}$ (i.e., no
quantified variable can occur also as a domain variable in the same quantifier
prefix). Note that in $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ RUQ
and REQ cannot be mixed in the same expression.

$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ is a decidable language
which allows to express all the operators of RA with the exception of
composition. Indeed, $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ only
allows to express $R\circ S\subseteq T$ but the other inclusion cannot be
written. The impossibility to express the other inclusion comes from the fact
that RUQ and REQ cannot be mixed in the same expression, which is tantamount
to preserve decidability of
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$. In effect, $T\subseteq
R\circ S$ is equivalent to:

$\mathop{\mathstrut{\forall}}\nolimits(x,z)\in
T:(\mathop{\mathstrut{\exists}}\nolimits(x_{1},y_{1})\in
R:(\mathop{\mathstrut{\exists}}\nolimits(y_{2},z_{1})\in
S:x_{1}=x\mathrel{\wedge}y_{1}=y_{2}\mathrel{\wedge}z_{1}=z))$ (36)

which is not a $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ formula (as
it mixes RUQ and REQ).

Now we analyze the decidability and expressiveness of
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ in terms of
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$:

  1. 1.

$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ sets are not necessarily
finite; $\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ sets are
finite. However, since we are interested in software verification this is not
a real restriction.

  2. 2.

$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ is not a parametric
language as $\mathcal{L}_{\mathcal{RQ}}$, although other works on CST provide
parametric languages in the line of
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$
https://doi.org/10.1002/cpa.3160340203 . Parametrization of
$\mathcal{L}_{\mathcal{RQ}}$ enables hybrid sets.

  3. 3.

$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ sets are pure, while
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ sets are hybrid. Pure
sets allow to encode ordered pairs, natural numbers, etc. However, these
encodings tend to reduce the efficiency of solvers. Working directly with
hybrid sets facilitates the integration with efficient solvers for other
theories, such as $\mathcal{LIA}$. For instance, the formula in Example 1
encodes the minimum of a set which would require a complex
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ formula.

  4. 4.

$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ extends the
decidability result of $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$. On
one hand, $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ almost expresses
RA so if in $\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$
composition is used as in $\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$,
the former is a fragment of the latter in what concerns to RA. On the other
hand, $\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ allows to fully
express composition by a suitable encoding of formula (36):

$foreach((x,z)\in T,exists([(x_{1},y_{1})\in R,(x_{2},z_{1})\in
S],x_{1}=x\mathrel{\wedge}y_{1}=y_{2}\mathrel{\wedge}z_{1}=z))$

As can be seen, this formula is free of
$\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits$
loops as long as the variable of $T$ is different from the variables of $R$
and $S$. Hence, Cantone and Longo go to far in restricting
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ as the real problem with
composition comes with formulas such as $R\subseteq R\circ S$ or $S\subseteq
R\circ S$. This is aligned with our results concerning the decidability of
$\mathcal{L}_{\mathcal{BR}}$ (DBLP:journals/jar/CristiaR20, , Section 5.3,
Definition 16). Finding larger decidable fragments of RA is important as it is
a fundamental theory in Computer Science due to its expressiveness
(DBLP:journals/jar/Givant06, , last paragraph Section 1). Besides, as shown in
Section 6.3 with formula `permsDom`, allowing
$\Phi_{\mathop{\mathstrut{\forall}}\nolimits\mathop{\mathstrut{\exists}}\nolimits}$
formulas is useful in practice.

  5. 5.

$\mathcal{L}_{\mathcal{RQ}}(\mathcal{LIA}+\mathcal{BR})$ allows quantified
variables to occur as domains in the same quantifier prefix (cf. ($\dagger$)
above). Recall, for instance, formula `notDupPerm` in Section 6.3. These
formulas are ruled out from
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ because they compromise
completeness, not soundness (https://doi.org/10.1002/cpa.3160340203, ,
Sections 2 and 4). The problem is that there are formulas not adhering to
($\dagger$) that are satisfied only by infinite sets when $\in$ is part of the
quantifier-free theory parlamentoPolicriti . So if we allow these formulas in
$\\{log\\}$ its answers are correct because the tool is still sound, although
it will not terminate for those formulas that are satisfied only by infinite
sets. As shown in Section 6.3, allowing formulas not adhering to ($\dagger$)
is useful in practical cases.

  6. 6.

$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ is proved to be decidable
by encoding each of its formulas as a
$\mathop{\mathstrut{\forall}}\nolimits_{0}^{\pi}$-formula. In turn,
$\mathop{\mathstrut{\forall}}\nolimits_{0}^{\pi}$ is shown to be decidable by
means of the notions of skeletal representation and of its realization
Cantone2011 . The authors do not provide an algorithm with an obvious
operative semantics for the decidability problem of
$\mathop{\mathstrut{\forall}}\nolimits_{0,2}^{\pi}$ formulas. Conversely, by
adapting our results on RIS, we provide a simple and concrete solver for
$\mathcal{L}_{\mathcal{RQ}}$ (i.e., $SAT_{\mathcal{RQ}}$) with CLP properties
easily implementable as part of $\\{log\\}$. In turn, we provide empirical
evidence of its practical capabilities. The algorithms presented by Breban
https://doi.org/10.1002/cpa.3160340203  are closer to $SAT_{\mathcal{RQ}}$.

##  8 Final Remarks

We have presented a decision procedure for quantifier-free, decidable
languages extended with restricted quantifiers. The decision procedure is
based on a small collection of rewrite rules for primitive set-theoretic
operators ($\subseteq,\in,=$). Although all but one of the decidability
results underlying our decision procedure are not new, as far as we
understand, the decision procedure and its rewrite rules are novel. The new
decidability result concerns quantified formulas where a restricted
existential quantifier comes after a restricted universal quantifier. The
result is based on building a graph linking the universally quantified domains
with those existentially quantified. Then, a path analysis is performed to
find out whether or not there is a path from a universally quantified domain
to the same domain but making part of an existential quantifier. Finally, the
implementation of the decision procedure as part of a software tool
($\\{log\\}$) and its successful application to real-world, industrial-
strength case studies as an automated software verifier provide empirical
evidence of the usefulness of the approach.

Our strongest decidability results are possible by imposing some restrictions
on the quantifier-free language—namely, that it does not include terms
denoting sets. Although non-trivial languages fulfill these restrictions
(e.g., linear integer arithmetic), the greatest expressiveness is reached when
some of these restrictions are lifted at the expense of termination. Hence, as
a future work we plan to study what quantifier-free languages preserve
termination even though they support sets to some extent. In particular, the
long and fruitful work on CST should help us in finding those languages.

## References

  * (1) Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edn. (2010)
  * (2) Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010), https://doi.org/10.1007/s10009-010-0145-y
  * (3) Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical foundations. MTR 2547, The MITRE Corporation (May 1973)
  * (4) Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical model. ESD-TR 73-278, The MITRE Corporation (Nov 1973)
  * (5) Bellè, D., Parlamento, F.: Truth in V for $\mathop{\mathstrut{\exists}}\nolimits$${}^{\mbox{*}}$$\mathop{\mathstrut{\forall}}\nolimits$$\mathop{\mathstrut{\forall}}\nolimits$-sentences is decidable. J. Symb. Log. 71(4), 1200–1222 (2006), https://doi.org/10.2178/jsl/1164060452
  * (6) Berghammer, R., Höfner, P., Stucke, I.: Automated verification of relational while-programs. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds.) Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28-May 1, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8428, pp. 173–190. Springer (2014), http://dx.doi.org/10.1007/978-3-319-06251-8\\_11
  * (7) Betarte, G., Campo, J.D., Luna, C., Romano, A.: Formal analysis of Android’s permission-based security model,. Sci. Ann. Comp. Sci. 26(1), 27–68 (2016), https://doi.org/10.7561/SACS.2016.1.27
  * (8) Betarte, G., Campo, J.D., Luna, C.D., Romano, A.: Verifying Android’s permission model. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9399, pp. 485–504. Springer (2015), https://doi.org/10.1007/978-3-319-25150-9\\_28
  * (9) Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K. (eds.) ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Toulouse, France, June 2-6, 2014. Proceedings. Communications in Computer and Information Science, vol. 433, pp. 1–18. Springer (2014), https://doi.org/10.1007/978-3-319-07512-9\\_1
  * (10) Breban, M., Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Communications on Pure and Applied Mathematics 34(2), 177–195 (1981), https://onlinelibrary.wiley.com/doi/abs/10.1002/cpa.3160340203
  * (11) Cantone, D., Ferro, A., Omodeo, E.: Computable Set Theory. Clarendon Press, USA (1989)
  * (12) Cantone, D., Longo, C.: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions. Theor. Comput. Sci. 560, 307–325 (2014), http://dx.doi.org/10.1016/j.tcs.2014.03.021
  * (13) Cantone, D., Longo, C., Asmundo, M.N.: A decidable quantified fragment of set theory involving ordered pairs with applications to description logics. In: Bezem, M. (ed.) Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings. LIPIcs, vol. 12, pp. 129–143. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
  * (14) Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing - From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science, Springer (2001), http://dx.doi.org/10.1007/978-1-4757-3452-2
  * (15) Cristiá, M., Katz, R.D., Rossi, G.: Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra. The Computer Journal (05 2021), https://doi.org/10.1093/comjnl/bxab030, bxab030
  * (16) Cristiá, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295–330 (2020), https://doi.org/10.1007/s10817-019-09520-4
  * (17) Cristiá, M., Rossi, G.: Automated proof of Bell-LaPadula security properties. J. Autom. Reason. 65(4), 463–478 (2021), https://doi.org/10.1007/s10817-020-09577-6
  * (18) Cristiá, M., Rossi, G.: Automated reasoning with restricted intensional sets. J. Autom. Reason. 65(6), 809–890 (2021), https://doi.org/10.1007/s10817-021-09589-w
  * (19) Cristiá, M., Rossi, G.: An automatically verified prototype of a landing gear system. CoRR abs/2112.15147 (2021), https://arxiv.org/abs/2112.15147
  * (20) Cristiá, M., Rossi, G.: An automatically verified prototype of the Tokeneer ID station specification. J. Autom. Reason. 65(8), 1125–1151 (2021), https://doi.org/10.1007/s10817-021-09602-2
  * (21) Cristiá, M., Rossi, G.: A decision procedure for a theory of finite sets with finite integer intervals. CoRR abs/2105.03005 (2021), https://arxiv.org/abs/2105.03005, under consideration in Theoretical Computer Science
  * (22) Cristiá, M., Rossi, G.: Integrating cardinality constraints into constraint logic programming with sets. Theory and Practice of Logic Programming pp. 1–33 (2021), https://doi.org/10.1017/S1471068421000521
  * (23) Cristiá, M., Rossi, G.: $\\{\mathit{log}\\}$: set formulas as programs. Rend. Ist. Mat. Univ. Trieste 53, 24 (2021), id/No 23
  * (24) Cristiá, M., Rossi, G., Frydman, C.S.: $\\{log\\}$ as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229–243. Springer (2013)
  * (25) Cristiá, M., Rossi, G., Frydman, C.S.: Adding partial functions to constraint logic programming with sets. Theory Pract. Log. Program. 15(4-5), 651–665 (2015), https://doi.org/10.1017/S1471068415000290
  * (26) De Luca, G., Luna, C.: Towards a certified reference monitor of the Android 10 permission system. In: de’Liguoro, U., Berardi, S., Altenkirch, T. (eds.) 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy. LIPIcs, vol. 188, pp. 3:1–3:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020), https://doi.org/10.4230/LIPIcs.TYPES.2020.3
  * (27) Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking 52(3), 365–473
  * (28) Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000)
  * (29) Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645–701 (2006)
  * (30) Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV. Lecture Notes in Computer Science, vol. 4144, pp. 81–94. Springer (2006)
  * (31) Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. Log. Methods Comput. Sci. 15(3) (2019), https://doi.org/10.23638/LMCS-15(3:18)2019
  * (32) Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Jr., W.A.H., Somenzi, F. (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2725, pp. 355–367. Springer, https://doi.org/10.1007/978-3-540-45069-6_34
  * (33) Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories 55(1-2), 101–122
  * (34) Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 306–320. Springer (2009), http://dx.doi.org/10.1007/978-3-642-02658-4_25
  * (35) Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reasoning 37(4), 277–322 (2006), http://dx.doi.org/10.1007/s10817-006-9062-x
  * (36) Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http://research.microsoft.com/users/lamport/tla/book.html
  * (37) Leuschel, M., Butler, M.: ProB: A model checker for B. In: Keijiro, A., Gnesi, S., Mandrioli, D. (eds.) FME. Lecture Notes in Computer Science, vol. 2805, pp. 855–874. Springer-Verlag (2003)
  * (38) Luna, C., Betarte, G., Campo, J.D., Sanz, C., Cristiá, M., Gorostiaga, F.: A formal approach for the verification of the permission-based security model of Android. CLEI Electron. J. 21(2) (2018), https://doi.org/10.19153/cleiej.21.2.3
  * (39) Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K. (eds.) ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Toulouse, France, June 2-6, 2014. Proceedings. Communications in Computer and Information Science, vol. 433, pp. 80–94. Springer (2014), https://doi.org/10.1007/978-3-319-07512-9\\_6
  * (40) de Moura, L.M., Bjørner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4603, pp. 183–198. Springer, https://doi.org/10.1007/978-3-540-73595-3_13
  * (41) Omodeo, E.G., Parlamento, F., Policriti, A.: Decidability of $\mathop{\mathstrut{\exists}}\nolimits$${}^{\mbox{*}}$$\mathop{\mathstrut{\forall}}\nolimits$-sentences in membership theories. Math. Log. Q. 42, 41–58 (1996), https://doi.org/10.1002/malq.19960420105
  * (42) Omodeo, E.G., Policriti, A.: The Bernays - Schönfinkel - Ramsey class for set theory: decidability. J. Symb. Log. 77(3), 896–918 (2012), https://doi.org/10.2178/jsl/1344862166
  * (43) Parlamento, F., Policriti, A.: Undecidability results for restricted universally quantified formulae of set theory. Communications on Pure and Applied Mathematics 46(1), 57–73 (1993), https://onlinelibrary.wiley.com/doi/abs/10.1002/cpa.3160460104
  * (44) Parlamento, F., Policriti, A.: The logically simplest form of the infinity axiom 103(1), 274–276
  * (45) Parlamento, F., Policriti, A.: The decision problem for restricted universal quantification in set theory and the axiom of foundation. Math. Log. Q. 38(1), 143–156 (1992), https://doi.org/10.1002/malq.19920380110
  * (46) Rossi, G.: $\\{log\\}$. http://www.clpset.unipr.it/setlog.Home.html (2008), last access 2022
  * (47) Schneider, S.: The B-method: An Introduction. Cornerstones of computing, Palgrave (2001), http://books.google.com.ar/books?id=Krs0OQAACAAJ
  * (48) Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1996)

##  Appendix A Proofs

In the following, a set of the form $\\{P(x):F(x)\\}$ (where pattern and
filter are separated by a colon ($:$), instead of a bar ($|$), and the pattern
is _before_ the colon) is a shorthand for
$\\{y:\mathop{\mathstrut{\exists}}\nolimits x(P(x)=y\mathrel{\wedge}F(x))\\}$.
That is, the set is written in the classic notation for intensional sets used
in mathematics.

###### Proposition 1

$\displaystyle\begin{split}\mathop{\mathstrut{\forall}}\nolimits d,&D:\\\
&\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}|\phi\mathbin{\bullet}u\\}=\\{u(d):\phi(d)\\}\cup\\{u(x):x\in
D\mathrel{\wedge}\phi(x)\\}\end{split}$

###### Proof

Taking any $d$ and $D$ we have:

$\displaystyle\\{x:\\{d\mathbin{\scriptstyle\sqcup}D\\}|\phi\mathbin{\bullet}u\\}$
$\displaystyle=\\{u(x):x\in\\{d\mathbin{\scriptstyle\sqcup}D\\}\mathrel{\wedge}\phi(x)\\}$
$\displaystyle=\\{u(x):(x=d\mathrel{\vee}x\in D)\mathrel{\wedge}\phi(x)\\}$
$\displaystyle=\\{u(x):(x=d\mathrel{\wedge}\phi(x))\mathrel{\vee}(x\in
D\mathrel{\wedge}\phi(x))\\}$
$\displaystyle=\\{u(x):x=d\mathrel{\wedge}\phi(x)\\}\cup\\{u(x):x\in
D\mathrel{\wedge}\phi(x)\\}$ $\displaystyle=\\{u(d):\phi(d)\\}\cup\\{u(x):x\in
D\mathrel{\wedge}\phi(x)\\}$

∎

######  Lemma 2 (Equivalence of rule (10))

$\displaystyle\mathop{\mathstrut{\forall}}\nolimits t,A:t\notin A\Rightarrow$
$\displaystyle\quad\\{t\sqcup A\\}\cup\\{x:\\{t\sqcup
A\\}|\phi\\}=\\{x:\\{t\sqcup
A\\}|\phi\\}\Leftrightarrow\phi(t)\mathrel{\wedge}A\cup\\{x:A|\phi\\}=\\{x:A|\phi\\}$

###### Proof

First note that

$t\notin A\Rightarrow\\{t\\}\parallel
A\mathrel{\wedge}\\{t\\}\parallel\\{A|\phi\\}$ (37)

and

$\\{x:\\{t\\}|\phi\\}\subseteq\\{t\\}$ (38)

and

$\\{x:\\{t\\}|\phi\\}=\\{t\\}\Leftrightarrow\phi(t)$ (39)

$\displaystyle\\{t\sqcup A\\}\cup\\{x:\\{t\sqcup A\\}|\phi\\}=\\{x:\\{t\sqcup
A\\}|\phi\\}$ $\displaystyle\Leftrightarrow\\{t\\}\cup
A\cup\\{x:\\{t\\}|\phi\\}\cup\\{x:A|\phi\\}=\\{x:\\{t\\}|\phi\\}\cup\\{x:A|\phi\\}$
[by Prop. 1; semantics $\mathbin{\scriptstyle\sqcup}$]
$\displaystyle\Leftrightarrow\\{t\\}\cup
A\cup\\{x:A|\phi\\}=\\{x:\\{t\\}|\phi\\}\cup\\{x:A|\phi\\}$ [by (38);
$\\{t\\}$ in left-hand side]
$\displaystyle\Leftrightarrow\phi(t)\mathrel{\wedge}\\{t\\}\cup
A\cup\\{x:A|\phi\\}=\\{t\\}\cup\\{x:A|\phi\\}$ [by (39)]
$\displaystyle\Leftrightarrow\phi(t)\mathrel{\wedge}A\cup\\{x:A|\phi\\}=\\{x:A|\phi\\}$
[by (37); basic property of $\parallel$ and $\cup$]