tcb@breakable

11institutetext: Tel Aviv University, Tel Aviv, Israel 22institutetext:
University of Wisconsin-Madison, Madison, WI, USA 33institutetext: VMware
Research, Palo Alto, CA, USA

# Efficient Implementation of an Abstract Domain of Quantified First-Order
Formulas

Eden Frenkel 11 0009-0009-4589-2173 Tej Chajed 22 0000-0002-9889-4828 Oded
Padon 33 0009-0006-4209-1635 Sharon Shoham 11 0000-0002-7226-3526

###### Abstract

This paper lays a practical foundation for using abstract interpretation with
an abstract domain that consists of sets of quantified first-order logic
formulas. This abstract domain seems infeasible at first sight due to the
complexity of the formulas involved and the enormous size of sets of formulas
(abstract elements). We introduce an efficient representation of abstract
elements, which eliminates redundancies based on a novel syntactic subsumption
relation that under-approximates semantic entailment. We develop algorithms
and data structures to efficiently compute the join of an abstract element
with the abstraction of a concrete state, operating on the representation of
abstract elements. To demonstrate feasibility of the domain, we use our data
structures and algorithms to implement a symbolic abstraction algorithm that
computes the least fixpoint of the best abstract transformer of a transition
system, which corresponds to the strongest inductive invariant. We succeed at
finding, for example, the least fixpoint for Paxos (which in our
representation has 1,438 formulas with $\forall^{*}\exists^{*}\forall^{*}$
quantification) in time comparable to state-of-the-art property-directed
approaches.

###### Keywords:

Abstract interpretation First-order logic Symbolic abstraction Invariant
inference Quantifier alternation Least fixpoint.

0

##  1 Introduction

Recent years have seen significant progress in automated verification based on
first-order logic. In particular, quantified first-order formulas have been
used to model many systems, their properties and their inductive invariants
[23, 19, 12, 27, 17, 6, 9, 15, 21, 30, 29, 13, 10, 8, 16, 14, 25, 1].
Automatic verification in this domain is challenging because of the
combination of the complexity of first-order reasoning performed by solvers
and the enormous search space of formulas, especially due to the use of
quantifiers. Despite these challenges, there are impressive success stories of
automatically inferring quantified inductive invariants for complex
distributed and concurrent algorithms [9, 30, 29, 13, 10, 8, 16, 14, 25].

Previous works on invariant inference for first-order logic search for
invariants in the form of sets of formulas (interpreted conjunctively) from
some language of quantified first-order formulas. Each approach fixes some
restricted, typically finite (but extremely large) language $\mathcal{L}$, and
searches for a set of $\mathcal{L}$-formulas that form an inductive invariant
using sophisticated heuristics and algorithmic techniques, such as property-
directed reachability (IC3) [13, 14], incremental induction [10, 25],
generalization from finite instances [16, 8], and clever forms of pruning and
exploration [30, 29]. While prior techniques can successfully handle some
challenging examples, the accumulation of specially-tailored techniques makes
the results computed by these techniques unpredictable, and makes it hard to
extend or improve them.

Abstract interpretation [4, 5] suggests a more systematic approach for the
development of verification algorithms based on logical languages, where we
consider sets of $\mathcal{L}$-formulas as elements in an abstract domain. The
abstraction of a set of states $S$ in this domain is given by
$\alpha(S)=\\{\varphi\in\mathcal{L}\mid\forall s\in S.\ s\models\varphi\\}$,
i.e., the formulas that are satisfied by all states in the set. Algorithms
based on abstract interpretation are better understood and are easier to
combine, extend, and improve. However, an abstract domain of quantified first-
order formulas seems infeasible: for interesting systems, the abstract
elements involved in proofs would contain an astronomical number of formulas.

The main contribution of this work is to develop algorithms and data
structures that make an abstract domain based on quantified first-order
formulas feasible. Working with this abstract domain introduces two main
challenges: (i) efficiently storing and manipulating abstract elements
comprising of many formulas, and (ii) overcoming solver limitations when
reasoning over them. This work focuses on the first challenge and adopts ideas
from prior work [14] to deal with the second. Our techniques lay a practical
foundation for using an abstract interpretation approach to develop new
analyses in the domain of quantified first-order formulas. We demonstrate
feasibility of the abstract domain by applying it to an analysis of several
intricate distributed protocols.

Our first key idea is to design a _subsumption relation_ for quantified first-
order formulas and use it to represent abstract elements (sets of formulas)
more compactly, pruning away some formulas that are redundant since they are
equivalent to or are entailed by another formula. Subsumption over
propositional clauses (disjunctions of literals) is traditionally used for
similar pruning purposes (e.g., [18]), but the generalization to first-order
formulas, which include disjunction, conjunction, and quantification, is
novel.

The second key ingredient of our approach is a way to manipulate abstract
elements in our representation. Rather than implementing the standard
operations of $\alpha$ (abstraction) and $\sqcup$ (abstract join), we observe
that our subsumption-based representation makes it more natural to directly
implement an operation that computes the join of an abstract element $a$ with
the abstraction of a given concrete state $s$, i.e., $a\sqcup\alpha(\\{s\\})$.
This operation can be used to compute the abstraction of a set of states, and
can also be used to compute the least fixpoint of the best abstract
transformer (in the style of symbolic abstraction [26]). The crux of computing
$a\sqcup\alpha(\\{s\\})$ is to _weaken_ the formulas in the representation of
$a$ to formulas that are subsumed by them and that $s$ satisfies.

Finally, the third key ingredient of our approach is a data structure for
storing a set of formulas, with efficient filters for (i) formulas that a
given state does not satisfy, and (ii) formulas that subsume a given formula.
This data structure is then used to store abstract elements, and the filters
make the implementation of $a\sqcup\alpha(\\{s\\})$ more efficient.

While the paper presents the ingredients of our approach (subsumption,
weakening, and the data structure) sequentially, they are interconnected; they
all affect each other in subtle ways, and must be designed and understood
together. Specifically, there is an intricate tradeoff between the precision
of subsumption, which determines the extent of pruning (and therefore the
compactness of the representation), and the complexity of abstract domain
operations such as weakening (e.g., for computing $a\sqcup\alpha(\\{s\\})$).
The definitions, algorithms, and data structures we present are carefully
crafted to balance these considerations. Our subsumption relation, which
approximates entailment, is cheap to compute, eliminates enough redundancy to
keep the representation of abstract elements compact, and enables an efficient
implementation of the weakening operation.

To evaluate our implementation of the abstract domain, we use it to implement
a symbolic abstraction [26] procedure that computes the least fixpoint of the
best abstract transformer of a transition system (i.e., the strongest
inductive invariant for the transition system in the given language). Our
evaluation uses benchmarks from the literature, mostly from safety
verification of distributed protocols. While our fixpoint computation
algorithm is not fully competitive with property-directed invariant inference
approaches that exploit various sophisticated heuristics and optimizations, it
does demonstrate that fixpoint computation in our abstract domain is feasible,
which is quite surprising given the amount of quantified formulas the domain
considers. Our approach successfully computes the least fixpoint for
transition systems that previously could only be analyzed using property-
directed, heuristic techniques (which do not compute the least fixpoint, but
an unpredictable heuristic fixpoint). For example, we succeed at finding the
strongest inductive invariant of Paxos as modeled in [23] (which in our
representation has 1,438 formulas with $\forall^{*}\exists^{*}\forall^{*}$
quantification, representing orders of magnitude more subsumed formulas).

In summary, this paper makes the following contributions:

  1. 1.

We develop a compact representation of sets of formulas based on a novel
syntactic _subsumption relation_. We make a tradeoff here between the extent
of pruning and efficiency, accepting some redundant formulas in exchange for
practical algorithms. (Sec. 3)

  2. 2.

We show how to implement a key operation of _weakening_ a formula to be
satisfied by a given state, and leverage it to compute the join of an abstract
element and the abstraction of a state, when abstract elements are represented
using our subsumption-based representation. (Sec. 4)

  3. 3.

We present a data structure that provides an efficient implementation of
operations used in the join computation described above. (Sec. 5)

  4. 4.

We evaluate the approach by applying it to compute the least fixpoint of the
best abstract transformer for several distributed and concurrent protocols
from the literature, demonstrating the promise of our approach. (Sec. 6)

The rest of this paper is organized as follows: Sec. 2 introduces definitions
and notation, Secs. 3, 4, 5 and 6 present the main contributions outlined
above, Sec. 7 discusses related work, and Sec. 8 concludes. The proofs of all
theorems stated in the paper are given in App. 0.B. An extended running
example appears in App. 0.A.

##  2 Background

##### First-order logic.

For simplicity of the presentation, we present our approach for single-sorted
first-order logic, although in practice we consider many-sorted logic. The
generalization of our methods to many-sorted logic is straightforward.

Given a first-order signature $\Sigma$ that consists of constant, function and
relation symbols, the sets of terms and formulas are defined in the usual way:
a _term_ $t$ is either a variable $x$, a constant $c$ or a function
application $f(t_{1},\ldots,t_{n})$ on simpler terms; a _formula_ is either an
equality between terms $t_{1}=t_{2}$, a relation application
$r(t_{1},\ldots,t_{n})$ on terms, or the result of applying Boolean
connectives or quantification. We also include $\bot$ as a formula (that is
never satisfied).

Terms and formulas are interpreted over first-order structures and assignments
to the (free) variables. Given a first-order signature $\Sigma$, a structure
$\sigma=(\mathcal{U},\mathcal{I})$ consists of a _universe_ $\mathcal{U}$ and
an _interpretation_ $\mathcal{I}$ to the symbols in $\Sigma$. We denote by
$\mathbf{structs}[{\Sigma}]$ the set of structures of $\Sigma$ whose universe
is a finite set.111 We restrict our attention to FOL fragments that have a
finite-model property. When considering formulas with free variables $V$, and
given some structure $\sigma=(\mathcal{U},\mathcal{I})$, an _assignment_
$\mu:V\to\mathcal{U}$ maps each variable to an element of the structure’s
universe. We write $(\sigma,\mu)\models\varphi$ to mean that a structure
$\sigma$ with an assignment $\mu$ satisfies a formula $\varphi$, and
$\psi\models\varphi$ to mean that a formula $\psi$ semantically entails
$\varphi$, i.e., $(\sigma,\mu)\models\psi$ whenever
$(\sigma,\mu)\models\varphi$.

##### Abstract interpretation.

Abstract interpretation [4, 5] is a framework for approximating the semantics
of systems. It assumes a concrete domain and an abstract domain, each given by
a partially ordered set, $(\mathcal{C},\sqsubseteq_{\mathcal{C}})$ and
$(\mathcal{A},\sqsubseteq_{\mathcal{A}})$, respectively. These are related via
a Galois connection consisting of a monotone abstraction function
$\alpha:\mathcal{C}\to\mathcal{A}$ and a monotone concretization function
$\gamma:\mathcal{A}\to\mathcal{C}$ satisfying
$\alpha(c)\sqsubseteq_{\mathcal{A}}a\iff c\sqsubseteq_{\mathcal{C}}\gamma(a)$
for all $a\in\mathcal{A}$ and $c\in\mathcal{C}$.

In this work we consider logical abstract domains parameterized by a finite
first-order language $\mathcal{L}$ of closed formulas over signature $\Sigma$.
In this context, concrete elements are sets of states from
$\mathbb{S}=\mathbf{structs}[{\Sigma}]$,222Later we consider non-closed
formulas and let $\mathbb{S}$ denote structures with assignments. i.e.,
$\mathcal{C}={\mathcal{P}(\mathbb{S})}$, ordered by
$\sqsubseteq_{\mathcal{C}}=\subseteq$ (set inclusion). Abstract elements are
sets of formulas from $\mathcal{L}$, i.e.,
$\mathcal{A}={\mathcal{P}(\mathcal{L})}$, ordered by
$\sqsubseteq_{\mathcal{A}}=\supseteq$, and the Galois connection is given by
$\alpha(S)=\\{\varphi\in\mathcal{L}\mid\forall s\in\mathbb{S}.\
s\models\varphi\\}$ and $\gamma(F)=\\{s\in\mathbb{S}\mid\forall\varphi\in F.\
s\models\varphi\\}$. That is, abstraction in this domain consists of all
$\mathcal{L}$-formulas that hold on a given concrete set, and concretization
consists of all states that satisfy a given set of formulas. Note that sets of
formulas are interpreted conjunctively in this context.

This logical abstract domain forms a join-semilattice (meaning every two
elements have a least upper bound) with a least element. The least element,
denoted $\bot_{\mathcal{A}}$ (not to be confused with the formula $\bot$), is
$\mathcal{L}$, and join, denoted $\sqcup$, corresponds to set intersection.
For example, $F\sqcup\alpha(\\{s\\})=F\cap\\{\varphi\in\mathcal{L}\mid
s\models\varphi\\}=\\{\varphi\in F\mid s\models\varphi\\}$, and can be
understood as _weakening_ $F$ by eliminating from it all formulas that are not
satisfied by $s$.

##  3 Subsumption-Based Representation of Sets of Formulas

In this section we develop an efficient representation for elements in the
abstract domain $\mathcal{A}={\mathcal{P}(\mathcal{L})}$ induced by a finite
first-order language $\mathcal{L}$. The abstract elements are sets of
formulas, interpreted conjunctively, which may be extremely large (albeit
finite). Our idea is to reduce the size and complexity of such sets by
avoiding redundancies that result from semantic equivalence and entailment.
For example, when representing a set of formulas we would like to avoid
storing both $\varphi$ and $\psi$ when they are semantically equivalent
($\varphi\equiv\psi$). Similarly, if $\varphi\models\psi$ then instead of
keeping both $\varphi$ and $\psi$ we would like to keep only $\varphi$.

In practice, it is not possible to remove all such redundancies based on
semantic equivalence and entailment, since, as we shall see in Sec. 4,
performing operations over the reduced representation of abstract elements
involves recovering certain subsumed formulas, and finding these in the case
of entailment essentially requires checking all formulas in the language. This
is clearly infeasible for complex languages such as the ones used in our
benchmarks (see Table 1), and is exacerbated by the fact that merely checking
entailment is expensive for formulas with quantifiers. Instead, our key idea
is to remove redundancies based on a cheap-to-compute subsumption relation,
which approximates semantic entailment, and enables efficient operations over
abstract elements such as joining them with an abstraction of a concrete
state.

We start the section with an inductive definition of a family of finite first-
order languages that underlies all of our developments (Sec. 3.1). We then
introduce a syntactic _subsumption_ relation for first-order formulas (Sec.
3.2), which we leverage to develop an efficient _canonicalization_ of
formulas, effectively determining a single representative formula for each
subsumption-equivalence class (Sec. 3.3). We then use antichains of canonical
formulas, i.e., sets of canonical formulas where no formula is subsumed by
another, to represent sets of formulas (Sec. 3.4). Secs. 4 and 5 develop ways
to effectively manipulate this representation in order to accommodate
important operations for abstract interpretation algorithms, such as weakening
an abstraction to include a given concrete state.

###  3.1 Bounded First-Order Languages

At core of our approach is an inductively-defined family of first-order
languages, termed _bounded first-order languages_. These languages are all
finite and bound various syntactic measures of formulas (e.g., number of
quantifiers, size of the Boolean structure), which, in turn, determine the
precision of the abstract domain. The inductive definition of bounded
languages facilitates efficient recursive implementations of our developments.

We fix a signature $\Sigma$ and a variable set $V$. Def. 1 provides the
inductive definition of the family of bounded first-order languages (over
$\Sigma$ and $V$), where each language $\mathcal{L}$ is also equipped with a
bottom element $\bot_{\mathcal{L}}$ (equivalent to false). We use
$\mathfrak{S}_{X}$ to denote the set of permutations over a set of variables
$X$, and use $\varphi\pi$ to denote the formula obtained by substituting free
variables in a formula $\varphi$ according to $\pi\in\mathfrak{S}_{X}$. A set
of formulas $F$ is $\mathfrak{S}_{X}$-closed if $\varphi\pi\in F$ for every
$\varphi\in F$, $\pi\in\mathfrak{S}_{X}$. All bounded first-order languages
will be $\mathfrak{S}_{V}$-closed; this will be important for
canonicalization. We use
$\bar{\varphi}=\langle{\varphi_{1},\ldots,\varphi_{n}}\rangle$ to denote a
sequence of formulas, $\varphi_{-i}$ to denote the formula $\varphi_{n-i+1}$
in the sequence, ${|{\bar{\varphi}}|}$ for the length of $\bar{\varphi}$, and
$[{\bar{\varphi}}]$ for its set of indices $\\{1,\dots,|\bar{\varphi}|\\}$. We
use $\mathcal{L}^{*}$ for the set of all (finite) sequences of formulas from
$\mathcal{L}$, and $\epsilon$ for the empty sequence (${|{\epsilon}|}=0$).

######  Definition 1 (Bounded First-Order Languages)

A _bounded first-order language_ is one of the following, where $X\subseteq V$
denotes a finite set of variables, and $\mathcal{L}$, $\mathcal{L}_{1}$ and
$\mathcal{L}_{2}$ denote bounded first-order languages:

$\displaystyle\mathcal{L}_{A}$ $\displaystyle=A\cup\\{\bot\\}\text{ with
}\bot_{\mathcal{L}_{A}}=\bot\text{, where }A\text{ is any finite
$\mathfrak{S}_{V}$-closed set of formulas}$
$\displaystyle{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$
$\displaystyle=\\{\varphi_{1}\vee\varphi_{2}\mid\varphi_{1}\in\mathcal{L}_{1},\varphi_{2}\in\mathcal{L}_{2}\\}\text{
with
}\bot_{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}=\bot_{\mathcal{L}_{1}}\vee\bot_{\mathcal{L}_{2}}$
$\displaystyle{{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$
$\displaystyle=\\{\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\in\mathcal{L}_{1},\varphi_{2}\in\mathcal{L}_{2}\\}\text{
with
}\bot_{{{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}=\bot_{\mathcal{L}_{1}}\wedge\bot_{\mathcal{L}_{2}}$
$\displaystyle{{\bm{\vee}}_{k}[{\mathcal{L}}]}$
$\displaystyle=\\{\bigvee\bar{\varphi}\mid\bar{\varphi}\in\mathcal{L}^{*}\text{
and }{|{\bar{\varphi}}|}\leq k\\}\text{ with
}\bot_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}=\bigvee\epsilon\text{, where
}k\in\mathbb{N}$ $\displaystyle{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$
$\displaystyle=\\{\bigwedge\bar{\varphi}\mid\epsilon\neq\bar{\varphi}\in\mathcal{L}^{*}\\}\text{
with
}\bot_{{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}}=\bigwedge\langle{\bot_{\mathcal{L}}}\rangle$
$\displaystyle{{\bm{\exists}}_{X}[{\mathcal{L}}]}$ $\displaystyle=\\{\exists
X.\varphi\mid\varphi\in\mathcal{L}\\}\text{ with
}\bot_{{{\bm{\exists}}_{X}[{\mathcal{L}}]}}=\exists X.\bot_{\mathcal{L}}$
$\displaystyle{{\bm{\forall}}_{X}[{\mathcal{L}}]}$ $\displaystyle=\\{\forall
X.\varphi\mid\varphi\in\mathcal{L}\\}\text{ with
}\bot_{{{\bm{\forall}}_{X}[{\mathcal{L}}]}}=\forall X.\bot_{\mathcal{L}}$
$\displaystyle{{\mathrlap{\bm{\exists}}\hskip
2.47998pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}$
$\displaystyle=\left\\{QX.\varphi\mid\varphi\in\mathcal{L},Q\in\left\\{\exists,\forall\right\\}\right\\}\text{
with }\bot_{{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}=\forall X.\bot_{\mathcal{L}}$

The base case is any finite set of formulas (over $\Sigma$ and $V$) that is
closed under variable permutations, augmented by $\bot$ (denoting false).
Typical examples include the set of all literals over $\Sigma$ and $V$ with a
bounded depth of function applications. We introduce binary language
constructors for disjunction and conjunction, each operating on two possibly
different languages. We also introduce constructors for homogeneous
disjunction of at most $k$ disjuncts, as well as unbounded non-empty
conjunction, over any single language. Finally, we introduce constructors for
quantification ($\exists$ or $\forall$) over a finite set of variables and a
language, as well as a constructor that includes both quantifiers for
languages where both options are desired. Note that for the construction of a
logical abstract domain, we are interested in languages where all formulas are
closed (have no free variables), but the inductive definition includes
languages with free variables.

The semantics of formulas in each language is defined w.r.t. states
$\mathbb{S}$ that consist of first-order structures and assignments to the
free variables, following the standard first-order semantics, extended to
conjunctions and disjunctions of finite sequences in the natural way, where
$\bigvee\epsilon\equiv\bot$. (We do not allow $\bigwedge\epsilon$, which would
have been equivalent to “true”, since it is not useful for our developments.)

Observe that for a fixed language $\mathcal{L}$, the formulas
$\varphi_{1}\vee\varphi_{2}\in{{\bm{\vee}}[{\mathcal{L}},{\mathcal{L}}]}$ and
$\bigvee\langle{\varphi_{1},\varphi_{2}}\rangle\in{{\bm{\vee}}_{2}[{\mathcal{L}}]}$
are syntactically different but semantically equivalent (and similarly for
conjunctions). Nonetheless, we introduce homogeneous disjunction and
conjunction since they admit a more precise subsumption relation, yielding a
more efficient representation of sets of formulas. Also note that we consider
bounded disjunction but unbounded conjunction; Sec. 4.3 explains this choice.

###### Example 1

$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
with $A=\\{p(x),\neg p(x),p(y),\neg p(y)\\}$ is a bounded first-order language
over signature $\Sigma$ that has one unary predicate $p$ and variables
$V=\\{x,y\\}$. Formulas in this language are universally quantified,
homogeneous disjunctions of at most two literals. For instance, $\mathcal{L}$
includes $\forall\\{x,y\\}.\bigvee\epsilon$, which is also
$\bot_{\mathcal{L}}$, as well as
$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle$,
$\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(y)}\rangle$, etc.

###  3.2 Syntactic Subsumption

Next, we define a _subsumption_ relation for each bounded first-order
language. The subsumption relation serves as an easy-to-compute under-
approximation for entailment between formulas from the same language. We use
$\sqsubseteq_{\mathcal{L}}$ to denote the subsumption relation for language
$\mathcal{L}$, or simply $\sqsubseteq$ when $\mathcal{L}$ is clear from
context. When $\varphi\sqsubseteq\psi$ we say $\varphi$ _subsumes_ $\psi$, and
then we will also have $\varphi\models\psi$.

######  Definition 2 (Subsumption)

We define $\sqsubseteq_{\mathcal{L}}$ inductively, following the definition of
bounded first-order languages, as follows, where $\circ\in\\{\vee,\wedge\\}$,
$k\in\mathbb{N}$, $Q,Q^{\prime}\in\\{\exists,\forall\\}$, $X$ is a finite set
of variables, and $\mathcal{L}$, $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are
bounded first-order languages:

$\displaystyle\varphi\sqsubseteq_{\mathcal{L}_{A}}\psi$ $\displaystyle\text{
iff }\varphi=\bot\text{ or }\varphi=\psi$
$\displaystyle\varphi_{1}\circ\varphi_{2}\sqsubseteq_{{\circ[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\psi_{1}\circ\psi_{2}$
$\displaystyle\text{ iff
}\varphi_{1}\sqsubseteq_{\mathcal{L}_{1}}\psi_{1}\text{ and
}\varphi_{2}\sqsubseteq_{\mathcal{L}_{2}}\psi_{2}\quad\text{(pointwise
extension)}$
$\displaystyle\bigvee\bar{\varphi}\sqsubseteq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\bigvee\bar{\psi}$
$\displaystyle\text{ iff }\exists
m\colon[{\bar{\varphi}}]\to[{\bar{\psi}}].\,\forall
i\in[{\bar{\varphi}}].\,\varphi_{i}\sqsubseteq\psi_{m(i)}\text{ and }m\text{
is injective}$
$\displaystyle\bigwedge\bar{\varphi}\sqsubseteq_{{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}}\bigwedge\bar{\psi}$
$\displaystyle\text{ iff }\exists
m\colon[{\bar{\psi}}]\to[{\bar{\varphi}}].\,\forall
i\in[{\bar{\psi}}].\,\varphi_{m(i)}\sqsubseteq\psi_{i}$
$\displaystyle(QX.\varphi)\sqsubseteq_{{Q_{X}[{\mathcal{L}}]}}(QX.\psi)$
$\displaystyle\text{ iff
}\exists\pi\in\mathfrak{S}_{X}.\,\varphi\sqsubseteq_{\mathcal{L}}\psi\pi$
$\displaystyle(QX.\varphi)\sqsubseteq_{{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}(Q^{\prime}X.\psi)$
$\displaystyle\text{ iff
}\exists\pi\in\mathfrak{S}_{X}.\,\varphi\sqsubseteq_{\mathcal{L}}\psi\pi\text{,
and }Q=\forall\text{ or }Q^{\prime}=\exists$

The subsumption relation of a bounded first-order language $\mathcal{L}$ is
composed, hierarchically, from the subsumption relations of the bounded first-
order languages that $\mathcal{L}$ is composed from. For example, the
languages participating in the composition of
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
defined in Ex. 1 are $\mathcal{L}_{A}$,
${{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}$, and
${{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$, and
each is equipped with its own subsumption relation.

In the base case, formulas in ${\mathcal{L}_{A}}$ are only subsumed by
themselves or by $\bot$. For example, considering Ex. 1,
$p(x)\not\sqsubseteq_{\mathcal{L}_{A}}p(y)$. Subsumption is lifted to
languages obtained by binary conjunctions and disjunctions in a pointwise
manner. For the languages obtained by homogeneous constructors, a mapping over
indices determines which element of one sequence subsumes which element of the
other. To approximate entailment, the mapping in the disjunctive case maps
each element of $\bigvee\bar{\varphi}$ to one in $\bigvee\bar{\psi}$ that it
subsumes, and in the conjunctive case maps each element of
$\bigwedge\bar{\psi}$ to one in $\bigwedge\bar{\varphi}$ that subsumes it. As
a result, subsumption is more precise in the homogeneous case than in the
binary one. For example, considering $A$ from Ex. 1, $p(x)\lor
p(y)\not\sqsubseteq_{{{\bm{\vee}}[{\mathcal{L}_{A}},{\mathcal{L}_{A}}]}}p(y)\lor
p(x)$, even though the formulas are semantically equivalent. On the other
hand,
$\bigvee\langle{p(x),p(y)}\rangle\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\bigvee\langle{p(y),p(x)}\rangle$

In the case of quantifiers, subsumption is lifted from the language of the
body while considering permutations over the quantified variables. For
example, in Ex. 1,
$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle\sqsubseteq_{\mathcal{L}}\forall\\{x,y\\}.\bigvee(p(y))$
due to variable permutations, even though
$\bigvee\langle{p(x)}\rangle\not\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\bigvee\langle{p(y)}\rangle$.
When both quantifiers are considered, a universal quantifier can subsume an
existential one.

The injectivity requirement for
$\sqsubseteq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}$ can be dropped without
damaging any of the definitions or theorems in this section, but it enables a
simpler definition of the weakening operator in Sec. 4 (as discussed further
in Sec. 4.3).

The following theorem establishes the properties of
$\sqsubseteq_{\mathcal{L}}$.

######  Theorem 3.1 (Properties of $\sqsubseteq_{\mathcal{L}}$)

For any bounded first-order language $\mathcal{L}$,
$\sqsubseteq_{\mathcal{L}}$ is a preorder (i.e., reflexive and transitive)
such that for any $\varphi,\psi\in\mathcal{L}$, if $\varphi\sqsubseteq\psi$
then $\varphi\models\psi$. Moreover,
$\bot_{\mathcal{L}}\sqsubseteq_{\mathcal{L}}\varphi$ for any
$\varphi\in\mathcal{L}$.

As with entailment, where two distinct formulas can entail each other (i.e.,
be semantically equivalent), there can be distinct formulas
$\varphi,\psi\in\mathcal{L}$ with $\varphi\sqsubseteq_{\mathcal{L}}\psi$ and
$\psi\sqsubseteq_{\mathcal{L}}\varphi$ (since $\sqsubseteq_{\mathcal{L}}$ is
not always a partial order, i.e., not antisymmetric). We call such formulas
_subsumption-equivalent_ , and denote it by
$\varphi\equiv_{\sqsubseteq_{\mathcal{L}}}\psi$.
($\equiv_{\sqsubseteq_{\mathcal{L}}}$ is clearly an equivalence relation.) The
existence of subsumption-equivalent formulas is a positive sign, indicating
that our subsumption relation manages to capture nontrivial semantic
equivalences. This is thanks to the definition of subsumption for homogeneous
disjunction and conjunction, as well as for quantification. For example,
$\bigvee\langle{\varphi,\psi}\rangle\equiv_{\sqsubseteq}\bigvee\langle{\psi,\varphi}\rangle$
(and similarly for conjunction), and if $\varphi\sqsubseteq\psi$ then
$\bigwedge\langle{\varphi,\psi}\rangle\equiv_{\sqsubseteq}\bigwedge\langle{\varphi}\rangle$.
For quantifiers, $QX.\varphi\equiv_{\sqsubseteq}QX.\varphi\pi$ for any
$\pi\in\mathfrak{S}_{X}$ and $Q\in\\{\exists,\forall\\}$. (In contrast,
$\sqsubseteq_{\mathcal{L}_{A}}$ is always antisymmetric, and the definitions
of ${{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$ and
${{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$ preserve antisymmetry.)

###  3.3 Canonicalization

As a first step towards an efficient representation of sets of formulas, we
use a canonicalization of formulas w.r.t. $\equiv_{\sqsubseteq}$, which allows
us to only store canonical formulas as unique representatives of their
(subsumption-) equivalence class. In general, a _canonicalization_ w.r.t. an
equivalence relation $\equiv$ over a set $S$ is a function $c\colon S\to S$
such that $\forall x\in S.\,c(x)\equiv x$ (representativeness) and $\forall
x,y\in S.\,x\equiv y\iff c(x)=c(y)$ (decisiveness). We say that $x$ is
_canonical_ if $c(x)=x$. When the equivalence relation is derived from a
preorder (as $\equiv_{\sqsubseteq}$ is derived from $\sqsubseteq$) then the
preorder is a partial order over the set of canonical elements. For our case,
that means that $\sqsubseteq_{\mathcal{L}}$ is a partial order over the set of
canonical $\mathcal{L}$-formulas.

It is useful, both for the algorithms developed in the sequel and for the
definition of canonicalization for ${Q_{X}[{\mathcal{L}}]}$
($Q\in\\{\bm{\exists},\bm{\forall},{\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}}\\}$), to define a total order $\leq_{\mathcal{L}}$
over canonical $\mathcal{L}$-formulas that extends
$\sqsubseteq_{\mathcal{L}}$. We thus define the canonicalization function
$c_{\mathcal{L}}$ and the total order $\leq_{\mathcal{L}}$ over canonical
$\mathcal{L}$-formulas by mutual induction. For a set of canonical
$\mathcal{L}$-formulas $F$, we use $\min_{\sqsubseteq_{\mathcal{L}}}F$ to
denote the set of formulas in $F$ not subsumed by others, i.e.,
$\min_{\sqsubseteq_{\mathcal{L}}}F=\\{\varphi\in F\mid\forall\psi\in
F\setminus\\{\varphi\\}.\,\psi\not\sqsubseteq\varphi\\}$, and use
$\min_{\leq_{\mathcal{L}}}F$ to denote the minimal element of a non-empty set
$F$ w.r.t. the total order $\leq_{\mathcal{L}}$. Finally, we use
${{\langle{\bar{\varphi}}\rangle}_{\leq}}$ for the sequence obtained by
sorting $\bar{\varphi}$ according to $\leq$ in ascending order, and similarly
${{\langle{F}\rangle}_{\leq}}$ for the sequence obtained by sorting the
elements of a set $F$.

######  Definition 3 (Canonicalization)

For every bounded first-order language $\mathcal{L}$, we define the
_canonicalization function_ $c_{\mathcal{L}}\colon\mathcal{L}\to\mathcal{L}$
and a total order $\leq_{\mathcal{L}}$ over canonical $\mathcal{L}$-formulas
by mutual induction (where $\circ\in\\{\vee,\wedge\\}$ and
$Q\in\\{\exists,\forall\\}$):

$\displaystyle c_{\mathcal{L}_{A}}(\varphi)$ $\displaystyle=\varphi$
$\displaystyle
c_{\circ[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}(\varphi_{1}\circ\varphi_{2})$
$\displaystyle=c_{\mathcal{L}_{1}}(\varphi_{1})\circ
c_{\mathcal{L}_{2}}(\varphi_{2})\text{ (pointwise)}$ $\displaystyle
c_{{\bm{\vee}}_{k}[{\mathcal{L}}]}(\bigvee\bar{\varphi})$
$\displaystyle=\bigvee{{\langle{c_{\mathcal{L}}(\varphi_{1}),\ldots,c_{\mathcal{L}}(\varphi_{{|{\bar{\varphi}}|}})}\rangle}_{\leq_{\mathcal{L}}}}$
$\displaystyle
c_{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}(\bigwedge\bar{\varphi})$
$\displaystyle=\bigwedge{{\langle{\min{}_{\sqsubseteq_{\mathcal{L}}}\\{c_{\mathcal{L}}(\varphi_{1}),\ldots,c_{\mathcal{L}}(\varphi_{{|{\bar{\varphi}}|}})\\}}\rangle}_{\leq_{\mathcal{L}}}}$
$\displaystyle c_{Q_{X}[{\mathcal{L}}]}(QX.\varphi)$
$\displaystyle=QX.\min{}_{\leq_{\mathcal{L}}}\left\\{c_{\mathcal{L}}(\varphi\pi)\bigm{|}\pi\in\mathfrak{S}_{X}\right\\}$
$\displaystyle c_{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}(QX.\varphi)$
$\displaystyle=c_{Q_{X}[{\mathcal{L}}]}(QX.\varphi)$

and

$\displaystyle\leq_{\mathcal{L}_{A}}$ $\displaystyle\text{ is an arbitrary
total order extending }\sqsubseteq_{\mathcal{L}_{A}}$
$\displaystyle\varphi_{1}\circ\varphi_{2}\leq_{{\circ[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\psi_{1}\circ\psi_{2}$
$\displaystyle\iff\varphi_{1}<_{\mathcal{L}_{1}}\psi_{1}\text{, or
}\varphi_{1}=\psi_{1}\text{ and }\varphi_{2}\leq_{\mathcal{L}_{2}}\psi_{2}$
$\displaystyle\begin{split}\bigvee\bar{\varphi}\leq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\bigvee\bar{\psi}&\iff\bar{\varphi}\text{
is a suffix of }\bar{\psi},\\\ &\hskip 28.00005pt\text{or }\exists
i\in[{\bar{\varphi}}]\cap[{\bar{\psi}}].\
\varphi_{-i}<_{\mathcal{L}}\psi_{-i}\land\forall j<i.\
\varphi_{-j}=\psi_{-j}\end{split}$
$\displaystyle\begin{split}\bigwedge\bar{\varphi}\leq_{{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}}\bigwedge\bar{\psi}&\iff\bar{\psi}\text{
is a prefix of }\bar{\varphi},\\\ &\hskip 28.00005pt\text{or }\exists
i\in[{\bar{\varphi}}]\cap[{\bar{\psi}}].\
\varphi_{i}<_{\mathcal{L}}\psi_{i}\land\forall j<i.\
\varphi_{j}=\psi_{j}\end{split}$ $\displaystyle
QX.\varphi\leq_{{Q_{X}[{\mathcal{L}}]}}QX.\psi$
$\displaystyle\iff\varphi\leq_{\mathcal{L}}\psi$ $\displaystyle
QX.\varphi\leq_{{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}Q^{\prime}X.\psi$
$\displaystyle\iff Q=Q^{\prime}\text{ and
}\varphi\leq_{\mathcal{L}}\psi\text{, or }Q=\forall\text{ and
}Q^{\prime}=\exists$

where $\varphi<_{\mathcal{L}}\psi$ is shorthand for
“$\varphi\leq_{\mathcal{L}}\psi$ and $\varphi\neq\psi$”.

Our inductive definition of canonicalization in Def. 3 recognizes the only
possible sources of nontrivial subsumption-equivalence in our construction:
non-canonicity of subformulas, ordering of sequences, internal subsumption in
${{\bm{\wedge}}_{\omega}[{\cdot}]}$-sequences, and permuting of quantified
variables. To address these, we canonicalize all subformulas, order their
sequences w.r.t $\leq_{\mathcal{L}}$ in ${{\bm{\vee}}_{k}[{\mathcal{L}}]}$ and
${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$, minimize
${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$-sequences w.r.t
$\sqsubseteq_{\mathcal{L}}$, and in ${Q_{X}[{\mathcal{L}}]}$,
$Q\in\\{\bm{\exists},\bm{\forall},{\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}}\\}$, choose the permutation yielding the
$\leq_{\mathcal{L}}$-least (canonical) body. For the total order in the cases
of Boolean connectives, we use lexicographic-like orderings carefully designed
to extend their associated subsumption relations (e.g., homogeneous
disjunction uses a right-to-left lexicographic ordering). For quantification,
the total order is directly lifted from the total order for canonical bodies.

As an example, consider
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
from Ex. 1. To obtain a canonicalization for $\mathcal{L}$, we provide an
arbitrary total order $\leq_{\mathcal{L}_{A}}$, say
$p(x)<_{\mathcal{L}_{A}}\neg
p(x)<_{\mathcal{L}_{A}}p(y)<_{\mathcal{L}_{A}}\neg p(y)$ (recall that
$\bot\in\mathcal{L}_{A}$ is least). This uniquely determines the total order
and canonicalization of $\mathcal{L}$ and all of its sub-languages. For
example, canonicalization of both
$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle$ and
$\forall\\{x,y\\}.\bigvee\langle{p(y)}\rangle$, which are
$\sqsubseteq_{\mathcal{L}}$-equivalent, is
$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle$. This is because
$p(x)<_{\mathcal{L}_{A}}p(y)$, and thus
$c_{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}\left(\bigvee\langle{p(x)}\rangle\right)=\bigvee\langle{p(x)}\rangle<_{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}\bigvee\langle{p(y)}\rangle=c_{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}\left(\bigvee\langle{p(y)}\rangle\right)$.
Note that $\bigvee\langle{p(x)}\rangle$ and $\bigvee\langle{p(y)}\rangle$ are
both canonical, but adding quantifiers merges the two formulas into the same
subsumption-equivalence class, necessarily making the quantified version of
one of them non-canonical. Similarly, the
$\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}$-equivalent formulas
$\bigvee\langle{p(x),p(y)}\rangle$ and $\bigvee\langle{p(y),p(x)}\rangle$ are
both canonicalized into $\bigvee\langle{p(x),p(y)}\rangle$ (by sorting the
sequences of literals according to $\leq_{\mathcal{L}_{A}}$).

The properties of $c_{\mathcal{L}}$ and $\leq_{\mathcal{L}}$ defined above are
established by the following theorem, which ensures that Def. 3 is well-
defined (e.g., that whenever $\min_{\leq_{\mathcal{L}}}$ is used,
$\leq_{\mathcal{L}}$ is a total order).

###### Theorem 3.2

For any bounded language $\mathcal{L}$, $c_{\mathcal{L}}$ is a
canonicalization w.r.t. $\equiv_{\sqsubseteq_{\mathcal{L}}}$, that is, it is
representative
($c_{\mathcal{L}}(\varphi)\equiv_{\sqsubseteq_{\mathcal{L}}}\varphi$) and
decisive ($\varphi\equiv_{\sqsubseteq_{\mathcal{L}}}\psi\iff
c_{\mathcal{L}}(\varphi)=c_{\mathcal{L}}(\psi)$); $\sqsubseteq_{\mathcal{L}}$
is a partial order over canonical $\mathcal{L}$-formulas; and
$\leq_{\mathcal{L}}$ is a total order over canonical $\mathcal{L}$-formulas
that extends $\sqsubseteq_{\mathcal{L}}$.

###### Corollary 1

For any $\varphi,\psi\in\mathcal{L}$, if
$\varphi\sqsubseteq_{\mathcal{L}}\psi$ then
$c_{\mathcal{L}}(\varphi)\leq_{\mathcal{L}}c_{\mathcal{L}}(\psi)$.

Henceforth, we use ${\bm{\mathcal{L}}}$ to denote the set of canonical
$\mathcal{L}$-formulas.

###  3.4 Representing Sets of Formulas

We utilize the subsumption relation and canonicalization to efficiently
represent sets of formulas which are interpreted conjunctively as antichains
of canonical formulas, where an _antichain_ is a set of formulas incomparable
by subsumption.

######  Definition 4 (Set Representation)

Given a set of formulas $F\subseteq\mathcal{L}$, we define its
_representation_ as the set
$R_{F}=\min{}_{\sqsubseteq_{\mathcal{L}}}\\{c(\varphi)\mid\varphi\in F\\}$.

The representation combines two forms of redundancy elimination: the use of
canonical formulas eliminates redundancies due to subsumption-equivalence, and
the use of $\sqsubseteq_{\mathcal{L}}$-minimal elements reduces the size of
the set by ignoring subsumed formulas. Observe that the more permissive the
subsumption relation is, the smaller the set representations are, because more
formulas will belong to the same equivalence class and more formulas will be
dropped by $\min_{\sqsubseteq_{\mathcal{L}}}$.

This representation preserves the semantics of a set of formulas (interpreted
conjunctively). For sets that are upward-closed w.r.t. subsumption (e.g.,
$\alpha(S)$ for some set of states $S$), the representation is lossless as a
set can be recovered by taking the upward closure of its representation. For a
set $F\subseteq\mathcal{L}$, we use ${\uparrow}{F}$ to denote its _upward
closure_ (w.r.t. $\sqsubseteq_{\mathcal{L}}$), given by
${\uparrow}{F}=\\{\varphi\in\mathcal{L}\mid\exists\psi\in
F.\,\psi\sqsubseteq_{\mathcal{L}}\varphi\\}$.

######  Theorem 3.3 (Antichain Representation)

For $F\subseteq\mathcal{L}$ and
$R_{F}=\min{}_{\sqsubseteq_{\mathcal{L}}}\\{c(\varphi)\mid\varphi\in F\\}$ its
representation, $\bigwedge R_{F}\equiv\bigwedge F$ and
${\uparrow}{R_{F}}={\uparrow}{F}$.

###### Corollary 2

If $F\subseteq\mathcal{L}$ is upward closed w.r.t. $\sqsubseteq_{\mathcal{L}}$
then $F={\uparrow}{R_{F}}$.

In particular, Cor. 2 applies to any set that is closed under entailment.

##  4 The Weaken Operator

This section develops an algorithm that computes a _weaken_ operator, which
takes a representation of an upward-closed set $F\subseteq\mathcal{L}$ and a
state $s$ and computes a representation of $F\cap\alpha(\\{s\\})=\\{\varphi\in
F\mid s\models\varphi\\}$. When $F$ is viewed as an abstract element, this
operation corresponds to computing $F\sqcup\alpha(\\{s\\})$. While it is not a
general abstract join operator, joining an abstract element with the
abstraction of a single concrete state is a powerful building block that can
be used, for example, to compute the abstraction of a set of states or even
the least fixpoint of the best abstract transformer (_á la_ symbolic
abstraction [26]).

In an explicit representation of $F$, computing $F\sqcup\alpha(\\{s\\})$ would
amount to removing from $F$ all the formulas that are not satisfied by $s$.
However, in the subsumption-based representation $R_{F}$, simply removing said
formulas is not enough. Instead, we must _weaken_ them, i.e., replace them by
formulas they subsume that are satisfied by $s$. To this end, Sec. 4.1
develops an appropriate weakening operator for a single formula, and Sec. 4.2
then lifts it to antichains used as representations.

###  4.1 Weakening a Single Canonical Formula

Given a canonical formula $\varphi$ and a state $s$ such that
$s\not\models\varphi$, the weaken operator computes the set of minimal
canonical formulas that are subsumed by $\varphi$ and satisfied by $s$, which
can be understood as a representation of
${\uparrow}{\\{\varphi\\}}\cap\alpha(\\{s\\})$.

######  Definition 5 (The Weaken Operator)

The _weaken operator_ of $\mathcal{L}$ is the function
$\mathcal{W}_{\mathcal{L}}\colon{\bm{\mathcal{L}}}\times\mathbb{S}\to{\mathcal{P}({\bm{\mathcal{L}}})}$
defined as follows:

${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}=\min{}_{\sqsubseteq_{\mathcal{L}}}\left\\{c_{\mathcal{L}}(\psi)\mid\psi\in\mathcal{L},\varphi\sqsubseteq\psi\text{,
and }s\models\psi\right\\}.$

Note that ${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ returns a
set of formulas, since there may be different incomparable ways to weaken
$\varphi$ such that it is satisfied by $s$.

While Def. 5 does not suggest a way to compute
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$, the following theorem
provides a recursive implementation of
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ that follows the
inductive structure of bounded languages. For the quantification cases, we
weaken according to all assignments of variables in $X\subseteq V$. Recall
that a state can be unpacked as $s=((\mathcal{U},\mathcal{I}),\mu)$ where
$(\mathcal{U},\mathcal{I})$ is a first-order structure (universe and
interpretation) and $\mu$ is an assignment to variables (into $\mathcal{U}$).
For assignments $\mu$ and $\nu$, we use ${\mu}\overleftarrow{\cup}{\nu}$ to
denote the assignment obtained from $\mu$ by updating (possibly extending) it
according to $\nu$.

######  Theorem 4.1 (Implementation of Weaken)

Let $\varphi\in\mathcal{L}$ be a canonical formula in a bounded first-order
language $\mathcal{L}$ and $s\in\mathbb{S}$ a state. If $s\models\varphi$ then
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}=\\{\varphi\\}$. If
$s\not\models\varphi$, then
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ is given by:

$\displaystyle{\mathcal{W}_{\mathcal{L}_{A}}\left({\varphi},{s}\right)}$
$\displaystyle=\begin{cases}\\{\psi\in A\mid s\models\psi\\},&\text{ if
}\varphi=\bot\\\ \emptyset,&\text{ if }\varphi\neq\bot\end{cases}$
$\displaystyle\begin{split}{\mathcal{W}_{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\left({\varphi_{1}\vee\varphi_{2}},{s}\right)}&=\\{\psi\vee\varphi_{2}\mid\psi\in{\mathcal{W}_{\mathcal{L}_{1}}\left({\varphi_{1}},{s}\right)}\\}\,\cup\\{\varphi_{1}\vee\psi\mid\psi\in{\mathcal{W}_{\mathcal{L}_{2}}\left({\varphi_{2}},{s}\right)}\\}\end{split}$
$\displaystyle{\mathcal{W}_{{{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\left({\varphi_{1}\wedge\varphi_{2}},{s}\right)}$
$\displaystyle=\\{\psi_{1}\wedge\psi_{2}\mid\psi_{1}\in{\mathcal{W}_{\mathcal{L}_{1}}\left({\varphi_{1}},{s}\right)},\psi_{2}\in{\mathcal{W}_{\mathcal{L}_{2}}\left({\varphi_{2}},{s}\right)}\\}$
$\displaystyle\begin{split}{\mathcal{W}_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\left({\bigvee\bar{\varphi}},{s}\right)}&=\min{}_{\sqsubseteq_{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\left(W_{{|{\bar{\varphi}}|}}\cup
W_{{|{\bar{\varphi}}|}+1}\right)\text{ where }\\\
&W_{{|{\bar{\varphi}}|}}=\left\\{\bigvee{{\langle{\varphi_{1},\ldots,\varphi_{i-1},\psi,\varphi_{i+1},\ldots,\varphi_{{|{\bar{\varphi}}|}}}\rangle}_{\leq_{\mathcal{L}}}}\mid
i\in[{\bar{\varphi}}],\psi\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{i}},{s}\right)}\right\\}\text{
and }\\\
&W_{{|{\bar{\varphi}}|}+1}=\left\\{\bigvee{{\langle{\varphi_{1},\ldots,\varphi_{{|{\bar{\varphi}}|}},\psi}\rangle}_{\leq_{\mathcal{L}}}}\mid\psi\in{\mathcal{W}_{\mathcal{L}}\left({\bot_{\mathcal{L}}},{s}\right)}\text{
and }{|{\bar{\varphi}}|}<k\right\\}\end{split}$
$\displaystyle{\mathcal{W}_{{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}}\left({\bigwedge\bar{\varphi}},{s}\right)}$
$\displaystyle=\left\\{\bigwedge{{\langle{\min{}_{\sqsubseteq_{\mathcal{L}}}{\mathcal{W}_{\mathcal{L}}\left({\varphi_{1}},{s}\right)}\cup\cdots\cup{\mathcal{W}_{\mathcal{L}}\left({\varphi_{|{\bar{\varphi}}|}},{s}\right)}}\rangle}_{\leq_{\mathcal{L}}}}\right\\}$
$\displaystyle\begin{split}{\mathcal{W}_{{{\bm{\exists}}_{X}[{\mathcal{L}}]}}\left({\exists
X.\varphi},{((\mathcal{U},\mathcal{I}),\mu)}\right)}&=\min{}_{\sqsubseteq_{{\bm{\exists}}_{X}[{\mathcal{L}}]}}\\{c(\exists
X.\psi)\mid\nu\colon
X\to\mathcal{U},\psi\in{\mathcal{W}_{\mathcal{L}}\left({\varphi},{((\mathcal{U},\mathcal{I}),{\mu}\overleftarrow{\cup}{\nu})}\right)}\\}\end{split}$
$\displaystyle\begin{split}{\mathcal{W}_{{{\bm{\forall}}_{X}[{\mathcal{L}}]}}\left({\forall
X.\varphi},{((\mathcal{U},\mathcal{I}),\mu)}\right)}&=\min{}_{\sqsubseteq_{{\bm{\forall}}_{X}[{\mathcal{L}}]}}\\{c(\forall
X.\psi)\mid\psi\in\Omega_{\varphi}\left(\\{((\mathcal{U},\mathcal{I}),{\mu}\overleftarrow{\cup}{\nu})\mid\nu\colon
X\to\mathcal{U}\\}\right)\\}\\\ &\text{where
}\Omega_{\varphi_{0}}\left(\\{s_{1},\ldots,s_{n}\\}\right)=\\{\varphi_{n}\mid\varphi_{1}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{0}},{s_{1}}\right)},\ldots,\varphi_{n}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{n-1}},{s_{n}}\right)}\\}\end{split}$
$\displaystyle\begin{split}{\mathcal{W}_{{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}\left({\exists
X.\varphi},{s}\right)}&={\mathcal{W}_{{{\bm{\exists}}_{X}[{\mathcal{L}}]}}\left({\exists
X.\varphi},{s}\right)}\\\ {\mathcal{W}_{{{\mathrlap{\bm{\exists}}\hskip
1.73598pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}\left({\forall
X.\varphi},{s}\right)}&=\min{}_{\sqsubseteq_{{\mathrlap{\bm{\exists}}\hskip
1.23999pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}}\left({\mathcal{W}_{{{\bm{\exists}}_{X}[{\mathcal{L}}]}}\left({\exists
X.\varphi},{s}\right)}\cup{\mathcal{W}_{{{\bm{\forall}}_{X}[{\mathcal{L}}]}}\left({\forall
X.\varphi},{s}\right)}\right)\end{split}$

When $s\models\varphi$, no weakening of $\varphi$ is needed for $s$ to satisfy
it. In the case of $\mathcal{L}_{A}$, only $\bot$ can be weakened to make $s$
satisfy it, yielding the set of formulas from $A$ that are satisfied by $s$.
(For $\mathcal{L}_{A}$, weakening anything except $\bot$ that is not satisfied
by $s$ yields the empty set.) In the case of disjunction, it suffices for one
of the disjuncts to be satisfied by $s$. Therefore, weakening is done by (i)
weakening exactly one of the existing disjuncts, which applies to both
${{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$ and
${{\bm{\vee}}_{k}[{\mathcal{L}}]}$; or by (ii) adding a disjunct that weakens
$\bot_{\mathcal{L}}$, which applies only to
$\bigvee\bar{\varphi}\in{{\bm{\vee}}_{k}[{\mathcal{L}}]}$ when
${|{\bar{\varphi}}|}<k$. In the case of homogeneous disjunction, each
resulting disjunction needs to be sorted to restore canonicity; moreover, some
of the resulting disjunctions may be subsumed by others, so
$\min{}_{\sqsubseteq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}}$ is applied to the
set of weakened disjunctions. In the case of conjunction, all conjuncts need
to be weakened to be satisfied by $s$. In the binary case, this leads to all
pairs that combine weakened conjuncts. But in the homogeneous case a single
conjunction can accumulate all weakened conjuncts, so weakening always yields
a singleton set; filtering the weakened conjuncts using
$\min{}_{\sqsubseteq_{\mathcal{L}}}$ is required to ensure canonicity, as one
weakened conjunct may subsume another. To satisfy an existentially quantified
formula, it suffices for the body to be satisfied by a single assignment.
Therefore, each possible assignment $\nu$ contributes to the result of
weakening. In contrast, for a universally quantified formula the body must be
satisfied by all assignments. Therefore, the body of the formula is
iteratively weakened by _all_ assignments. In both cases, formulas are re-
canonicalized and non-minimal elements are removed. The case of
${{\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}$
combines the two quantified cases.

###### Example 2

Consider applying the weaken operator of
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
from Ex. 1 to the bottom element
$\bot_{\mathcal{L}}=\forall\\{x,y\\}.\bigvee\epsilon$, with the state
$s=((\mathcal{U},\mathcal{I}),\mu)$ where $\mathcal{U}=\\{a,b\\}$,
$p^{\mathcal{I}}=\\{a,b\\}$, and $\mu$ is an empty assignment. To weaken the
universally quantified formula, we first iteratively weaken its body,
$\varphi_{0}=\bigvee\epsilon$, with the states $s_{1},\ldots,s_{4}$, each of
which extends $s$ with one of the 4 possible assignments to $x,y$. Since all
of these states satisfy $p(x)$ and $p(y)$, the first weakening (with $s_{1}$)
results in $\\{\bigvee\langle{p(x)}\rangle,\bigvee\langle{p(y)}\rangle\\}$,
and no formula is weakened further in later iterations (since both of them are
already satisfied by $s_{2},s_{3},s_{4}$). As we have seen in Sec. 3.3, both
formulas are canonical; however, they become subsumption-equivalent when the
quantifier prefix is added, demonstrating the need for additional
canonicalization in the computation of weaken for
${{\bm{\forall}}_{X}[{\cdot}]}$. The result is the antichain of canonical
formulas $\\{\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle\\}$. Note that the
weakened formula $\bot_{\mathcal{L}}$ has 21 formulas in its
$\sqsubseteq_{\mathcal{L}}$-upward closure, and its weakening has 14 formulas
(see Sec. 0.A.4 for the lists of formulas); yet throughout the weakening
process we only dealt with at most two formulas.

###  4.2 Weakening Sets of Formulas

We lift the weaken operator to sets of canonical formulas. For a set
$R\subseteq{\bm{\mathcal{L}}}$, we define
${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}=\min{}_{\sqsubseteq}\bigcup_{\varphi\in
R}{\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$, motivated by the
following theorem.

######  Theorem 4.2 (From Weaken to Join)

Let $F\subseteq\mathcal{L}$ be upward-closed w.r.t. $\sqsubseteq$, $R_{F}$ its
representation ($R_{F}=\min{}_{\sqsubseteq}\\{c(\varphi)\mid\varphi\in F\\}$),
and $s$ a state. The representation of $F\sqcup\alpha(\\{s\\})$ is given by
${\mathcal{W}_{\mathcal{L}}\left({R_{F}},{s}\right)}=\min{}_{\sqsubseteq}\bigcup_{\varphi\in
R_{F}}{\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$.

######  Corollary 3 (Weaken for a Set of States)

Let $F\subseteq\mathcal{L}$ be upward-closed w.r.t. $\sqsubseteq$, $R_{F}$ its
representation, and $s_{1},\ldots,s_{n}$ states. The representation of
$F\sqcup\alpha(\\{s_{1},\ldots,s_{n}\\})$ is given by
${\mathcal{W}_{\mathcal{L}}\left({{\mathcal{W}_{\mathcal{L}}\left({\cdots{\mathcal{W}_{\mathcal{L}}\left({{\mathcal{W}_{\mathcal{L}}\left({R_{F}},{s_{1}}\right)}},{s_{2}}\right)}},{\cdots
s_{n-1}}\right)}},{s_{n}}\right)}$.

######  Corollary 4 (Abstraction of a Set of States)

The representation of $\alpha(S)$ for a set of states $S$ is given by
${\mathcal{W}_{\mathcal{L}}\left({{\mathcal{W}_{\mathcal{L}}\left({\cdots{\mathcal{W}_{\mathcal{L}}\left({{\mathcal{W}_{\mathcal{L}}\left({\\{\bot_{\mathcal{L}}\\}},{s_{1}}\right)}},{s_{2}}\right)}},{\cdots
s_{n-1}}\right)}},{s_{n}}\right)}$.

Thm. 4.2 and Cor. 3 show that weakening of a single formula can be lifted to
compute join between an upward-closed set of formulas (represented using its
minimal elements w.r.t. $\sqsubseteq$) and the abstraction of one or more
states.

Next, we observe that we can implement
${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}$ by  (i) focusing only on
formulas that actually need weakening, i.e., formulas in $R$ that are not
satisfied by $s$, without iterating over formulas that $s$ satisfies; and
(ii) leveraging the $\leq_{\mathcal{L}}$ total order to accumulate the set of
minimal elements more efficiently.

Input: An antichain of canonical $\mathcal{L}$-formulas $R$ stored in the
$\text{LSet}[{\mathcal{L}}]$ data structure and a state $s\in\mathbb{S}$

Output: $R$ modified in place to store
${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}$

1

2$U$ := ${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$;

3 for  _$\varphi\in U$_ do $R$.remove($\varphi$);

4 $W$ := $\bigcup_{\varphi\in
U}{\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$;

5 for  _$\varphi\in W$ sorted by $\leq_{\mathcal{L}}$_ do

6 if  _${R}|_{\sqsubseteq{\varphi}}=\emptyset$_ then $R$.insert($\varphi$);

7

Algorithm 1 In-place Weaken for $\text{LSet}[{\mathcal{L}}]$

Alg. 1 presents our implementation of
${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}$ for an antichain $R$ of
canonical formulas and a state $s$. It updates $R$ to
${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}$ in place, which is useful
for computing an abstraction of a set of states (Cor. 3) or even for fixpoint
computation (Sec. 6). The algorithm uses a data structure
$\text{LSet}[{\mathcal{L}}]$ (whose implementation is explained in Sec. 5)
that stores a set of canonical $\mathcal{L}$-formulas and supports two
efficient filters: one for formulas that are not satisfied by a given state
$s$, denoted by ${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$; and one for
formulas that subsume a given formula $\varphi$, denoted by
${R}|_{\sqsubseteq{\varphi}}$. Formally:
${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}=\\{\psi\in R\mid
s\not\models\psi\\}$ and ${R}|_{\sqsubseteq{\varphi}}=\\{\psi\in
R\mid\varphi\sqsupseteq\psi\\}$.

To weaken $R$, Alg. 1 first identifies all formulas that need weakening using
the ${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ filter. It then removes these
formulas, weakens them, and adds the weakened formulas back to the set, while
filtering out formulas that are not $\sqsubseteq_{\mathcal{L}}$-minimal. For
the minimality filtering, we leverage $\leq_{\mathcal{L}}$ to ensure that if
$\varphi\sqsubseteq_{\mathcal{L}}\psi$ then $\varphi$ is added before $\psi$.
As a result, when inserting a formula $\varphi$ we only need to check that it
is not already subsumed by another formula in the set, which is done by
checking if ${R}|_{\sqsubseteq{\varphi}}$ is empty333While the implementation
of the weaken operator only checks the emptiness of
${R}|_{\sqsubseteq{\varphi}}$, the full set is used in the recursive
implementation of ${R}|_{\sqsubseteq{\varphi}}$ (Sec. 5).. Importantly, a
formula $\varphi\in R\setminus{R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ cannot
be subsumed by a formula from
${\mathcal{W}_{\mathcal{L}}\left({\psi},{s}\right)}$ for
$\psi\in{R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$. (If we assume the contrary
we easily get that $\psi\sqsubseteq\varphi$, contradicting the fact that $R$
is an antichain.)

###  4.3 Design Consideration and Tradeoffs

We are now in a position to discuss the tradeoffs and considerations that
arise in our framework in the design of languages and their subsumption
relations, explaining the design choices behind Defs. 1 and 2.

There is a tradeoff between the precision of the subsumption relation
$\sqsubseteq_{\mathcal{L}}$ and the complexity of implementing the weaken
operator $\mathcal{W}_{\mathcal{L}}$. From a representation perspective, a
more precise $\sqsubseteq_{\mathcal{L}}$ is desirable (i.e., relating more
formulas), since it means that the upward closure ${\uparrow}{\\{\varphi\\}}$
of a formula $\varphi$ is larger, and (upward-closed) sets of formulas can be
represented using less minimal formulas. On the other hand, when
${\uparrow}{\\{\varphi\\}}$ is larger, computing
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ is generally more
complicated. As an extreme case, if $\sqsubseteq_{\mathcal{L}}$ is trivial
(i.e., a formula only subsumes itself), we get no pruning in the
representation, but computing
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ is very easy, since it
is either $\\{\varphi\\}$ or $\emptyset$. As another example, compare
${{\bm{\vee}}[{\mathcal{L}},{\mathcal{L}}]}$ with
${{\bm{\vee}}_{2}[{\mathcal{L}}]}$. The subsumption relation of
${{\bm{\vee}}[{\mathcal{L}},{\mathcal{L}}]}$ is a pointwise extension, while
that of ${{\bm{\vee}}_{2}[{\mathcal{L}}]}$ allows swapping the two formulas,
which is more precise. (E.g.,
$\bigvee\langle{\varphi,\psi}\rangle\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}}]}}\bigvee\langle{\psi,\varphi}\rangle$
always holds but we might have
$\varphi\vee\psi\not\sqsubseteq_{{{\bm{\vee}}[{\mathcal{L}},{\mathcal{L}}]}}\psi\vee\varphi$.)
Accordingly, weakening of ${{{\bm{\vee}}_{2}[{\mathcal{L}}]}}$-formulas is
slightly more involved.

As opposed to reordering of disjuncts,
$\sqsubseteq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}$ does not allow multiple
disjuncts to subsume the same one, e.g.,
$\bigvee\langle{\varphi,\psi}\rangle\not\sqsubseteq_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\bigvee\langle{\psi}\rangle$
even if $\varphi\sqsubseteq_{\mathcal{L}}\psi$ (recall that the mapping
between disjuncts must be injective). This choice makes the computation of
$\mathcal{W}_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}$ simpler, as it only needs to
consider individually weakening each disjunct or adding a new one, but not
merging of disjuncts (to “make space” for a new disjunct). For example, when
computing
${\mathcal{W}_{{{\bm{\vee}}_{2}[{\mathcal{L}}]}}\left({\bigvee\langle{\varphi_{1},\varphi_{2}}\rangle},{s}\right)}$,
we do not have to consider formulas of the form
$\bigvee\langle{\varphi,\psi}\rangle$ where $s\models\psi$ and
$\varphi_{1},\varphi_{2}\sqsubseteq_{\mathcal{L}}\varphi$, which we would need
to include if the mapping was not required to be injective. One seemingly
undesirable consequence of the injectivity requirement is that canonical
formulas may contain redundant disjuncts, e.g.,
$\bigvee\langle{\varphi,\psi}\rangle$ when $\varphi\sqsubseteq\psi$ (or even
$\bigvee\langle{\varphi,\varphi}\rangle$). However, when formulas are obtained
by iterative weakening, as in the computation of the representation of
$\alpha(S)$ for a set of concrete states $S$, formulas with such redundancies
will be eliminated as they are always subsumed by a canonical formula without
redundancies.

Our design of bounded first-order languages uses bounded disjunction but
unbounded conjunction. The reason is that we obtain formulas by weakening
other formulas, starting from $\bot_{\mathcal{L}}$. In this scenario, bounding
the size of conjunctions would have replaced one conjunction by all of its
subsets smaller than the bound, causing an exponential blowup in the number of
formulas, without contributing much to generalization. On the other hand,
bounding the size of disjunctions yields generalization without blowing up the
number of formulas (in fact, it reduces the number of formulas compared to
unbounded disjunction).

##  5 Data Structure for Sets of Formulas

The implementation of ${\mathcal{W}_{\mathcal{L}}\left({R},{s}\right)}$
presented in Alg. 1 uses the filters
${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ and ${R}|_{\sqsubseteq{\varphi}}$.
Since the sets may be very large, a naive implementation that iterates over
$R$ to find formulas that are not satisfied by $s$
(${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$) or formulas that subsume
$\varphi$ (${R}|_{\sqsubseteq{\varphi}}$) may become inefficient. We therefore
introduce a data structure for bounded first-order languages, which we call
$\text{LSet}[{\mathcal{L}}]$, that stores a set of canonical
$\mathcal{L}$-formulas $R$ (not necessarily an antichain), and implements
${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ and ${R}|_{\sqsubseteq{\varphi}}$
without iterating over all formulas in $R$. The key idea is to define the
$\text{LSet}[{\mathcal{L}}]$ data structure recursively, following the
structure of $\mathcal{L}$, and to use auxiliary data to implement the
${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ and ${R}|_{\sqsubseteq{\varphi}}$
filters more efficiently.

For example, to implement
$\text{LSet}[{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}]$, we store
a set of ${{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$-formulas and two
auxiliary data fields: an LSet $L:\text{LSet}[{\mathcal{L}_{1}}]$ and a map
$M:\text{Map}[{\mathcal{L}_{1}},{\text{LSet}[{\mathcal{L}_{2}}]}]$. We
maintain the invariant that $\varphi_{1}\vee\varphi_{2}$ is in the set iff
$\varphi_{2}\in M[\varphi_{1}]$, and that $L$ contains the same
$\mathcal{L}_{1}$-formulas as the keys of $M$. Then, to find formulas that are
not satisfied by a state $s$, i.e., formulas where both disjuncts are not
satisfied by $s$, we first query $L$ to find $\varphi_{1}$’s that are not
satisfied by $s$, and for each such $\varphi_{1}$ we query the LSet
$M[\varphi_{1}]$ to find $\varphi_{2}$’s that are not satisfied by $s$.
Implementing the subsumption filter follows a similar logic.

Our implementation of $\text{LSet}[{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}]$ uses a
trie data structure that generalizes the binary case. Each edge is labeled by
an $\mathcal{L}$-formula, and each node represents an
${{\bm{\vee}}_{k}[{\mathcal{L}}]}$-formula that is the disjunction of the edge
labels along the path from the root to the node. The outgoing edges of each
node are stored using an $\text{LSet}[{\mathcal{L}}]$ that can be used to
filter only the edges whose label is not satisfied by a given state, or
subsumes a given formula. Then, the ${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$
and ${R}|_{\sqsubseteq{\bigvee\bar{\varphi}}}$ filters are implemented by
recursive traversals of the tree that only traverse filtered edges.

The recursive implementation for the other language constructors is simpler,
and follows a similar intuition to that of the cases presented above. The base
case $\text{LSet}[{\mathcal{L}_{A}}]$ is implemented without any auxiliary
data using straightforward iteration. The full details of the
$\text{LSet}[{\mathcal{L}}]$ data structure appear in App. 0.C.

##  6 Implementation and Evaluation

To evaluate our abstract domain implementation, we used it to implement a
symbolic abstraction [28, 26] algorithm that computes the least fixpoint of
the best abstract transformer of a transition system. We evaluated our
implementation on 19 distributed protocols commonly used as benchmarks in
safety verification and obtained promising results.

###  6.1 Implementation

We implemented our abstract domain and the symbolic abstraction algorithm in
Flyvy,444Flyvy’s code is available at https://github.com/vmware-
research/temporal-verifier. an open-source verification tool written in Rust,
whose implementation leverages parallelism and the optimizations detailed
below. The implementation and benchmarks used, as well as the log files and
raw results from the experiments reported, are publicly available in this
paper’s artifact [7].

Our implementation receives as input (i) a first-order transition system
$(\iota,\tau)$ over signature $\Sigma$, where $\iota$ is a closed first-order
formula over $\Sigma$ specifying the initial states and $\tau$ is a closed
first-order formula over two copies of $\Sigma$ specifying the transitions,
and (ii) a specification of a bounded first-order language $\mathcal{L}$ over
$\Sigma$ that defines the abstract domain ${\mathcal{P}(\mathcal{L})}$. The
reachable states of the system are the least fixpoint of a concrete
transformer
$\mathcal{T}:{\mathcal{P}(\mathbb{S})}\to{\mathcal{P}(\mathbb{S})}$ given by
$\mathcal{T}(S)=\\{s^{\prime}\in\mathbb{S}\mid
s^{\prime}\models\iota\lor\exists s\in S.\
\langle{s,s^{\prime}}\rangle\models\tau\\}$, where
$\langle{s,s^{\prime}}\rangle\models\tau$ indicates that the pair of states
satisfies the two-vocabulary formula $\tau$, i.e., that $s^{\prime}$ is a
successor of $s$ w.r.t the transition relation defined by $\tau$. For more
details on this style of modeling distributed systems in first-order logic,
see [22, 23, 24].

The Galois connection $(\alpha,\gamma)$ between ${\mathcal{P}(\mathbb{S})}$
and ${\mathcal{P}(\mathcal{L})}$ induces a _best abstract transformer_
${\mathcal{T}}^{\sharp}:{\mathcal{P}(\mathcal{L})}\to{\mathcal{P}(\mathcal{L})}$
defined by ${\mathcal{T}}^{\sharp}=\alpha\circ\mathcal{T}\circ\gamma$. Any
fixpoint of ${\mathcal{T}}^{\sharp}$, i.e., a set $F\subseteq\mathcal{L}$ such
that ${\mathcal{T}}^{\sharp}(F)=F$, is an _inductive invariant_ of
$(\iota,\tau)$ (when sets are interpreted conjunctively), and the least
fixpoint, $\text{lfp}{\mathcal{T}}^{\sharp}$, is the strongest inductive
invariant in $\mathcal{L}$. The strongest inductive invariant is useful for
verifying safety properties of the system, or showing that they cannot be
proven in $\mathcal{L}$ (if the strongest inductive invariant in $\mathcal{L}$
cannot prove safety, neither can any other inductive invariant expressible in
$\mathcal{L}$).

Symbolic abstraction computes $\text{lfp}{\mathcal{T}}^{\sharp}$ without
computing ${\mathcal{T}}^{\sharp}$ explicitly: beginning with $F=\mathcal{L}$
(the least element in ${\mathcal{P}(\mathcal{L})}$), and as long as
$F\neq{\mathcal{T}}^{\sharp}(F)$, a _counterexample to induction_ (CTI) of $F$
is sampled, i.e., a state $s^{\prime}\not\models\bigwedge F$ that is either an
initial state or the successor of a state $s$ with $s\models\bigwedge F$, and
$F$ is updated to $F\sqcup\alpha(\\{s^{\prime}\\})$. Our implementation uses
the representation $R_{F}$ and Alg. 1 to compute the join (more details in
App. 0.E). To find CTIs or determine that none exist we use SMT solvers (Z3
[20] and cvc5 [2]), with queries restricted to the EPR fragment (following
[23]), which ensures decidability and the existence of finite counterexamples.
Solvers still struggle in some challenging benchmarks, and we employ several
optimizations detailed in App. 0.F to avoid solver timeouts.

###  6.2 Experiments

To evaluate our techniques, we computed the least fixpoints (strongest
inductive invariants) of 19 distributed protocols commonly used as benchmarks
in safety verification, in a language expressive enough to capture their
human-written safety invariants. We used all EPR benchmarks from [14], except
for universally quantified Paxos variants. To evaluate the utility of the LSet
data structure described in Sec. 5, we ran each experiment twice, once using
LSet and once using a naive (but parallelized) implementation for the filters
${R}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ and ${R}|_{\sqsubseteq{\varphi}}$.

To specify the bounded first-order language for each example, we provide the
tool with a quantifier prefix (using ${{\bm{\exists}}_{X}[{\cdot}]}$,
${{\bm{\forall}}_{X}[{\cdot}]}$, and ${{\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}}_{X}[{\cdot}]}$) composed on top of a quantifier-free
bounded language that captures $k$-pDNF (following [14]). A $k$-pDNF formula
has the structure $c_{1}\to(c_{2}\vee\dots\vee c_{k})$, where
$c_{1},c_{2},\dots,c_{k}$ are cubes (conjunctions of literals). We specify
such formulas as
${{\bm{\vee}}[{{{\bm{\vee}}_{n}[{\mathcal{L}_{A_{1}}}]}},{{{\bm{\vee}}_{k-1}[{{{\bm{\wedge}}_{\omega}[{\mathcal{L}_{A_{2}}}]}}]}}]}$,
where $k$ and $n$ are parameters, and $A_{1}$ and $A_{2}$ are sets of
literals. Inspired by [29], we observe that we can restrict the variables used
in $A_{1}$ and $A_{2}$ to reduce the size of the language without losing
precision.555One of the language reductions used by [29] relies on an overly
generalized lemma [29, Lemma 6]; we confirmed this with the authors of [29].
We prove and use a correct (but less general) variant of this lemma, see App.
0.D for details.  For additional details see App. 0.D. The list of examples
with their language parameters appears in Table 1. For each example, we report
the quantifier structure, the $k$ and $n$ parameters of the $k$-pDNF
quantifier-free matrix, and the approximate size of the language
$\mathcal{L}$. Recall that the size of the abstract domain is
$2^{|\mathcal{L}|}$.

All experiments were performed on a 48-threaded machine with 384 GiB of RAM
(AWS’s z1d.metal) and a three-hour time limit. For each example we also
provide runtimes of two state-of-the-art safety verification tools, DuoAI [29]
and P-FOL-IC3 [14]. Note that, unlike our technique, these tools look for
_some_ inductive invariant proving safety, not necessarily the strongest, but
are also given fewer explicit language constraints. Moreover, the runtimes of
DuoAI and P-FOL-IC3 are sourced from their respective papers, and reflect
different architectures and time limits. Thus, the inclusion of their results
is not intended as a precise comparison to our tool, but as a reference for
the difficulty of the invariant inference task of each example, as evidenced
by state-of-the-art techniques.

###  6.3 Results

Table 1:  Symbolic abstraction over invariant inference benchmarks with a time
limit of 3 hours (10800s). We describe the bounded language underlying the
abstract domain of each example, including its approximate size, and report
the runtime of our technique—with and without using LSet—along with some
statistics. For reference, we provide runtimes of two state-of-the-art safety-
verification tools. ‘T/O’ indicates a timeout, and ‘N/A’ indicates that the
example was not reported by the respective tool.

Example Language Runtime (sec) LSet % in $\mathcal{W}$ Lfp. Size Max. Size
Safety (sec) quant. $k$ $n$ size P-FOL-IC3 DuoAI lockserv $\forall^{2}$ 1 3
$10^{4}$ $\mathbf{0.4\pm 0.1}$ ✓ $6\pm 1\ \%$ 12 $28\pm 7$ 19 1.9 $0.5\pm 0.1$
– $6\pm 1\ \%$ $29\pm 3$ toy-consensus- forall $\forall^{3}$ 1 3 $10^{3}$
$\mathbf{0.2\pm 0.0}$ ✓ $9\pm 2\ \%$ 5 $18\pm 5$ 4 1.9 $0.2\pm 0.0$ – $7\pm 1\
\%$ $18\pm 4$ ring-id $\forall^{3}$ 1 3 $10^{5}$ $\mathbf{1.6\pm 0.1}$ ✓
$16\pm 1\ \%$ 97 $182\pm 22$ 7 3.5 $1.9\pm 0.1$ – $20\pm 1\ \%$ $189\pm 22$
sharded-kv $\forall^{5}$ 1 3 $10^{4}$ $\mathbf{0.5\pm 0.1}$ ✓ $8\pm 0\ \%$ 20
$26\pm 2$ 8 1.9 $0.5\pm 0.0$ – $8\pm 1\ \%$ $26\pm 4$ ticket $\forall^{4}$ 1 5
$10^{9}$ $\mathbf{32.6\pm 3.3}$ ✓ $43\pm 7\ \%$ 2621 $8531\pm 119$ 23 23.9
$862.2\pm 21.9$ – $97\pm 0\ \%$ $8533\pm 121$ learning- switch $\forall^{4}$ 1
4 $10^{11}$ T/O ✓ $98\ \%$ – 9576194 76 52.4 T/O – $100\ \%$ 5998 consensus-
wo-decide $\forall^{3}$ 1 3 $10^{6}$ $\mathbf{3.0\pm 0.2}$ ✓ $19\pm 1\ \%$ 41
$717\pm 109$ 50 3.9 $4.0\pm 0.6$ – $38\pm 4\ \%$ $724\pm 43$ consensus- forall
$\forall^{4}$ 1 3 $10^{6}$ $\mathbf{3.5\pm 0.4}$ ✓ $21\pm 2\ \%$ 51 $740\pm
114$ 1980 11.9 $5.1\pm 0.9$ – $40\pm 6\ \%$ $708\pm 82$ cache $\forall^{6}$ 1
5 $10^{11}$ $\mathbf{4029.4\pm 220.7}$ ✓ $30\pm 2\ \%$ 106348 $271255\pm
13081$ 2492 N/A T/O – $100\pm 0\ \%$ $19183\pm 9466$ sharded-kv- no-lost-keys
$\forall^{1}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{2}$ 1 2
$10^{2}$ $\mathbf{0.3\pm 0.0}$ ✓ $3\pm 0\ \%$ 4 $4\pm 0$ 4 2.1 $0.3\pm 0.0$ –
$2\pm 0\ \%$ $4\pm 0$ toy-consensus- epr
$\forall^{2}({\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}})^{1}\forall^{1}$ 1 3 $10^{4}$ $\mathbf{0.3\pm 0.0}$ ✓
$9\pm 1\ \%$ 5 $18\pm 4$ 4 2.6 $0.3\pm 0.0$ – $7\pm 1\ \%$ $19\pm 3$
consensus- epr $({\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}})^{1}\forall^{4}$ 1 3 $10^{6}$ $\mathbf{5.1\pm 0.7}$ ✓
$17\pm 2\ \%$ 51 $800\pm 137$ 37 4.8 $8.8\pm 1.7$ – $46\pm 8\ \%$ $783\pm 88$
client- server-ae $\forall^{2}({\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}})^{1}$ 2 1 $10^{3}$ $\mathbf{0.2\pm 0.0}$ ✓ $4\pm 1\
\%$ 2 $5\pm 0$ 4 1.5 $0.2\pm 0.1$ – $3\pm 1\ \%$ $5\pm 0$ paxos-epr
$\forall^{4}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{2}$ 2 3
$10^{11}$ $\mathbf{621.5\pm 246.8}$ ✓ $1\pm 1\ \%$ 1438 $1693\pm 203$ 920 60.4
$789.6\pm 285.5$ – $11\pm 3\ \%$ $1737\pm 168$ flexible- paxos-epr
$\forall^{4}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{2}$ 2 3
$10^{11}$ $\mathbf{166.7\pm 29.3}$ ✓ $4\pm 1\ \%$ 964 $1622\pm 177$ 418 78.7
$235.6\pm 31.7$ – $35\pm 8\ \%$ $1575\pm 196$ multi- paxos-epr
$\forall^{5}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{3}$ 2 3
$10^{30}$ T/O ✓ $2\ \%$ – 27508 4272 1549 T/O – $100\ \%$ 6400 fast- paxos-epr
$\forall^{4}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{3}$ 2 4
$10^{14}$ T/O ✓ $1\ \%$ – 16290 9630 26979 T/O – $99\ \%$ 13683 stoppable-
paxos-epr $\forall^{7}({\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}})^{3}$ 2 5 $10^{155}$ T/O ✓ $100\ \%$ – 37529 $>$18297
4051 T/O – $100\ \%$ 3331 vertical- paxos-epr
$\forall^{4}({\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}})^{3}$ 3 5
$10^{54}$ T/O ✓ $100\ \%$ – 112990 T/O T/O T/O – $100\ \%$ 2576

The results of the symbolic abstraction computation are presented in Table 1.
For each experiment we report the runtime of our tool and the following
statistics: the percentage of time spent weakening formulas (as opposed to
searching for CTIs), the number of formulas in the representation of the
fixpoint (if reached), and the maximal number of formulas in the
representation of an abstract element throughout the run. Each experiment was
run five times, unless it timed out, in which case it was run only once. We
aggregate the results of each statistic across multiple runs as $median\pm
deviation$, where $deviation$ is the maximal distance between the median value
and the value of the statistic in any given run.

For simple examples, the fixpoint computation terminates very quickly, often
faster than the other tools, and maintains only tens or hundreds of formulas
throughout its run. Some of the larger examples, such as ticket, paxos-epr,
flexible-paxos-epr, and cache also terminate after similar times to the other
tools. In fact, this is the first work to compute least fixpoints for any
Paxos variant or cache. (DuoAI, for instance, has a component that attempts to
compute a precise fixpoint, but [29] reports that it times out on all Paxos
variants.)

Unsurprisingly, there is a significant gap between the runtimes of examples
with and without quantifier alternation, mostly due to the time spent in SMT
solvers. For example, in ticket we spend about $43\%$ of the runtime
performing weakenings, but this percentage drops to $1\%$ and $4\%$ for paxos-
epr and flexible-paxos-epr, respectively. This causes the runtime of paxos-epr
to exceed that of ticket by more than an order of magnitude, although its
fixpoint computation considers fewer formulas and actually spends less time
weakening. Similarly, in cache we manage to prove a fixpoint of a hundred
thousand formulas in about an hour and spend a third of it weakening formulas,
while multi-paxos-epr and fast-paxos-epr time out, although they consider far
fewer formulas and spend a negligible amount of time weakening.

Next, we observe that the use of LSet significantly reduces time spent in
weakening, leading to more than an order of magnitude difference even in
moderate examples, e.g., ticket and paxos-epr. In terms of the _total_
fixpoint computation time, in examples where the runtime is small or dominated
by the SMT solvers, the effect might be negligible, but otherwise the speedup
is significant. For example, cache is not solved within the 3-hour limit with
a naive data structure; it gets stuck after reaching $\sim$ 20,000 formulas in
the abstraction, whereas using LSet it is solved in about an hour while
handling more than ten times the number of formulas. Similarly, in the two
unsolved examples where SMT calls seem to be the bottleneck (multi-paxos-epr
and fast-paxos-epr), using a naive data structure causes weakening to become
the bottleneck and time out.

Finally, the remaining timeouts, learning-switch, stoppable-paxos-epr, and
vertical-paxos-epr, are the only examples where the weakening process itself
is the bottleneck. These are cases where the language induced by the human-
written invariant, using the constraining parameters of bounded languages,
create a inefficient weakening process. The cause for this is either a
profusion of literals in the basis language ($>$ 600 in learning-switch and
stoppable-paxos-epr, less than 200 in all other examples), or a very
expressive language (e.g., vertical-paxos-epr uses 3-pDNF, whereas all other
examples use 1- and 2-pDNF). For these examples, it might be necessary to
restrict the languages in additional ways, e.g., as was done in [29]. Our
experience, however, is that the more significant bottleneck for computing
least fixpoints for the most complicated examples is the SMT queries.

##  7 Related Work

Many recent works tackle invariant inference in first-order logic [9, 30, 29,
13, 10, 8, 16, 14, 25]. These works are all property-guided and employ
sophisticated heuristics to guide the search for invariants. Of these works,
the most closely related to ours are [30, 29]. DistAI [30] is restricted to
universally quantified invariants, while DuoAI [29] infers invariants with
quantifier alternations. DuoAI defines a “minimum implication graph”
enumerating all formulas in a first-order logical language, whose transitive
closure can be understood as a specific subsumption relation, and where
replacing a node with its successors can be understood as a form of weakening.
DuoAI’s “top-down refinement” precisely computes the strongest invariant in
the logical domain. However, this computation does not scale to complex
examples such as all Paxos variants, in which case “bottom-up refinement” is
used—a property-guided process that does not compute the strongest invariant.
Our approach based on a generic subsumption relation is both more principled
and more scalable, as it succeeds in computing the least fixpoint for some
Paxos variants.

Another work concerning a least-fixpoint in a logical domain is [18], which
computes the set of propositional clauses up to length $k$ implied by a given
formula, minimized by the subsumption relation $\sqsubseteq=\subseteq$; a
trie-based data structure is used to maintain the formulas, weaken them, and
check subsumption of a formula by the entire set. Both that data structure and
$\text{LSet}[{{{\bm{\vee}}_{k}[{\cdot}]}}]$ bear similarity to UBTrees [11],
also employed in [3], which store sets and implement filters for subsets and
supersets. However, while UBTrees and LSets always maintain ordered tree
paths, these are unordered in [18], which allows [18] to perform weakening
directly on the data structure, whereas we need to remove the unsatisfied
disjunctions, weaken, and insert them. On the other hand, this makes filtering
for subsets in UBTrees and LSets more efficient. Also note that LSet is more
general than both, since it supports a more general subsumption relation.

##  8 Conclusion

We have developed key algorithms and data structures for working with a
logical abstract domain of quantified first-order formulas. Our fundamental
idea is using a well-defined subsumption relation and a _weaken_ operator
induced by it. This idea makes the abstract domain feasible, and it is also
extensible: while we explored one possible subsumption relation and its
associated weaken operator, future work may explore others, representing
different tradeoffs between pruning and weakening. We demonstrated the
feasibility of our approach by computing the least abstract fixpoint for
several distributed protocols modeled in first-order logic—a challenging
application domain where previously only property-directed heuristics have
been successful. For some of the examples in our evaluation, the computation
still times out. In some of these cases, SMT queries (for computing CTIs)
become the bottleneck. Dealing with this bottleneck is an orthogonal problem
that we leave for future work. For the examples with the largest logical
languages, abstract domain operations remain the bottleneck, and future work
may either scale the abstract domain implementation to such languages or
explore combinations with property-directed approaches.

####  8.0.1 Acknowledgements

We thank Alex Fischman and James R. Wilcox for their contributions to the
Flyvy verification tool. We thank Raz Lotan, Kenneth McMillan, and the
anonymous reviewers for their helpful and insightful comments.

The research leading to these results has received funding from the European
Research Council under the European Union’s Horizon 2020 research and
innovation programme (grant agreement No [759102-SVIS]). This research was
partially supported by the Israeli Science Foundation (ISF) grant No. 2117/23.

## References

  * [1] Ball, T., Bjørner, N.S., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014. pp. 282–293. ACM (2014). https://doi.org/10.1145/2594291.2594317, https://doi.org/10.1145/2594291.2594317
  * [2] Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_24, https://doi.org/10.1007/978-3-030-99524-9_24
  * [3] Cadar, C., Dunbar, D., Engler, D.R., et al.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI. vol. 8, pp. 209–224 (2008)
  * [4] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973, https://doi.org/10.1145/512950.512973
  * [5] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778, https://doi.org/10.1145/567752.567778
  * [6] Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. In: TACAS (1). Lecture Notes in Computer Science, vol. 10205, pp. 76–95 (2017). https://doi.org/10.1007/978-3-662-54577-5_5
  * [7] Frenkel, E., Chajed, T., Padon, O., Shoham, S.: Efficient implementation of an abstract domain of quantified first-order formulas (artifact) (Apr 2024). https://doi.org/10.5281/zenodo.10938367, https://doi.org/10.5281/zenodo.10938367
  * [8] Goel, A., Sakallah, K.A.: On symmetry and quantification: A new approach to verify distributed protocols. In: NFM. Lecture Notes in Computer Science, vol. 12673, pp. 131–150. Springer (2021). https://doi.org/10.1007/978-3-030-76384-8_9
  * [9] Goel, A., Sakallah, K.A.: Towards an automatic proof of lamport’s paxos. In: FMCAD. pp. 112–122. IEEE (2021). https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_20
  * [10] Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: It’s a small (enough) world after all. In: Mickens, J., Teixeira, R. (eds.) 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021. pp. 115–131. USENIX Association (2021), https://www.usenix.org/conference/nsdi21/presentation/hance
  * [11] Hoffmann, J., Koehler, J.: A new method to index and query sets. In: IJCAI. vol. 99, pp. 462–467 (1999)
  * [12] Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: CAV. Lecture Notes in Computer Science, vol. 8044, pp. 756–772. Springer (2013). https://doi.org/10.1007/978-3-642-39799-8_53
  * [13] Karbyshev, A., Bjørner, N.S., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 7:1–7:33 (2017). https://doi.org/10.1145/3022187, https://doi.org/10.1145/3022187
  * [14] Koenig, J.R., Padon, O., Shoham, S., Aiken, A.: Inferring invariants with quantifier alternations: Taming the search space explosion. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 338–356. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_18, https://doi.org/10.1007/978-3-030-99524-9_18
  * [15] Löding, C., Madhusudan, P., Peña, L.: Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang. 2(POPL), 10:1–10:30 (2018). https://doi.org/10.1145/3158098, https://doi.org/10.1145/3158098
  * [16] Ma, H., Goel, A., Jeannin, J., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: SOSP. pp. 370–384. ACM (2019). https://doi.org/10.1145/3341301.3359651
  * [17] Mathur, U., Madhusudan, P., Viswanathan, M.: What’s decidable about program verification modulo axioms? In: TACAS (2). Lecture Notes in Computer Science, vol. 12079, pp. 158–177. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_10
  * [18] McMillan, K.: Don’t-care computation using k-clause approximation. Proc. IWLS’05 pp. 153–160 (2005)
  * [19] McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: SAS. Lecture Notes in Computer Science, vol. 11002, pp. 43–55. Springer (2018). https://doi.org/10.1007/978-3-319-99725-4_4
  * [20] de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24, https://doi.org/10.1007/978-3-540-78800-3_24
  * [21] Murali, A., Peña, L., Blanchard, E., Löding, C., Madhusudan, P.: Model-guided synthesis of inductive lemmas for FOL with least fixpoints. Proc. ACM Program. Lang. 6(OOPSLA2), 1873–1902 (2022). https://doi.org/10.1145/3563354, https://doi.org/10.1145/3563354
  * [22] Padon, O.: Deductive Verification of Distributed Protocols in First-Order Logic. Ph.D. thesis, Tel Aviv University (2019)
  * [23] Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1–108:31 (2017). https://doi.org/10.1145/3140568, https://doi.org/10.1145/3140568
  * [24] Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI. pp. 614–630. ACM (2016). https://doi.org/10.1145/2908080.2908118
  * [25] Padon, O., Wilcox, J.R., Koenig, J.R., McMillan, K.L., Aiken, A.: Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6(POPL), 1–29 (2022). https://doi.org/10.1145/3498712
  * [26] Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2937, pp. 252–266. Springer (2004). https://doi.org/10.1007/978-3-540-24622-0_21, https://doi.org/10.1007/978-3-540-24622-0_21
  * [27] Taube, M., Losa, G., McMillan, K.L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J.R., Woos, D.: Modularity for decidability of deductive verification with applications to distributed systems. In: PLDI. pp. 662–677. ACM (2018). https://doi.org/10.1145/3192366.3192414
  * [28] Thakur, A.V.: Symbolic abstraction: Algorithms and applications. Ph.D. thesis, The University of Wisconsin-Madison (2014)
  * [29] Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In: Aguilera, M.K., Weatherspoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022. pp. 485–501. USENIX Association (2022), https://www.usenix.org/conference/osdi22/presentation/yao
  * [30] Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: Distai: Data-driven automated invariant learning for distributed protocols. In: OSDI. pp. 405–421. USENIX Association (2021)

##  Appendix 0.A Running Example

###  0.A.1 Bounded First-Order Language

Consider the signature $\Sigma$ with one unary predicate $p$, and variables
$V=\\{x,y\\}$. These induce the set of first-order literals $A=\\{p(x),\neg
p(x),p(y),\neg p(y)\\}$, which can be used to define, for example, the bounded
language
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$.
Formulas in this language are universally quantified (homogeneous)
disjunctions of at most two literals. For instance, $\mathcal{L}$ includes

  * •

$\forall\\{x,y\\}.\bigvee\epsilon$, which is also $\bot_{\mathcal{L}}$,

  * •

$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle$,

  * •

$\forall\\{x,y\\}.\bigvee\langle{p(y),p(x)}\rangle$,

  * •

$\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(y)}\rangle$,

  * •

$\forall\\{x,y\\}.\bigvee\langle{p(x),p(x)}\rangle$,

  * •

etc.

###  0.A.2 Subsumption

The language
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
defined in Sec. 0.A.1 is composed, hierarchically, using three bounded first-
order languages: $\mathcal{L}_{A}$, ${{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}$,
and ${{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$.
Each is equipped with its own subsumption relation as defined inductively in
Def. 2. Observe that $p(x)\not\sqsubseteq_{\mathcal{L}_{A}}p(y)$ and
$\bigvee\langle{p(x)}\rangle\not\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\bigvee\langle{p(y)}\rangle$,
but

$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle\quad\sqsubseteq_{\mathcal{L}}\quad\forall\\{x,y\\}.\bigvee\langle{p(y)}\rangle,$

because by permuting $x$ and $y$ we can infer the above from
$\bigvee\langle{p(x)}\rangle\sqsubseteq\bigvee\langle{p(x)}\rangle$. Thus, one
source of subsumption is due to permutation of variables in ways that do not
change the semantics of a formula. Another is due to reordering subformulas in
a homogeneous connective, for example,

$\bigvee\langle{p(x),p(y)}\rangle\quad\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\quad\bigvee\langle{p(y),p(x)}\rangle.$

What the above demonstrates is that subsumption approximates semantic
entailment by utilizing the local semantic characteristics of each language.
It is indeed not the case that $p(x)\models p(y)$, but when both are
quantified universally, or when both are put in a disjunction and then
reordered, we can infer something useful about their semantics using simple
facts like $p(x)\models p(x)$ and $p(y)\models p(y)$, which are trivial and
thus assumed by the basis subsumption of $\mathcal{L}_{A}$.

###  0.A.3 Canonicalization

In order to have a canonicalization w.r.t $\equiv_{\sqsubseteq_{\mathcal{L}}}$
for
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$
defined in Sec. 0.A.1, we need to provide an arbitrary total order
$\leq_{\mathcal{L}_{A}}$. Say we choose

$p(x)<_{\mathcal{L}_{A}}\neg
p(x)<_{\mathcal{L}_{A}}p(y)<_{\mathcal{L}_{A}}\neg p(y),$

and recall that $\bot\in\mathcal{L}_{A}$ is least. Def. 3, together with Thm.
3.2, show that the above induces a canonicalization $c_{\mathcal{L}}$, as well
as a total order $\leq_{\mathcal{L}}$ over canonical $\mathcal{L}$-formulas
which extends $\sqsubseteq_{\mathcal{L}}$.

To see how the canonicalization $c_{\mathcal{L}}$ eliminates subsumption
equivalence, consider the two subsumption-equivalent formulas presented in
Sec. 0.A.2:

$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle\quad\equiv_{\sqsubseteq_{\mathcal{L}}}\quad\forall\\{x,y\\}.\bigvee\langle{p(y)}\rangle.$

The canonicalization of both is
$\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle$, since $c_{\mathcal{L}}$
selects the minimal canonical body after applying all variable permutations
over $x,y$ (Def. 3), and $p(x)<_{\mathcal{L}_{A}}p(y)$. Note that
$\bigvee\langle{p(x)}\rangle$ and $\bigvee\langle{p(y)}\rangle$ are both
canonical, but adding quantifiers merges the two formulas into the same
subsumption-equivalence class, necessarily making the quantified version of
one of them non-canonical.

Similarly, at the level of ${{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}$,

$\bigvee\langle{p(x),p(y)}\rangle\quad\equiv_{\sqsubseteq_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}}\quad\bigvee\langle{p(y),p(x)}\rangle,$

and canonicalization is achieved by sorting the sequences of literals, so both
are canonicalized as $\bigvee\langle{p(x),p(y)}\rangle$. Interestingly,
observe that for the quantified formula
$\forall\\{x,y\\}.\bigvee\langle{p(x),p(y)}\rangle$, any variable permutation
applied the quantifier-free body, after canonicalization w.r.t
${{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}$, i.e., sorting, yields
$\bigvee\langle{p(x),p(y)}\rangle$. Thus, for the subsumption-equivalence
class of this formula, canonicalization w.r.t
${{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}$ also eliminates any subsumption-
equivalence due to quantification. This is not entirely surprising, since in
this case, permuting the variables and permuting the literals in the
disjunction has the same effect.

###  0.A.4 Weakening

As an example, let us weaken the bottom element $\bot_{\mathcal{L}}$ for
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$,
i.e., $\forall\\{x,y\\}.\bigvee\epsilon$, with the state
$s=((\mathcal{U},\mathcal{I}),\mu)$ where $\mathcal{U}=\\{a,b\\}$,
$\mathcal{I}(p)=\\{a,b\\}$, and $\mu$ is an arbitrary assignment. At the
topmost level, the weakening procedure for
$\mathcal{L}={{\bm{\forall}}_{\\{x,y\\}}[{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}]}$,
detailed in Thm. 4.1, requires us to first compute

$\Omega_{\varphi_{0}}\left(\\{s_{1},\ldots,s_{n}\\}\right)=\\{\varphi_{n}\mid\varphi_{1}\in{\mathcal{W}_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\left({\varphi_{0}},{s_{1}}\right)},\ldots,\varphi_{n}\in{\mathcal{W}_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\left({\varphi_{n-1}},{s_{n}}\right)}\\}$

where $\varphi_{0}=\bigvee\epsilon$, and $s_{1},\ldots,s_{n}$ are all updates
of $s$ with assignments to $x,y$. The above can be computed iteratively as
follows:

  * •

$R_{0}:=\\{\bigvee\epsilon\\}$;

  * •

$R_{1}:=\bigcup_{\varphi\in
R_{0}}{\mathcal{W}_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\left({\varphi},{s_{1}}\right)}$;

  * •

$\cdots$

  * •

$R_{n}:=\bigcup_{\varphi\in
R_{n-1}}{\mathcal{W}_{{{\bm{\vee}}_{2}[{\mathcal{L}_{A}}]}}\left({\varphi},{s_{n}}\right)}$.

In our case $n=4$, and all updated states satisfy $p(x)$ and $p(y)$.
Therefore,
$R_{1}=\\{\bigvee\langle{p(x)}\rangle,\bigvee\langle{p(y)}\rangle\\}$, and no
formula is weakened further, since both formulas in $R_{1}$ are satisfied by
the remaining $s_{2},s_{3},s_{4}$. Thus, $R_{1}=\cdots=R_{n}$. As expected, at
the end of this process we are guaranteed to get formulas satisfying all
possible updates of $s$ with assignments to $x,y$.

As we saw in Sec. 0.A.3, both of the resulting formulas are canonical;
however, adding the requisite quantification results in one non-canonical
formula. This demonstrates the need for additional canonicalization for
${{\bm{\forall}}_{X}[{\cdot}]}$.

Note the savings the subsumption-based representation affords us even for this
simple language. The singleton $\\{\bot_{\mathcal{L}}\\}$, which we
effectively weakened per Alg. 1, represents the following abstract element
containing 21 formulas:

$\displaystyle\mathcal{L}=\Big{\\{}\ $
$\displaystyle\forall\\{x,y\\}.\bigvee\epsilon,\
\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{p(x),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{\neg p(x),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(x),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(x),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(x),\neg p(y)}\rangle$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{p(y),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),\neg p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{\neg p(y),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(y),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(y),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(y),\neg p(y)}\rangle\ \Big{\\}}.$

Moreover, the singleton $\\{\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle\\}$
we got from the weakening process represents the following abstract element
containing 14 formulas:

$\displaystyle\hskip 14.00003pt\Big{\\{}\ $
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{p(x),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(x),\neg p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{\neg p(x),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(x),p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{p(y),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),p(y)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),\neg p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{p(y),\neg p(y)}\rangle,$
$\displaystyle\forall\\{x,y\\}.\bigvee\langle{\neg p(y),p(x)}\rangle,\
\forall\\{x,y\\}.\bigvee\langle{\neg p(y),p(y)}\rangle\ \Big{\\}},$

but throughout the weakening process we only dealt with at most two formulas.

##  Appendix 0.B Proofs for Subsumption-Based Representation

###  0.B.1 Correctness of Subsumption

######  Proof (Thm. 3.1)

The proof follows the inductive definition of subsumption in Def. 2. The
semantic claim, that for each $\varphi,\psi\in\mathcal{L}$ if
$\varphi\sqsubseteq\psi$ then $\varphi\models\psi$, is straightforward to
verify using the definition of $\varphi\sqsubseteq\psi$ for each case: For the
base case we have $\varphi=\bot$ or $\varphi=\psi$, which implies
$\varphi\models\psi$. For both disjunction cases, if each disjunct of
$\varphi$ has a disjunct of $\psi$ that it subsumes, and therefore entails,
then any state satisfying $\varphi$, which therefore satisfies one of its
disjuncts, also satisfies some disjunct of $\psi$. For both conjunction cases,
if each conjunct of $\psi$ has a conjunct of $\varphi$ that subsumes it, and
therefore entails it, than any state satisfying $\varphi$, which therefore
satisfies all of its conjuncts, must also satisfy all of the conjuncts of
$\psi$. These conditions for disjunction and conjunction, respectively, are
ensured by the respective subsumption relations. For the case of quantifiers,
adding the same quantification to any $\varphi$ and $\psi$, or quantifying
$\varphi$ universally and $\psi$ existentially, as well as permuting
quantified variables, all maintain entailment, so the semantic property of
subsumption can be directly lifted from the induction hypothesis.

Next, we prove by induction that $\sqsubseteq_{\mathcal{L}}$ is a preorder for
all $\mathcal{L}$; i.e., that it is reflexive and transitive. For the base
case of $\sqsubseteq_{\mathcal{L}_{A}}$ the claim clearly holds. For
$\mathcal{L}_{1}\circ\mathcal{L}_{2}$ where $\circ\in\\{\vee,\wedge\\}$,
$\sqsubseteq_{\mathcal{L}_{1}\circ\mathcal{L}_{2}}$ is the standard preorder
resulting from pointwise extension, which maintains reflexivity and
transitivity. For ${{\bm{\vee}}_{k}[{\mathcal{L}}]}$, reflexivity is shown by
choosing the mapping $m(i)=i$ and using the reflexivity of
$\sqsubseteq_{\mathcal{L}}$ (i.h.); regarding transitivity, given
$\bigvee\bar{\varphi}\sqsubseteq\bigvee\bar{\psi}\sqsubseteq\bigvee\bar{\xi}$,
there exist injective $m_{1}:[{\bar{\varphi}}]\to[{\bar{\psi}}]$ and
$m_{2}:[{\bar{\psi}}]\to[{\bar{\xi}}]$, so $m_{2}\circ
m_{1}:[{\bar{\varphi}}]\to[{\bar{\xi}}]$ is injective and guarantees
$\varphi_{i}\sqsubseteq_{\mathcal{L}}\psi_{m_{1}(i)}\sqsubseteq_{\mathcal{L}}\xi_{(m_{2}\circ
m_{1})(i)}$, and using the transitivity of $\sqsubseteq_{\mathcal{L}}$ (i.h.),
$\varphi_{i}\sqsubseteq_{\mathcal{L}}\xi_{(m_{2}\circ m_{1})(i)}$. The cases
of ${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$ and ${Q_{X}[{\mathcal{L}}]}$ for
$Q\in\\{\exists,\forall\\}$ are proven in a similar manner, by choosing the
identity mapping or permutation, respectively, to show reflexivity, and
composing mappings or permutations to show transitivity. For
${{\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}$, the subsumption relation
extends the subsumption relations of ${Q_{X}[{\mathcal{L}}]}$ for
$Q\in\\{\exists,\forall\\}$, and reflexivity and transitivity can easily be
lifted from them.

Lastly, the fact that $\bot_{\mathcal{L}}\sqsubseteq_{\mathcal{L}}\varphi$ for
any $\varphi\in\mathcal{L}$ easily follows from its definition, using a
similar inductive argument over the structure of bounded languages.

###  0.B.2 Correctness of Canonicalization

######  Proof (Thm. 3.2)

The proof follows the mutually inductive definitions of the canonicalization
and the total order in Def. 3. To avoid confusion, we write $c(\cdot)$,
$\sqsubseteq$, and $\leq$ to refer to the canonicalization and orders of the
language for which the claim is proven in the induction step (omitting the
subscript).

The fact that $c$ is representative, i.e., that
$c(\varphi)\equiv_{\sqsubseteq}\varphi$ for all $\varphi$, is apparent in
almost all cases, since they simply canonicalize subformulas in ways which,
given the induction hypothesis, clearly result in subsumption-equivalent
formulas. The only interesting case is
${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$, where

$c_{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}(\bigwedge\bar{\varphi})=\bigwedge{{\langle{\min{}_{\sqsubseteq_{\mathcal{L}}}\\{c_{\mathcal{L}}(\varphi_{1}),\ldots,c_{\mathcal{L}}(\varphi_{{|{\bar{\varphi}}|}})\\}}\rangle}_{\leq_{\mathcal{L}}}},$

since there might be fewer formulas in
$\bar{\varphi}_{c}={{\langle{\min{}_{\sqsubseteq_{\mathcal{L}}}\\{c_{\mathcal{L}}(\varphi_{1}),\ldots,c_{\mathcal{L}}(\varphi_{{|{\bar{\varphi}}|}})\\}}\rangle}_{\leq_{\mathcal{L}}}}$
than in $\bar{\varphi}$, due to minimization, and the mappings from
$[{\bar{\varphi}}]$ to $[{\bar{\varphi}_{c}}]$ and from
$[{\bar{\varphi}_{c}}]$ to $[{\bar{\varphi}}]$ necessary to show mutual
subsumption are not obvious. However, due to $c_{\mathcal{L}}$ being
representative and decisive (i.h.), any formula in $\bar{\varphi}$ has a
formula subsuming it in $\bar{\varphi}_{c}$; and any formula in
$\bar{\varphi}_{c}$ has a subsumption-equivalent formula in $\bar{\varphi}$.
These facts precisely prove the existence of the required mappings.

For the decisiveness of $c$, we need to show that
$\varphi\equiv_{\sqsubseteq}\psi\iff c(\varphi)=c(\psi)$. We begin with the
“$\impliedby$” direction. This is again straightforward in all cases aside
from ${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$. For this case, denote
$\bigwedge\bar{\varphi}_{c}=c_{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}(\bigwedge\bar{\varphi})$
and
$\bigwedge\bar{\psi}_{c}=c_{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}(\bigwedge\bar{\psi})$,
and assume $\bigwedge\bar{\varphi}_{c}=\bigwedge\bar{\psi}_{c}$. Every formula
in $\bar{\varphi}$ has a formula in $\bar{\varphi}_{c}$ subsuming it, which is
therefore also in $\bar{\psi}_{c}$, and has a subsumption-equivalent formula
in $\bar{\psi}$. Thus, there is a mapping
$m:[{\bar{\varphi}}]\to[{\bar{\psi}}]$ showing
$\bigwedge\bar{\psi}\sqsubseteq\bigwedge\bar{\varphi}$, and the existence of a
mapping for the other direction is symmetrical.

Next, we recognize that the “$\implies$” direction of decisiveness for $c$ is
implied by its representativeness together with $\sqsubseteq$ being a partial
order (i.e., an anti-symmetric preorder) over canonical formulas, since then

$\varphi\equiv_{\sqsubseteq}\psi\quad\implies\quad
c(\varphi)\equiv_{\sqsubseteq}c(\psi)\quad\implies\quad c(\varphi)=c(\psi).$

We have already dealt with $c$ being representative, and $\sqsubseteq$ being a
partial order is implied by $\leq$ being a total order over canonical formulas
that extends $\sqsubseteq$, which we also need to prove. Therefore, it
suffices to prove the last claim.

The fact that $\leq$ is a total order can easily proven by observing that the
inductive definitions either lift total orders in pointwise manners
(${{\bm{\vee}}[{\cdot},{\cdot}]}$, ${{\bm{\wedge}}[{\cdot},{\cdot}]}$,
${{\bm{\exists}}_{X}[{\cdot}]}$, ${{\bm{\forall}}_{X}[{\cdot}]}$), in
lexicographic manners (${{\bm{\vee}}_{k}[{\cdot}]}$,
${{\bm{\wedge}}_{\omega}[{\cdot}]}$), or by chaining them
(${{\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}}_{X}[{\cdot}]}$).
Showing that $\leq$ extends $\sqsubseteq$ is more subtle. In the base case
this holds by definition. For ${\circ[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$
where $\circ\in\\{\vee,\wedge\\}$, given canonical
$\varphi_{1}\circ\varphi_{2}\sqsubseteq\psi_{1}\circ\psi_{2}$ it holds that
$\varphi_{1}\sqsubseteq_{\mathcal{L}_{1}}\psi_{1}$ and
$\varphi_{2}\sqsubseteq_{\mathcal{L}_{2}}\psi_{2}$, and therefore (i.h.)
$\varphi_{1}\leq_{\mathcal{L}_{1}}\psi_{1}$ and
$\varphi_{2}\leq_{\mathcal{L}_{2}}\psi_{2}$, which implies
$\varphi_{1}\circ\varphi_{2}\leq\psi_{1}\circ\psi_{2}$.

For ${{\bm{\vee}}_{k}[{\mathcal{L}}]}$, given canonical
$\bigvee\bar{\varphi}\sqsubseteq\bigvee\bar{\psi}$, there exists an
_injective_ $m:[{\bar{\varphi}}]\to[{\bar{\psi}}]$ such that for all
$i\in[{\bar{\varphi}}]$, $\varphi_{i}\sqsubseteq_{\mathcal{L}}\psi_{m(i)}$,
and thus $\varphi_{i}\leq_{\mathcal{L}}\psi_{m(i)}$. Since $\bar{\varphi}$ and
$\bar{\psi}$ are canonical, they are ordered by $\leq_{\mathcal{L}}$. Consider
the following cases:

  * •

There exists $i\geq 1$ such that $\varphi_{-i}\neq\psi_{-i}$. Let this $i$ be
minimal. By definition of the total order for
${{\bm{\vee}}_{k}[{\mathcal{L}}]}$,
$\bigvee\bar{\varphi}\leq\bigvee\bar{\psi}$ if
$\varphi_{-i}<_{\mathcal{L}}\psi_{-i}$. Assume for the sake of contradiction
that $\varphi_{-i}>_{\mathcal{L}}\psi_{-i}$ (we already know they are not
equal). Observe that every
$j\in\\{|\bar{\varphi}|-i+1,\dots,|\bar{\varphi}|\\}$ must have
$m(j)>|\bar{\psi}|-i+1$, since otherwise
$\varphi_{j}\geq_{\mathcal{L}}\varphi_{-i}>_{\mathcal{L}}\psi_{-i}\geq_{\mathcal{L}}\psi_{m(j)}$,
contradicting $\varphi_{j}\sqsubseteq_{\mathcal{L}}\psi_{m(j)}$. But this is a
contradiction, since it means $m$ is not injective. Thus,
$\varphi_{-i}<_{\mathcal{L}}\psi_{-i}$.

  * •

Otherwise, $\bar{\varphi}$ is a suffix of $\bar{\psi}$. ($\bar{\varphi}$
cannot be longer than $\bar{\psi}$, since there is an injection from
$[{\bar{\varphi}}]$ to $[{\bar{\psi}}]$.) This case also implies
$\bigvee\bar{\varphi}\leq\bigvee\bar{\psi}$.

For ${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$, given canonical
$\bigwedge\bar{\varphi}\sqsubseteq\bigwedge\bar{\psi}$, there exists
$m:[{\bar{\psi}}]\to[{\bar{\varphi}}]$ such that for all $i\in[{\bar{\psi}}]$,
$\varphi_{m(i)}\sqsubseteq_{\mathcal{L}}\psi_{i}$, and thus
$\varphi_{m(i)}\leq_{\mathcal{L}}\psi_{i}$. Since $\bar{\varphi}$ and
$\bar{\psi}$ are canonical, they are _antichains_ w.r.t
$\sqsubseteq_{\mathcal{L}}$ ordered by $\leq_{\mathcal{L}}$. Consider the
following cases:

  * •

There exists $i\geq 1$ such that $\varphi_{i}\neq\psi_{i}$. Let this $i$ be
minimal. By definition of the total order for
${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$,
$\bigwedge\bar{\varphi}\leq\bigwedge\bar{\psi}$ if
$\varphi_{i}<_{\mathcal{L}}\psi_{i}$. Assume for the sake of contradiction
that $\varphi_{i}>_{\mathcal{L}}\psi_{i}$ (we already know they are not
equal). Observe that every $j\in\\{1,...,i\\}$ must have $m(j)<i$, since
otherwise
$\varphi_{m(j)}\geq_{\mathcal{L}}\varphi_{i}>_{\mathcal{L}}\psi_{i}\geq_{\mathcal{L}}\psi_{j}$,
contradicting $\varphi_{m(j)}\sqsubseteq_{\mathcal{L}}\psi_{j}$. But this
means that there are distinct $1\leq j_{1}<j_{2}\leq i$ with
$m(j_{1})=m(j_{2})$. Since $j_{1}<i$, we also know
$\varphi_{j_{1}}=\psi_{j_{1}}$. Thus, either $m(j_{1})=m(j_{2})=j_{1}$, which
means that
$\psi_{j_{1}}=\varphi_{j_{1}}=\varphi_{m(j_{2})}\sqsubseteq_{\mathcal{L}}\psi_{j_{2}}$
and $\bigwedge\bar{\psi}$ is not canonical; or $m(j_{1})=m(j_{2})\neq j_{1}$,
which means that
$\varphi_{m(j_{1})}\sqsubseteq_{\mathcal{L}}\psi_{j_{1}}=\varphi_{j_{1}}$ and
$\bigwedge\bar{\varphi}$ is not canonical. Therefore,
$\bigwedge\bar{\varphi}\leq\bigwedge\bar{\psi}$.

  * •

Otherwise, $\bar{\psi}$ is a prefix of $\bar{\varphi}$. ($\bar{\varphi}$
cannot be a strict prefix of $\bar{\psi}$, since then there would be an
element in $\bar{\varphi}$, which is also in $\bar{\psi}$, subsuming two
distinct elements in $\bar{\psi}$, making $\bar{\psi}$ non-canonical.) This
case also implies $\bigvee\bar{\varphi}\leq\bigvee\bar{\psi}$.

For ${Q_{X}[{\mathcal{L}}]}$ where $Q\in\\{\bm{\exists},\bm{\forall}\\}$,
given canonical $QX.\varphi\sqsubseteq QX.\psi$, there exists
$\pi\in\mathfrak{S}_{X}$ such that $\varphi\pi\sqsubseteq_{\mathcal{L}}\psi$.
Since $QX.\varphi$ is ${Q_{X}[{\mathcal{L}}]}$-canonical,

$\varphi=\min{}_{\leq_{\mathcal{L}}}\\{c_{\mathcal{L}}(\varphi\theta)\mid\theta\in\mathfrak{S}_{X}\\}\leq_{\mathcal{L}}c_{\mathcal{L}}(\varphi\pi)\equiv_{\sqsubseteq_{\mathcal{L}}}\varphi\pi\sqsubseteq_{\mathcal{L}}\psi,$

and since $\psi$ is $\mathcal{L}$-canonical, $\varphi\leq_{\mathcal{L}}\psi$
and therefore $QX.\varphi\leq QX.\psi$ as well. The case for
${{\mathrlap{\bm{\exists}}\hskip 3.09998pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}$
uses the two single-quantifier cases in a straightforward way.

###  0.B.3 Correctness of Set Representation

######  Proof (Thm. 3.3)

Let $F\subseteq\mathcal{L}$ and
$R_{F}=\min{}_{\sqsubseteq}\\{c(\varphi)\mid\varphi\in F\\}$ its
representation. Using the definition of $\min{}_{\sqsubseteq}$, and due to
$\sqsubseteq$ being antisymmetric and well-founded over canonical formulas,
for all $\varphi\in F$ there exists $\psi\in R_{F}$ such that $\psi\sqsubseteq
c(\varphi)$. Due to $c$ being representative,
$c(\varphi)\equiv_{\sqsubseteq}\varphi$.

The above implies that for all $\varphi\in F$ there exists $\psi\in R_{F}$
such that $\psi\sqsubseteq\varphi$, and thus $\psi\models\varphi$; from this
is it easy to deduce that ${\uparrow}{R_{F}}\supseteq{\uparrow}{F}$ and
$\bigwedge R_{F}\models\bigwedge F$. Next, by definition, any $\psi\in R_{F}$
has some $\varphi\in F$ such that $\psi=c(\varphi)$, and therefore
$\psi\equiv_{\sqsubseteq}\varphi$ and $\psi\equiv\varphi$. This implies
${\uparrow}{F}\supseteq{\uparrow}{R_{F}}$ and $\bigwedge F\models\bigwedge
R_{F}$.

Taken together, we conclude that $\bigwedge R_{F}\equiv\bigwedge F$ and
${\uparrow}{R_{F}}={\uparrow}{F}$.

###  0.B.4 Correctness of Weaken

######  Proof (Thm. 4.1)

In order to prove that the implementation in Thm. 4.1 satisfies the
specification in Def. 5, it suffices to show that for all
$\varphi\in\mathcal{L}$ and $s\in\mathbb{S}$,  (i)
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$is an antichain w.r.t
$\sqsubseteq_{\mathcal{L}}$ of canonical formulas,  (ii) all formulas in
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ are subsumed by
$\varphi$ and satisfied by $s$, and  (iii) for all $\psi\in\mathcal{L}$ with
$\varphi\sqsubseteq\psi$ and $s\models\psi$, there exists
$\xi\in{\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ such that
$\xi\sqsubseteq\psi$.

The above suffices for the proof since item (ii) shows that

${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}\subseteq{\uparrow}{\big{(}\min{}_{\sqsubseteq_{\mathcal{L}}}\left\\{c_{\mathcal{L}}(\psi)\mid\psi\in\mathcal{L},\varphi\sqsubseteq\psi\text{,
and }s\models\psi\right\\}\big{)}},$

item (iii) shows that

${\uparrow}{{\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}}\supseteq\min{}_{\sqsubseteq_{\mathcal{L}}}\left\\{c_{\mathcal{L}}(\psi)\mid\psi\in\mathcal{L},\varphi\sqsubseteq\psi\text{,
and }s\models\psi\right\\},$

and because item (i) tells us
${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}$ is an antichain of
canonical formulas,

${\mathcal{W}_{\mathcal{L}}\left({\varphi},{s}\right)}=\min{}_{\sqsubseteq_{\mathcal{L}}}\left\\{c_{\mathcal{L}}(\psi)\mid\psi\in\mathcal{L},\varphi\sqsubseteq\psi\text{,
and }s\models\psi\right\\}.$

As usual, we shall prove (i)–(iii) by induction on the recursive
implementation. These clearly hold for any case where $s\models\varphi$, where
the implementation always returns $\\{\varphi\\}$. We therefore restrict our
discussion to cases where $s\not\models\varphi$. Claim (i) can be easily
verified by going case by case and using claim (i) of the induction
hypothesis. Claim (ii) is likewise easy to prove using claim (ii) of the
induction hypothesis, together with the definition of subsumption (Def. 2),
and the fact that a disjunction is satisfied if one of its disjuncts is
satisfied, a conjunction is satsified if all of its conjuncts are satisfied,
an existentially quantified formula is satisfied if there exists a state
updated with an assignment to quantified variables which satisfies its body,
and a universally quantified formula is satisfied if all such updated states
satisfy its body.

Thus, it remains to inductively prove claim (iii), which we do case by case.
Keep in mind that we assume $s\not\models\varphi$.

For $\mathcal{L}_{A}$, if $\varphi=\bot$,
${\mathcal{W}_{\mathcal{L}_{A}}\left({\varphi},{s}\right)}$ contains all
$\psi\in\mathcal{L}_{A}$ with $s\models\psi$, so (iii) holds due to
reflexivity of $\sqsubseteq$. If $\varphi\neq\bot$, nothing satisfying $s$ is
subsumed by it.

For ${{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$, assume
$\varphi_{1}\vee\varphi_{2}\sqsubseteq\psi_{1}\vee\psi_{2}$ and
$s\models\psi_{1}\vee\psi_{2}$. Either $s\models\psi_{1}$, in which case there
exists
$\xi_{1}\in{\mathcal{W}_{\mathcal{L}_{1}}\left({\varphi_{1}},{s}\right)}$ such
that $\xi_{1}\sqsubseteq_{\mathcal{L}_{1}}\psi_{1}$ (i.h.), and then
$\xi_{1}\vee\varphi_{2}\sqsubseteq\psi_{1}\vee\psi_{2}$ and
$\xi_{1}\vee\varphi_{2}\in{\mathcal{W}_{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\left({\varphi_{1}\vee\varphi_{2}},{s}\right)}$;
or $s\models\psi_{2}$, in which case there exists
$\xi_{2}\in{\mathcal{W}_{\mathcal{L}_{2}}\left({\varphi_{2}},{s}\right)}$ such
that $\xi_{2}\sqsubseteq_{\mathcal{L}_{2}}\psi_{2}$ (i.h.), and then
$\varphi_{1}\vee\xi_{2}\sqsubseteq\psi_{1}\vee\psi_{2}$ and
$\varphi_{1}\vee\xi_{2}\in{\mathcal{W}_{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\left({\varphi_{1}\vee\varphi_{2}},{s}\right)}$.

For ${{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$, assume
$\varphi_{1}\wedge\varphi_{2}\sqsubseteq\psi_{1}\wedge\psi_{2}$ and
$s\models\psi_{1}\wedge\psi_{2}$. Then $s\models\psi_{1}$ and
$s\models\psi_{2}$. So there exist
$\xi_{1}\in{\mathcal{W}_{\mathcal{L}_{1}}\left({\varphi_{1}},{s}\right)}$ and
$\xi_{2}\in{\mathcal{W}_{\mathcal{L}_{2}}\left({\varphi_{2}},{s}\right)}$ with
$\xi_{1}\sqsubseteq\psi_{1}$ and $\xi_{2}\sqsubseteq\psi_{2}$ (i.h.) (meaning
$\xi_{1}\wedge\xi_{2}\sqsubseteq\psi_{1}\wedge\psi_{2}$) such that
$\xi_{1}\wedge\xi_{2}\in{\mathcal{W}_{{{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}\left({\varphi_{1}\wedge\varphi_{2}},{s}\right)}$.

For ${{\bm{\vee}}_{k}[{\mathcal{L}}]}$, assume
$\bigvee\bar{\varphi}\sqsubseteq\bigvee\bar{\psi}$ and
$s\models\bigvee\bar{\psi}$. So there exists an injective
$m:[{\bar{\varphi}}]\to[{\bar{\psi}}]$ such that for all
$i\in[{\bar{\varphi}}]$, $\varphi_{i}\sqsubseteq\psi_{m(i)}$; and there exists
some $j\in[{\bar{\psi}}]$ such that $s\models\psi_{j}$. Consider the following
cases:

  * •

There exists $i\in[{\bar{\varphi}}]$ such that $m(i)=j$. Since
$\varphi_{i}\sqsubseteq\psi_{j}$ and $s\models\psi_{j}$, there exists some
$\xi\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{i}},{s}\right)}$ such that
$\xi\sqsubseteq\psi_{j}$ (i.h.), and

$\bigvee\bar{\xi}=\bigvee{{\langle{\varphi_{1},\ldots,\varphi_{i-1},\xi,\varphi_{i+1},\ldots,\varphi_{{|{\bar{\varphi}}|}}}\rangle}_{\leq_{\mathcal{L}}}}\sqsubseteq\bar{\psi},$

and
$\bigvee\bar{\xi}\in{\mathcal{W}_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\left({\bigvee\bar{\varphi}},{s}\right)}$,
(specifically, $\bigvee\bar{\xi}\in W_{{|{\bar{\varphi}}|}}$; see Thm. 4.1).

  * •

Otherwise, $m(i)\neq j$ for all $i\in[{\bar{\varphi}}]$. Therefore,
$\bar{\varphi}$ must be strictly shorter than $\bar{\psi}$, and therefore
${|{\bar{\varphi}}|}<k$. _Note that this is only the case because we required
$m$ to be injective when defining the subsumption relation. This is crucial
for weakening disjunctions in this way._ Since
$\bot_{\mathcal{L}}\sqsubseteq\psi_{j}$ and $s\models\psi_{j}$, there exists
some $\xi\in{\mathcal{W}_{\mathcal{L}}\left({\bot_{\mathcal{L}}},{s}\right)}$
such that $\xi\sqsubseteq\psi_{j}$ (i.h.), and

$\bigvee\bar{\xi}=\bigvee{{\langle{\varphi_{1},\ldots,\varphi_{{|{\bar{\varphi}}|}},\xi}\rangle}_{\leq_{\mathcal{L}}}}\sqsubseteq\bar{\psi},$

and
$\bigvee\bar{\xi}\in{\mathcal{W}_{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}\left({\bigvee\bar{\varphi}},{s}\right)}$,
(specifically, $\bigvee\bar{\xi}\in W_{{|{\bar{\varphi}}|}+1}$; see Thm. 4.1).

For ${{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}$, assume
$\bigwedge\bar{\varphi}\sqsubseteq\bigwedge\bar{\psi}$ and
$s\models\bigwedge\bar{\psi}$. So there exists
$m:[{\bar{\psi}}]\to[{\bar{\varphi}}]$ such that for all $i\in[{\bar{\psi}}]$,
$\varphi_{m(i)}\sqsubseteq\psi_{i}$ and $s\models\psi_{i}$. Therefore, for any
$i\in[{\bar{\psi}}]$ there exists
$\xi^{\prime}_{i}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{m(i)}},{s}\right)}$
such that $\xi^{\prime}_{i}\sqsubseteq\varphi_{m(i)}\sqsubseteq\psi_{i}$
(i.h.); and if we denote

$\bar{\xi}={{\langle{\min{}_{\sqsubseteq_{\mathcal{L}}}{\mathcal{W}_{\mathcal{L}}\left({\varphi_{1}},{s}\right)}\cup\cdots\cup{\mathcal{W}_{\mathcal{L}}\left({\varphi_{|{\bar{\varphi}}|}},{s}\right)}}\rangle}_{\leq_{\mathcal{L}}}}$

then each $\xi^{\prime}_{i}$ has $j\in[{\bar{\xi}}]$ such that
$\xi_{j}\sqsubseteq\xi^{\prime}_{i}$. Thus, any $i\in[{\bar{\psi}}]$ has
$j\in[{\bar{\xi}}]$ such that $\xi_{j}\sqsubseteq\psi_{i}$, proving
$\bigwedge\bar{\xi}\sqsubseteq\bigwedge\bar{\psi}$; and indeed,
$\\{\bigwedge\bar{\xi}\\}={\mathcal{W}_{{{\bm{\wedge}}_{\omega}[{\mathcal{L}}]}}\left({\bigwedge\bar{\varphi}},{s}\right)}$.

For ${{\bm{\exists}}_{X}[{\mathcal{L}}]}$, assume $\exists
X.\varphi\sqsubseteq\exists X.\psi$ and
$((\mathcal{U},\mathcal{I}),\mu)\models\exists X.\psi$. So there exists
$\pi\in\mathfrak{S}_{X}$ such that $\varphi\sqsubseteq\psi\pi$; and since
$((\mathcal{U},\mathcal{I}),\mu)\models\exists X.\psi\pi$ as well, there
exists $\nu:X\to\mathcal{U}$ such that
$((\mathcal{U},\mathcal{I}),{\mu}\overleftarrow{\cup}{\nu})\models\psi\pi$.
Thus, there exists some
$\xi\in{\mathcal{W}_{\mathcal{L}}\left({\varphi},{((\mathcal{U},\mathcal{I}),{\mu}\overleftarrow{\cup}{\nu})}\right)}$
such that $\xi\sqsubseteq\psi\pi$, and therefore $\exists
X.\xi\sqsubseteq\exists X.\psi$; the rest of the proof follows due to
canonicalization being representative.

The case for ${{\bm{\forall}}_{X}[{\mathcal{L}}]}$, where we assume $\forall
X.\varphi\sqsubseteq\forall X.\psi$ and $s\models\forall X.\psi$, is similar,
but instead of weakening $\varphi$ according to any one assignment we weaken
it via

$\Omega_{\varphi_{0}}\left(\\{s_{1},\ldots,s_{n}\\}\right)=\\{\varphi_{n}\mid\varphi_{1}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{0}},{s_{1}}\right)},\ldots,\varphi_{n}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{n-1}},{s_{n}}\right)}\\}$

where we set $\varphi_{0}=\varphi$ and the states $s_{1},\dots,s_{n}$ to be
all updates of $s$ with assignments to $X$. The proof proceeds inductively and
shows that for all $i=1,...,n$, there exist
$\varphi_{0}\in\\{\varphi\\},\varphi_{1}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{0}},{s_{1}}\right)},...,\varphi_{i}\in{\mathcal{W}_{\mathcal{L}}\left({\varphi_{i-1}},{s_{i}}\right)}$
subsuming $\psi\pi$, where $\pi\in\mathfrak{S}_{X}$ is the permutation for
which $\varphi\sqsubseteq\psi\pi$. The induction step is similar to the case
for ${{\bm{\exists}}_{X}[{\mathcal{L}}]}$, and holds since $\psi$ satisfies
all updated states.

The case for ${{\mathrlap{\bm{\exists}}\hskip
3.09998pt{\bm{\forall}}}_{X}[{\mathcal{L}}]}$, where we assume
$QX.\varphi\sqsubseteq Q^{\prime}X.\psi$ and $s\models Q^{\prime}X.\psi$,
follows from the weakening procedure for ${{\bm{\exists}}_{X}[{\mathcal{L}}]}$
when $Q=Q^{\prime}=\exists$, from the weakening procedure for
${{\bm{\forall}}_{X}[{\mathcal{L}}]}$ when $Q=Q^{\prime}=\forall$, and handles
the case $Q=\forall,Q^{\prime}=\exists$ by including the result of weakening
$\exists X.\varphi$ as well if $Q=\forall$.

##  Appendix 0.C The $\text{LSet}[{\mathcal{L}}]$ Data Structure

We introduce the $\text{LSet}[{\mathcal{L}}]$ data structure for storing sets
of canonical $\mathcal{L}$-formulas (the sets are not necessarily antichains,
see discussion below), and implementing the
${\cdot}|_{\not\Relbar\joinrel\mathrel{|}{s}}$ and
${\cdot}|_{\sqsubseteq{\psi}}$ filters.

Table 2: The $\text{LSet}[{\mathcal{L}}]$ data structure.

$\mathcal{L}_{A}$ Fields: $S:\text{Set}[{\mathcal{L}_{A}}]$ Invariants: $\top$
Implementing ${}|_{\not\Relbar\joinrel\mathrel{|}{s}}$: $\\{\varphi\in S\mid
s\not\models\varphi\\}$ Implementing ${}|_{\sqsubseteq{\psi}}$:
$\\{\bot,\psi\\}\cap S$ ${{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$
Fields: $S:\text{Set}[{{{\bm{\vee}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}]$
$L:\text{LSet}[{\mathcal{L}_{1}}]$
$M:\text{Map}[{\mathcal{L}_{1}},{\text{LSet}[{\mathcal{L}_{2}}]}]$ Invariants:
$\varphi_{1}\in
L\Leftrightarrow\varphi_{1}\in\mathbf{dom}({M})\Leftrightarrow\exists\varphi_{2}.\,\varphi_{1}\vee\varphi_{2}\in
S$ $\varphi_{2}\in M[\varphi_{1}]\Leftrightarrow\varphi_{1}\vee\varphi_{2}\in
S$ Implementing ${}|_{\not\Relbar\joinrel\mathrel{|}{s}}$:
$\\{\varphi_{1}\vee\varphi_{2}\mid\varphi_{1}\in{L}|_{\not\Relbar\joinrel\mathrel{|}{s}},\varphi_{2}\in{M[\varphi_{1}]}|_{\not\Relbar\joinrel\mathrel{|}{s}}\\}$
Implementing ${}|_{\sqsubseteq{\psi_{1}\vee\psi_{2}}}$:
$\\{\varphi_{1}\vee\varphi_{2}\mid\varphi_{1}\in{L}|_{\sqsubseteq{\psi_{1}}},\varphi_{2}\in{M[\varphi_{1}]}|_{\sqsubseteq{\psi_{2}}}\\}$
${{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}$ Fields:
$S:\text{Set}[{{{\bm{\wedge}}[{\mathcal{L}_{1}},{\mathcal{L}_{2}}]}}]$
$L_{1}:\text{LSet}[{\mathcal{L}_{1}}]$ $L_{2}:\text{LSet}[{\mathcal{L}_{2}}]$
$M_{1}:\text{Map}[{\mathcal{L}_{1}},{\text{LSet}[{\mathcal{L}_{2}}]}]$
$M_{2}:\text{Map}[{\mathcal{L}_{2}},{\text{LSet}[{\mathcal{L}_{1}}]}]$
Invariants: $\varphi_{1}\in
L_{1}\Leftrightarrow\varphi_{1}\in\mathbf{dom}({M_{1}})\Leftrightarrow\exists\varphi_{2}.\,\varphi_{1}\wedge\varphi_{2}\in
S$ $\varphi_{2}\in
M_{1}[\varphi_{1}]\Leftrightarrow\varphi_{1}\wedge\varphi_{2}\in S$
$\varphi_{2}\in
L_{2}\Leftrightarrow\varphi_{2}\in\mathbf{dom}({M_{2}})\Leftrightarrow\exists\varphi_{1}.\,\varphi_{1}\wedge\varphi_{2}\in
S$ $\varphi_{1}\in
M_{2}[\varphi_{2}]\Leftrightarrow\varphi_{1}\wedge\varphi_{2}\in S$
Implementing ${}|_{\not\Relbar\joinrel\mathrel{|}{s}}$:
$\\{\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\in{L_{1}}|_{\not\Relbar\joinrel\mathrel{|}{s}},\varphi_{2}\in
M_{1}[\varphi_{1}]\\}\,\cup$
$\\{\varphi_{1}\wedge\varphi_{2}\mid\varphi_{2}\in{L_{2}}|_{\not\Relbar\joinrel\mathrel{|}{s}},\varphi_{1}\in
M_{2}[\varphi_{2}]\\}$ Implementing
${}|_{\sqsubseteq{\psi_{1}\wedge\psi_{2}}}$:
$\\{\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\in{L}|_{\sqsubseteq{\psi_{1}}},\varphi_{2}\in{M[\varphi_{1}]}|_{\sqsubseteq{\psi_{2}}}\\}$
${{\bm{\vee}}_{k}[{\mathcal{L}}]}$ Fields:
$S:\text{Set}[{{{\bm{\vee}}_{k}[{\mathcal{L}}]}}]$ $r:\text{TreeNode}$ where
TreeNode is
$~{}~{}~{}~{}(\text{LSet}[{\mathcal{L}}],\text{Map}[{\mathcal{L}},{\text{TreeNode}}])$
Invariants:
$\text{collect}(r)=\\{\epsilon\\}\cup\\{\bar{\varphi}\mid\exists\bar{\psi}.\,(\bigvee(\bar{\varphi}+\bar{\psi}))\in
S\\}$ $(L,M):\text{TreeNode}\Rightarrow(\varphi\in
L\Leftrightarrow\varphi\in\mathbf{dom}({M}))$
$(L,M):\text{TreeNode}\wedge(L^{\prime},M^{\prime})=M[\varphi]\wedge\psi\in
L^{\prime}\Rightarrow\varphi\leq_{\mathcal{L}}\psi$ Implementing
${}|_{\not\Relbar\joinrel\mathrel{|}{s}}$:
${\\{\bigvee\bar{\varphi}\mid\bar{\varphi}\in\text{collect}_{\not\Relbar\joinrel\mathrel{|}}(r,s)\text{
and }\bigvee\bar{\varphi}\in S\\}}$ Implementing
${}|_{\sqsubseteq{\bigvee\bar{\psi}}}$:
$\\{\bigvee\bar{\varphi}\mid\bar{\varphi}\in\text{collect}_{\sqsubseteq}(r,\bar{\psi})\text{
and }\bigvee\bar{\varphi}\in S\\}$ Recursive functions: collect($(L,M)$) =
$\\{\epsilon\\}\cup\\{\langle{\varphi}\rangle+\bar{\varphi}\mid\varphi\in
L,\bar{\varphi}\in\text{collect}(M[\varphi])\\}$ collect／=|($(L,M),s$) =