=Paper=
{{Paper
|id=Vol-1617/paper6
|storemode=property
|title=Reasoning with Sets and Sums of Sets
|pdfUrl=https://ceur-ws.org/Vol-1617/paper6.pdf
|volume=Vol-1617
|authors=Markus Bender
|dblpUrl=https://dblp.org/rec/conf/cade/Bender16
}}
==Reasoning with Sets and Sums of Sets==
https://ceur-ws.org/Vol-1617/paper6.pdf
Reasoning with Sets and Sums of Sets
Markus Bender
Universität Koblenz-Landau, Koblenz, Germany
mbender@uni-koblenz.de
Abstract
In this paper we introduce a decision procedure for the combined theory of sets, arithmetic and
sums of sets, that can be used as abstraction for problems in verification.
This theory and the developed decision procedures is also the first step in our path to develop
decision procedures for more theories that can be used as abstraction in more situations, for example
with the additional bridging functions min, max or measures.
1 Introduction
Verification of real world systems often incorporates decision procedures for different data structures.
To reason with these structures there are mainly two different approaches: one can extend an already
existing calculus and appropriate tools to deal with these structures in a native way, or one can try to find
an abstraction for these structures where there are already well established calculi and good tool support
for the chosen abstraction. Using the combined theory of sets, arithmetic and cardinalities has proven to
be a useful abstraction in many verification areas and there are multiple decision procedures based on it
for example by Ohlbach ([8]) and Kuncak et al. ([6, 10, 9, 12, 7]). We extend this theory in our approach.
Related Work There are many contributions in the area of reasoning with sets and cardinalities. In
addition to the work by Ohlbach ([8]) and by Kuncak and his collaborators ([6, 10, 9, 12, 7]) we want to
mention the following: In [4] the authors offer a different way of reasoning with sets, cardinalities and
arithmetic: They consider reasoning techniques for unions of non-disjoint theories where at least one
of the theories is P-gentle. This property allows to use the Nelson-Oppen procedure for reasoning in
combinations of non-disjoint theories. The authors identify the Löwenheim and Bernays-Schönfinkel-
Ramsey classes to be P-gentle which allows reasoning with sets and cardinalities.
In [11] Calogero G. Zarba introduces the language 2LSC (two-level syllogistic with cardinality) that
allows to reason about problems with sets, cardinality of sets, the elements of the sets and cardinal
numbers. A decision procedure for quantifier-free formulae in 2LSC is presented. It is inspired by the
Nelson-Oppen method and uses decision procedures for cardinal linear arithmetic and for the theory of
the elements of the sets as black boxes. As with the Nelson-Oppen method, the theories must be stably-
infinite, but there is no need for disjoint signatures, making the introduced method usable for 2LSC.
The authors of [1] identify two fragments of Presburger arithmetic with counting quantifiers and
uninterpreted function symbols, namely extended flat formulae and simply flat formulae. They show that
both fragments are decidable and establish bounds on the complexity of deciding the satisfiability of
formulae in these fragments.
Contributions In this paper we extend the results in [6] and propose a method that allows us to reason
about sets, arithmetic, cardinalities and sums of sets, which offers the possibility to be used as abstraction
in more cases. The shown method is also a starting point for an extension that gives even more flexibility
by introducing additional bridging functions like the minimal or maximal element of a set or measures.
These are current examples in our goal of finding properties and methods that allow us to construct a
framework for reasoning with sets, arithmetic and other bridging functions. Our method terminates and
has the same worst case complexity as the approach by Kuncak et al. [6].
Structure In Section 2 we introduce the preliminaries needed for our method. Section 3 then shows our
method and gives information about its properties. We conclude this paper in Section 4 by elaborating
the different kinds of extensions that are possible for this method and by summarizing the paper.
Reasoning with Sets and Sums of Sets Markus Bender
2 Preliminaries
2.1 Syntax
Let S = {nat, num, set} be a set of sorts, where nat is the sort of natural numbers, num is the so called
element sort and set is the sort of sets with elements of sort num. The sort nat is essentially only
introduced to express cardinalities of sets. Thus, we do not distinguish between nat and num for most of
our considerations. The following sets of function and predicate symbols
Ωcnum := {K | K a constant of sort nat or num with fixed semantics}
Ωcset := / U}
{0,
Ωnum := Ωcnum ∪ {+ : num × num → num, · : num × num → num}
Ωset := Ωcset ∪ {∪ : set × set → set, ∩ : set × set → set, { : set → set}
Ωsum := {card : set → nat} ∪ {sum : set → num}
Πnum := {≈num : num × num, < : num × num}
Πset := {≈set : set × set, ⊆ : set × set}
are used to define the following four signatures that are used throughout this paper:
Σsum := ({nat, num, set}, Ωnum ∪ Ωset ∪ Ωsum , Πnum ∪ Πset )
Σarith := ({nat, num}, Ωnum , Πnum )
The symbols in Ωcnum denote numbers and for the symbols in Ωcset , 0/ denotes the empty set and
U denotes the universal set. We sometimes use x instead of {x to denote the complement of a set
and in cases where the meaning is unambiguous, ≈ instead of ≈num , respectively ≈set . We introduce
the following constants with the given meaning as syntactic sugar: MAXC := card(U ) of sort nat and
MAXS := sum(U ) of sort num.
Let X = (X nat , X num , X set ) be a countably infinite many-sorted set of variables, where X nat ,
X num , and X set are sets of variables of sort nat, num and set respectively. If not stated otherwise, x, xi , y
denote variables of sort set, called set variables, k, ki , l, li , s, si denote variables of sort nat or num, called
arithmetical variables, v, vi denote set and arithmetical variables, and A, Ai denote any set expression,
where i is any index. We use ≤, ≥, >, ⊂, ⊇, ⊃ and 6≈ with the usual meaning.
Please note that this syntax explicitly allows to express constraints between terms of sort nat and
num like ∀ x sum(x) < 2card(x) or, a bit more subtle, ∀ x1 sum(x0 ) < 0 ∧ ((x1 ⊆ x0 ∧ card(x1 ) ≈ 1) →
sum(x1 ) > 0).
2.2 Semantics
We consider Σsum -structures of the form A := (N, F, ΩA , ΠA ), where
• N is the set of natural numbers that is only used as the codomain for the function card.
• F ⊆ R is a set of numbers that is closed under addition and multiplication, called element support
(of the structure). It is used as domain for the symbols in Πnum , as domain and codomain for the
symbols in Ωnum , and as the codomain for sum. Arithmetical variables are assigned values in F.
The finite power set of F, P f (F), is used as domain for card, sum and for the symbols in Πset .
Additionally it is used as domain and codomain for the symbols in Ωset and set variables are
assigned values in P f (F).
• For every function symbol f ∈ (Ωnum ∪ Ωset ∪ Ωsum ∪ Ωmin ), ΩA contains a function fA that
defines the semantics of the function symbol. The semantics for the symbols in Ωnum and Ωset are
as expected. The semantics for the symbols in Ωsum ∪ Ωmin are defined below.
• ΠA defines the semantics for the predicate symbols in Πnum ∪ Πset , which is as expected.
Reasoning with Sets and Sums of Sets Markus Bender
As with the sort nat, the support N is essentially only introduced to make sure, that the codomain of card
is a non-negative integer. Thus, we do not distinguish between N and F for most of our considerations.
The fact, that we consider P f (F) as domain for sets implies that we are only considering finite sets. If
not stated otherwise, c, ci denote elements of N, d, di , e, ei denote elements of F and o, oi denote elements
of P f (F), where i is any index.
The constant U has a special meaning for our approach as its interpretation, U A , is a finite subset
of F that defines the scope of interest. Thus we first introduce the following semantics considering U
and afterwards the general semantics of the bridging functions for o ∈ P f (F):
• U A ∈ P f (F),
• MAXCA = cardA (U A ) := |U A |, the number of elements in U A ,
• MAXSA = sumA (U A ) := ∑ e,
e∈U A
• cardA (o) := |o|, the number of elements in the set o,
• sumA (o) := ∑ e.
e∈o
Let o ∈ P f (F), then {A o := {e | e ∈ U A and e 6∈ o}. In cases where no ambiguity can arise, we
slightly abuse our notation by using A to denote the structure as well as the sorted supports of the
structure. Let β → A be a function assigning values to variables according of their sort that consists
of βnat : X nat → N, βnum : X num → F and βset : X set → P f (F). For βset we impose the additional
condition, that its codomain is P(U A ).
To reflect that U A is our scope of interest we impose the following: In the case of universal quan-
tification of a set variable, ∀ x p(x), is true, if and only if pA (o) is true for all o ∈ P(U A ) instead of
all o ∈ P f (F). In the case of existential quantification of a set variable, ∃ x p(x), is true, if and only if
pA (o) is true for at least one o ∈ P(U A ) instead of at least one o ∈ P f (F).
The semantics for the predicate and function symbols are fixed like this throughout the whole docu-
ment. Therefore, only F may differ between different Σsum -structures.
Σarith -structures are defined accordingly. To extend a Σarith -structure to a Σsum -structure, the fixed
semantics for the additional symbols need to be added.
2.3 Theories
We use the well known theories of linear arithmetic and sets. The theory of sums of sets is defined by the
axioms in Section 3 and the theory we consider is the union of these three theories. Whenever we talk
about satisfiability, we mean it in the sense of “satisfiable modulo the according background theory”.
2.4 Atomic Decompositions
The concept of atomic sets and atomic decompositions was introduced by Ohlbach in [8] and used under
the name of cubes by Kuncak et al. in [5]. Instead of giving a formal definition, we just give an intuition
with help of Example 2.1. For n set variables, there are 2n mutually disjoint regions in the Venn diagram
that can be described as an intersection with n participating expressions, where each of this expressions
is either a set variable or the complement of a set variable. These regions are called atomic sets. Every
set variable can be described as union of atomic sets. This union is called atomic decomposition.
If not stated otherwise, S , S i denote atomic sets, where i is any index.
If all set expressions in a formula are represented as atomic decompositions, the formula is called
set-atomic . Let S be the set of all atomic sets in a given formula and let T be a set such that 0/ ⊂ T ⊆ S.
Reasoning with Sets and Sums of Sets Markus Bender
x1 ∩ x2 y
x1 ∩ x2 y
x1 ∩ x2 x1 ∩ x2 x∩y x∩y
(a) The four atomic sets and the atomic decompositions (b) The general intuition of Lemma 2.2.
for the two sets x1 and x2 of Example 2.1.
Figure 1
Example 2.1. For a formula with exactly two set variables, x1 and x2 there are the following atomic sets:
S 00 := x1 ∩ x2 , S 01 := x1 ∩ x2 , S 10 := x1 ∩ x2 , S 11 := x1 ∩ x2 and these atomic decompositions:
x1 := S 10 ∪ S 11 = (x1 ∩ x2 ) ∪ (x1 ∩ x2 ), x2 := S 01 ∪ S 11 = (x1 ∩ x2 ) ∪ (x1 ∩ x2 ). This is depicted in
Figure 1a.
2.5 Boolean Algebra and Presburger Arithmetic (BAPA)
As our approach is based on the work of Kuncak et al. [6] we give a short overview of their method. In
Kuncak et al.’s approach [6] for solving constraints on sets and constraints on cardinalities a sentence in
BAPA is given and then transformed to an equisatisfiable sentence containing only Presburger arithmetic.
This transformation can roughly be summarized as follows:
replacing A1 ≈set A2 with A1 ⊆ A2 ∧ A2 ⊆ A1
1. Represent set atoms as arithmetical atoms by first
and then replacing A1 ⊆ A2 with card A1 ∩ A2 ≈ 0 for all set expressions A1 , A2 .
2. Represent every set expression as an atomic decomposition,
3. Use Lemma 2.2 for removing set quantifiers.
Lemma 2.2 ([6]). Let x1 , . . . , xn be finite disjoint sets and l1 , . . . , ln , k1 , . . . , kn be natural numbers. Then
the following two statements are equivalent:
n
1. ∃ y card(xi ∩ y) = ki ∧ card(xi ∩ y) = li , where y is a finite set.
V
i=1
n
V
2. card(xi ) = ki + li .
i=1
Figure 1b depicts the idea of Lemma 2.2. Lemma 2.2 introduces only a way of removing existentially
quantified set variables, but we can use ∀ x F ≡ ¬∃ x ¬F to remove universally quantified set variables.
We use the term original formula to refer to the input formula of the procedure and transformed
formula to refer to the output of the procedure.
The satisfiability of the transformed formula, and therefore the satisfiability of the original formula,
can then be decided by using a solver for Presburger arithmetic. This can always be done, as Kuncak
et al. [6] are only interested in the cardinality of sets, and do not impose additional constraints on the
elements. Thus, if the cardinalities are known, the assignment for the atomic sets can be done in a rather
simple way: Select an arbitrary element from the support, which has not yet been used, and assign it
to the set. Repeat selecting and assigning elements until the number of elements in the set is equal to
the value for the cardinality of the set. Proceed in this way until the assignment for all atomic sets is
fixed. This way of deciding BAPA formulae is sound and complete and the result of the transformation
is illustrated for a simple input in Example 2.3
Reasoning with Sets and Sums of Sets Markus Bender
Example 2.3. The sentence F 0 is the result of transforming the BAPA-sentence F = ∀ x ∀ y ∃ k (x ⊆ y →
card(x) + k ≈ card(y)) to an equisatisfiable formula that is pure arithmetic using the method by [6].
0
F = ∀ l0 ∀ l1 MAXC ≈ l0 + l1 → ∀ l00 , l01 , l10 , l11 l0 ≈ l00 + l01 ∧ l0 ≈ l10 + l11 → (1)
∃ k (l10 ≈ 0 → l10 + l11 + k ≈ l01 + l11 ) (2)
3 Reasoning with Sums of Sets
We show how to extend the method in [6] to deal with the following two extensions:
1. allow formulae with an arbitrary combination of quantified and free variables,
2. introduce the new bridging function sum, returning the sum of all elements of a set.
With the additional bridging function, our goal is to still use a prover for arithmetic, that has no know-
ledge of the background theories of the bridging functions to decide satisfiability for a given formula.
Thus we extend Kuncak et al.’s algorithm [6] in such a way, that is is able to transform a given formula
that contains sum, into a formula of pure arithmetic. In contrast to [6] we do not necessarily end up
with Presburger arithmetic, but depending on the element support of the chosen structure in different
arithmetical fragments. However, we keep BAPA as part of the name for our approach, namely we talk
about the theory BAPAS .
To encode some information of the background theory in the resulting arithmetical formula and
therefore prevent the generation of models for the transformed formula that cannot be used to generate
a model for the original formula, we add the following axioms during the transformation: To model the
property that sum(0)
/ = 0, we enrich the original formula by adding
card(S ) ≈ 0 → sum(S ) ≈ 0 (SumEmpty)
for all S ∈ S. Additionally, we add
card(S 1 ) ≈ 1 ∧ card(S 2 ) ≈ 1 → sum(S 1 ) 6≈ sum(S 2 ) (UniqueSingleton)
for all S 1 , S 2 ∈ S with S 1 6= S 2 .
Let F be a formula in BAPAS , then AxS (F) is the conjunction of the instances of SumEmpty for all
S ∈ S and the instances of UniqueSingleton for all S 1 , S 2 ∈ S with S 1 6= S 2 .
Although the enrichment of the formula is at the end of the transformation, i.e. the axioms are added
as pure arithmetical formulae, we show the axioms in their original form, i.e. containing sets and bridging
functions, as this presentation is clearer and easier to comprehend.
Depending on the choice of the element support F, the original formula and the transformed formula
are not always equisatisfiable, even with the additional axioms. This is implied by the fact that sum
and its background theory not only impose constraints on the number of elements of the sets, but on the
elements as well, i.e. it is not sufficient to use arbitrary distinct elements of the domain as elements for
the atomic sets, but we need to find elements that have certain properties. We identified a property of
the element support which we name sum constructive (see Definition 3.3) for which we can show that
the original formula and the transformed formula are always equisatisfiable. Intuitively it states that the
element support F has the following property: There are infinitely many distinct ways to represent each
element in F as sum of two distinct elements in F.
The following steps are executed to transform a given formula in BAPAS to a formula in pure arith-
metic:
Reasoning with Sets and Sums of Sets Markus Bender
1. Eliminate ≈set by replacing A1 ≈set A2 with A1 ⊆ A2 ∧ A2 ⊆ A1 .
2. Eliminate ⊆ by replacing A1 ⊆ A2 with card A1 ∩ A2 ≈ 0.
3. Represent every set expression as an atomic decomposition.
4. Distribute card by replacing instances whose argument is a union of atomic sets with the sum of
the appropriate atomic instances i.e. card( S ∈T S ) ∑S ∈T card(S ), and purify by introducing
S
new nat-variables for instances of card.
5. Distribute sum by replacing instances whose argument is a union of atomic sets with the sum of
the appropriate atomic instances i.e. sum( S ∈T S ) ∑S ∈T sum(S ), and purify by introducing
S
new num-variables for the atomic instances of sum.
6. Eliminate quantifiers from inside out and add the instances of the axioms SumEmpty for all S ∈ S
and UniqueSingleton S 1 , S 2 ∈ S with S 1 6= S 2 .
The method that transforms a formula applying steps 1 to 4 is called α pre and α pre (F) denotes the
result of applying α pre on a formula F. α pre is identical to the first part of the approach described in [6].
Please note that after α pre is applied to a formula F, α pre (F) is set-atomic and set expressions appear
only as argument of bridging functions. Additionally we know that all instances of card are atomic
instances and due to the purification only occur as kind of prefix of the original formula. The method
that transforms a formula applying steps 1 to 6 is called α S . α S (F) denotes the result of applying α S on
a formula F.
Step 6, from now on denoted α Q S depends on the total number of set variables and the number and
type of quantification of quantified set variables. Its core component is the iterative removal of existential
and universal set quantifiers by using an extension of Lemma 2.2. In the following, we do not explicitly
use the duality ∀ x F ≡ ¬∃ x ¬F to rewrite the formula accordingly, but we do an additional rewrite step
to remove the negation symbol. Thus the type of the set quantifier under consideration just determines
which junctor and which type of quantifier is used while building the resulting formulae. Some details
on α QS are given in Definition 3.1 and Example 3.2 illustrates its use.
Definition 3.1. α Q 0
S is defined as follows: Let F be a formula in prenex normal form in BAPAS . The
0
formula F is derived from F by applying α pre , and then distribute sum and purify according to step 5.
Further let n denote the number of distinct set variables in F 0 , q the number of set quantifiers in F 0 and r
the number of all quantifiers in F 0 . Further, let m = 2n .
Due to the fact that F is the result of applying first α pre and then step 5 of α S , we know that F has
the following form
F = Q1 v1 . . . Qr vr G, where
m
^ m
^
G = ∃ ln,1 . . . ln,m ∃ sn,1 . . . sn,m card(S n,i ) ≈ ln,i ∧ sum(S n,i ) ≈ sn,i ∧ H
i=1 i=1
and that H does not contain any set expressions.
1. If q = 0, i.e. F contains only free set variables:
This implies that there are no quantified set variable. We then add the axioms to the formula
constructed by putting the quantifiers in front of H. We return AxS (F) ∧ Q1 v1 . . . Qr vr H
2. If q > 0, i.e. F contains quantified set variables:
We return the result of α ES ([Q1 v1 , . . . , Qr vr ], n, q, 0, G), where α ES is described below.
Reasoning with Sets and Sums of Sets Markus Bender
Instead of giving a formal definition of α ES , we just give a general intuition on how it works and then
present some of the details with the help of Example 3.2. α ES essentialy picks the quantifier Qr vr out
of the list Q1 v1 , . . . , Qr−1 vr−1 , Qr vr constructs a new formula G0 based on G and some other constraints
and then calls itself recursively with the shortened list Q1 v1 , . . . , Qr−1 vr−1 and the newly constructed
G0 . If the list of quantifiers is empty, the formula G is returned. If vr is an arithmetical variable, G0 :=
Qr vr G, otherwise G0 is constructed from G by using Lemma 2.2, where we use it for constructing
defining hierarchies of sums for card and sum. If not all set variables are quantified, the definition of the
purification for card and sum is removed after the last quantifier on sets is removed.
Example 3.2. Let F0 := ∀ x1 (x0 ⊆ x1 → sum(x0 ) ≈ sum(x0 ∩ x1 )) be a formula in BAPAS . We show
how α S (F0 ) is constructed.
1. Eliminate ≈set , and eliminate ⊆:
≈set does not appear in F0 . The atom x0 ⊆ x1 is rewritten to card(x0 ∩ x1 ) ≈ 0.
Thus we get F1 := ∀ x1 (card(x0 ∩ x1 ) ≈ 0 → sum(x0 ) ≈ sum(x0 ∩ x1 )).
2. Introduce Atomic Decompositions:
The atomic sets in F0 are: S 00 := x0 ∩ x1 , S 01 := x0 ∩ x1 , S 10 := x0 ∩ x1 , S 11 := x0 ∩ x1 . By
making F1 set-atomic, we get F2 := ∀ x1 (card(S 10 ) ≈ 0 → sum(S 10 ∪ S 11 ) ≈ sum(S 11 )).
3. Distribute card, purify card :
The only instance of card in F2 is already an atomic instance, thus we just purify
F3 := ∀ x1 ∃ l00 , l01 , l10 , l11
card(S 00 ) ≈ l00 ∧ · · · ∧ card(S 11 ) ≈ l11 ∧ (l10 ≈ 0 → sum(S 10 ∪ S 11 ) ≈ sum(S 11 ))
After this step, α pre is finished and the formula F3 is set-atomic.
4. Distribute sum, purify sum:
sum(S 10 ∪ S 11 ) ≈ sum(S 11 ) is rewritten to sum(S 10 ) + sum(S 11 ) ≈ sum(S 11 ).
F4 := ∀ x1 ∃ l00 , l01 , l10 , l11 ∃ s00 , s01 , s10 , s11
card(S 00 ) ≈ l00 ∧ · · · ∧ card(S 11 ) ≈ l11 ∧ sum(S 00 ) ≈ s00 ∧ · · · ∧ sum(S 11 ) ≈ s11 ∧
(l10 ≈ 0 → s10 + s11 ≈ s11 )
5. Eliminate Quantifiers (Step 6 in α S ):
Step 1: Call α Q
S (F4 ):
The number of distinct set variables in F1 is n = 2, the number of set quantifiers in F1 is q = 1
and the number of all quantifiers in F1 is r = 1.
As F4 contains quantified variables, we call α ES ([∀ x1 ], 2, 1, 0, G), where
G := ∃ l00 , l01 , l10 , l11 ∃ s00 , s01 , s10 , s11
card(S 00 ) ≈ l00 ∧ · · · ∧ card(S 11 ) ≈ l11 ∧ sum(S 00 ) ≈ s00 ∧ · · · ∧ sum(S 11 ) ≈ s11 ∧
(l10 ≈ 0 → s10 + s11 ≈ s11 )
Thus, we construct G0 as follows and then return the result of α ES ([], 2, 1, 1, G0 ).
G0 := ∀ l00 , l01 , l10 , l11 ∀ s00 , s01 , s10 , s11 (
l0 ≈ l00 + l01 ∧ l1 ≈ l10 + l11 ∧ s0 ≈ s00 + s01 ∧ s1 ≈ s10 + s11 ∧ AxS (F)
) → (l10 ≈ 0 → s10 + s11 ≈ s11 )
Reasoning with Sets and Sums of Sets Markus Bender
Some explanations on the construction of G0 :
• As we are considering ∀x1 , the quantifiers ∃ l00 , . . . l11 ∃ s00 , . . . s11 in G are changed to
universal quantifiers and the core formula is connected with →.
• As ∀ x1 is the first set quantifier to be treated, we add the appropriate axioms:
AxS (F) :=
(l01 ≈ 1 ∧ l00 ≈ 1) → (s01 6≈ s00 ) ∧ (l01 ≈ 1 ∧ l10 ≈ 1) → (s01 6≈ s10 ) ∧
(l10 ≈ 1 ∧ l00 ≈ 1) → (s10 6≈ s00 ) ∧ (l11 ≈ 1 ∧ l00 ≈ 1) → (s11 6≈ s00 ) ∧
(l11 ≈ 1 ∧ l01 ≈ 1) → (s11 6≈ s01 ) ∧ (l11 ≈ 1 ∧ l10 ≈ 1) → (s11 6≈ s10 ) ∧
(l00 ≈ 0 → s00 ≈ 0) ∧ (l01 ≈ 0 → s01 ≈ 0) ∧ (l10 ≈ 0 → s10 ≈ 0) ∧ (l11 ≈ 0 → s11 ≈ 0)
• We check if #used = q−1: As 0 = 1−1 = 0, i.e. we are considering the last set quantifier,
we do not add the following definitions of the purification
∃ l0 , l1 ∃ s0 , s1 card(x0 ) ≈ l0 ∧ card(x0 ) ≈ l1 ∧ sum(x0 ) ≈ s0 ∧ sum(x0 ) ≈ s1
to construct G0 from G.
Step 2: Call α ES ([], 2, 1, 1, G0 ): As the list of quantifiers is empty, α ES returns G0 .
F5 := ∀ l00 , l01 , l10 , l11 ∀ s00 , s01 , s10 , s11 ( (3)
l0 ≈ l00 + l01 ∧ l1 ≈ l10 + l11 ∧ s0 ≈ s00 + s01 ∧ s1 ≈ s10 + s11 ∧ (4)
AxS (F)) → (l10 ≈ 0 → s10 + s11 ≈ s11 ) (5)
The formula F5 does not contain any set expression and consists of arithmetical constraints only.
3.1 Properties
Thus with α S we can transform a given formula in BAPAS to a formula in pure arithmetic. The pro-
cess always terminates (Theorem 3.6). We identify a condition (sum constructive (Definition 3.3)) that
guarantees that the original formula and transformed formula are equisatisfiable (Theorem 3.4): We
show that we can construct a model for the original formula from a model for the transformed formula
(Corollary 3.5). We also offer information on the complexity of our method in Theorem 3.7.
We only provide ideas of the following proofs. A document with full proofs is available online1 .
Definition 3.3 (sum constructive). Let A be a Σsum -structure with element support F. F is called
sum constructive if and only if for all c ∈ F there exist infinitely many a, b ∈ F, such that a 6= b and
a + b = c.
If the element support of a structure is sum constructive, we call the structure sum constructive.
A formula is called sum constructive satisfiable if it has a sum constructive model.
Please note that the property sum constructive is only linked to the element support of the structure,
i.e. it does not rely on, or impose anything upon the interpretations of the functions and predicates in
a structure. The property guarantees that it is always possible to construct the missing elements in the
assignments for the set variables, as the transformed formula only provides information on the number
of elements and the sum of all elements for each set. Examples of sets that are sum constructive are Z,
Q and R. Examples of sets that are not sum constructive are N, R+ and any finite set.
1 userpages.uni-koblenz.de/~mbender/sum_full.pdf
Reasoning with Sets and Sums of Sets Markus Bender
Theorem 3.4 (Equisatisfiability for sum constructive structures). For all formulae F in BAPAS , F is
sum constructive satisfiable if and only if α S (F) is sum constructive satisfiable.
Proof. (Idea). The proof is based on how one can use sum constructive model for F to construct a
sum constructive model for α S (F) and vice versa. Transforming a Σsum -structure to an Σarith -structure
and vice versa can be done easily, therefore we focus on how to construct an assignment for the free
variables.
• To use the assignments for sets in F to construct assignments for the arithmetical variables in
α S (F) that correspond to cardinalities and sums of sets can be done straight forward. The property
sum constructive is not really needed for this part of the proof.
• The other way around is only possible if the element sort is sum constructive as we rely on this
property to construct information about the elements of the sets. As we know how many elements
each set has and what the sum of all the elements in a set is, we can use the two values to construct
all the elements of the sets and therefore construct an assignment for a sum constructive-model for
F from a sum constructive-model of α S (F).
Corollary 3.5 (Model Construction). For all formulae F in BAPAS , all sum constructive Σarith -structures
A and all assignments β : X → A , we can construct a Σsum -structure A 0 and an assignment β 0 : X →
A 0 such that, if A , β |= α S (F) then A 0 , β 0 |= F.
Proof. (Idea). This follows from the proof of Theorem 3.4.
Theorem 3.6 (Termination). Let F be a formula in BAPAS and let us assume that we have a prover for
arithmetic that always terminates. Therefore, checking if F is sum constructive satisfiable is decidable.
Proof. (Idea). This follows immediately from the way that α S works, as later steps do not influence
previous steps and all steps are essentially rewriting operations with a bounded number of steps.
Theorem 3.7 (Complexity). Let F be a formula in BAPAS and let size(F) denote the size of the formula
F. The following hold:
1. The size of α S (F) is bounded by O(22size(F) ).
2. The time for the transformation of F to α S (F) is bounded by O(22size(F) ).
3. The number of quantifier alternations in F and α S (F) are identical.
Proof. (Idea). The proofs for these three properties can be done by following the procedure α S and
analyzing how it changes the given formula.
4 Conclusion
We presented a method for reasoning in the combined theory of sets, cardinalities of sets, sums of sets
and arithmetic with an arbitrary mix of quantified and free set variables. This theory is useful as it can
be used as an abstraction for verification tasks. We have shown that our method is sound and complete
and that its complexity is comparable to the approach in [6] which is the basis of our extension.
Additionally, this method offers a good starting point for further extensions. Preliminary results
show that we can lift it to the theory BAPAM which contains sets, arithmetic, cardinalities and the two
bridging functions min and max that return the minimal, respectively the maximal element of a set. There
Reasoning with Sets and Sums of Sets Markus Bender
is already work on sets with constraints on infimum and supremum of sets showing that this fragment
can be useful [7]. BAPAS and BAPAM can be combined in a natural way leading to a broader variety of
possible uses. With those three bridging functions, we hope to see similarities and properties that allow
us to establish a more general method of reasoning with arithmetic, sets, cardinalities and more bridging
functions, to get a language with a higher expressiveness that has established decision procedures and
can be used as abstraction for verification and reasoning tasks.
On a different path, we expect that we can extend this framework to allow for measures as bridging
functions from sets to arithmetic and then from intervals to arithmetic. We want to pursue this direction
to get an decision procedure for intervals and measures. This is a step towards the target of developing a
decision procedure for fragments of the duration calculus ([3, 2]).
The implementation of the presented method α S is an ongoing task.
Acknowledgment: We thank Viorica Sofronie-Stokkermans for her helpful feedback and Matthias
Horbach for many valuable discussions. We are thankful for the constructive comments of the anonym-
ous reviewers, as well.
References
[1] F. Alberti, S. Ghilardi, and E. Pagani. Counting constraints in flat array fragments. CoRR, abs/1602.00458,
2016.
[2] Z. Chaochen and M. R. Hansen. Duration calculus: a formal approach to real-time systems. Springer, Berlin
New York, 2004.
[3] Z. Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Inf. Process. Lett., 40(5):269–276,
1991.
[4] P. Chocron, P. Fontaine, and C. Ringeissen. A gentle non-disjoint combination of satisfiability procedures.
In S. Demri, D. Kapur, and C. Weidenbach, editors, IJCAR 2014, Proceedings, volume 8562 of LNCS, pages
122–136. Springer, 2014.
[5] V. Kuncak, H. H. Nguyen, and M. C. Rinard. An algorithm for deciding BAPA: Boolean algebra with
presburger arithmetic. In R. Nieuwenhuis, editor, CADE-20, Proceedings, volume 3632 of LNCS, pages
260–277. Springer, 2005.
[6] V. Kuncak, H. H. Nguyen, and M. C. Rinard. Deciding boolean algebra with presburger arithmetic. J. Autom.
Reasoning, 36(3):213–239, 2006.
[7] V. Kuncak, R. Piskac, and P. Suter. Ordered sets in the calculus of data structures. In A. Dawar and H. Veith,
editors, CSL 2010, Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 34–48. Springer,
2010.
[8] H. J. Ohlbach. Set description languages and reasoning about numerical features of sets. In P. Lambrix,
A. Borgida, M. Lenzerini, R. Möller, and P. F. Patel-Schneider, editors, International Workshop on Descrip-
tion Logics (DL’99), Proceedings, volume 22 of CEUR Workshop Proceedings. CEUR-WS.org, 1999.
[9] T. Wies, R. Piskac, and V. Kuncak. Combining theories with shared set operations. In S. Ghilardi and
R. Sebastiani, editors, FroCoS 2009, Proceedings, volume 5749 of LNCS, pages 366–382. Springer, 2009.
[10] K. Yessenov, R. Piskac, and V. Kuncak. Collections, cardinalities, and relations. In G. Barthe and M. V.
Hermenegildo, editors, VMCAI 2010, Proceedings, volume 5944 of LNCS, pages 380–395. Springer, 2010.
[11] C. G. Zarba. Combining sets with cardinals. J. Autom. Reasoning, 34(1):1–29, 2005.
[12] K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In R. Gupta and
S. P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language
Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 349–361. ACM, 2008.