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.
2 2.1
Let S = fnat; num; setg 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 := fK j K a constant of sort nat or num with fixed semanticsg cset := f0/ ; U g num := cnum [ f+ : num num ! num; : num num ! numg set := cset [ f[ : set set ! set; \ : set set ! set; { : set ! setg sum := fcard : set ! natg [ fsum : set ! numg num := f num : num num; < : num numg set := f set : set set; : set setg are used to define the following four signatures that are used throughout this paper: sum := (fnat; num; setg; arith := (fnat; numg; num [ set [ sum; num; num [ set ) 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 8 x sum(x) < 2card(x) or, a bit more subtle, 8 x1 sum(x0) < 0 ^ ((x1 x0 ^ card(x1) 1) ! sum(x1) > 0). 2.2
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 2 ( 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. 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 2 P f (F):
U A 2 P f (F), MAXCA = cardA (U A ) := jU A j, the number of elements in U A , MAXSA = sumA (U A ) := å e,
e2U A cardA (o) := joj, the number of elements in the set o, sumA (o) := å e.
e2o Let o 2 P f (F), then {A o := fe j e 2 U A and e 62 og. 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 b ! A be a function assigning values to variables according of their sort that consists of bnat : X nat ! N, bnum : X num ! F and bset : X set ! P f (F). For bset 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 quantification of a set variable, 8 x p(x), is true, if and only if pA (o) is true for all o 2 P(U A ) instead of all o 2 P f (F). In the case of existential quantification of a set variable, 9 x p(x), is true, if and only if pA (o) is true for at least one o 2 P(U A ) instead of at least one o 2 P f (F).
The semantics for the predicate and function symbols are fixed like this throughout the whole document. 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
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
The concept of atomic sets and atomic decompositions was introduced by Ohlbach in [
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. x1 \ x2 x1 \ x2 x1 \ x2 x1 \ x2 y x \ y y x \ y (a) The four atomic sets and the atomic decompositions for the two sets x1 and x2 of Example 2.1.
(b) The general intuition of Lemma 2.2.
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.
As our approach is based on the work of Kuncak et al. [
i=1 n 2. V 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 8 x F :9 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. [
We show how to extend the method in [
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 2 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 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 2 S and the instances of UniqueSingleton for all S 1; S 2 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 arithmetic:
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(SS 2T S ) åS 2T card(S ), and purify by introducing 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(SS 2T S ) åS 2T sum(S ), and purify by introducing 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 2 S and UniqueSingleton S 1; S 2 2 S with S 1 6= S 2.
The method that transforms a formula applying steps 1 to 4 is called apre and apre(F) denotes the
result of applying apre on a formula F. apre is identical to the first part of the approach described in [
Step 6, from now on denoted aSQ 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 8 x F :9 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 aSQ are given in Definition 3.1 and Example 3.2 illustrates its use.
Definition 3.1. aSQ is defined as follows: Let F0 be a formula in prenex normal form in BAPAS. The formula F is derived from F0 by applying apre, and then distribute sum and purify according to step 5. Further let n denote the number of distinct set variables in F0, q the number of set quantifiers in F0 and r the number of all quantifiers in F0. Further, let m = 2n.
Due to the fact that F is the result of applying first apre and then step 5 of aS, we know that F has the following form
F = Q1 v1 : : : Qr vr G; where G = 9 ln;1 : : : ln;m
9 sn;1 : : : sn;m and that H does not contain any set expressions.
1. If q = 0, i.e. F contains only free set variables: m ^ card(S n;i) i=1
m ln;i ^ ^ sum(S n;i) i=1 sn;i ^ H 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 aSE([Q1 v1; : : : ; Qr vr]; n; q; 0; G), where aSE is described below. Example 3.2. Let F0 := 8 x1 (x0 how a S(F0) is constructed.
set , and eliminate
: Instead of giving a formal definition of a E, we just give a general intuition on how it works and then
S present some of the details with the help of Example 3.2. a SE 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. x1 ! sum(x0)
sum(x0 \ x1)) be a formula in BAPAS. We show set does not appear in F0. The atom x0 x1 is rewritten to card(x0 \ x1) 0.
Thus we get F1 := 8 x1 (card(x0 \ x1) 0 ! sum(x0) sum(x0 \ x1)).
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 := 8 x1 (card(S 10) 0 ! sum(S 10 [ S 11) sum(S 11)).
The only instance of card in F2 is already an atomic instance, thus we just purify F3 := 8 x1 9 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, a pre is finished and the formula F3 is set-atomic.
sum(S 10 [ S 11)
sum(S 11) is rewritten to sum(S 10) + sum(S 11) (l10
l00 ^ 0 ! s10 + s11 s11) F4 := 8 x1 9 l00; l01; l10; l11 9 s00; s01; s10; s11 card(S 00) ^ card(S 11) l11 ^ sum(S 00) sum(S 11). s00 ^ ^ sum(S 11) s11 ^
Step 1: Call a Q(F4):
S 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 a SE([8 x1]; 2; 1; 0; G), where (l10
l00 ^ 0 ! s10 + s11 G := 9 l00; l01; l10; l11 card(S 00) 9 s00; s01; s10; s11 ^ card(S 11) s11) l11 ^ sum(S 00) s00 ^ ^ sum(S 11) s11 ^ Thus, we construct G0 as follows and then return the result of a SE([]; 2; 1; 1; G0).
As we are considering 8x1, the quantifiers 9 l00; : : : l11 9 s00; : : : s11 in G are changed to universal quantifiers and the core formula is connected with !.
As 8 x1 is the first set quantifier to be treated, we add the appropriate axioms:
AxS(F) := (l01 (l10 (l11 (l00 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 9 l0; l1 9 s0; s1card(x0) l0 ^ card(x0) l1 ^ sum(x0) s0 ^ sum(x0) s1 to construct G0 from G.
Step 2: Call aSE([]; 2; 1; 1; G0): As the list of quantifiers is empty, aSE returns G0.
F5 := 8 l00; l01; l10; l11 8 s00; s01; s10; s11( l0 l00 + l01 ^ l1 l10 + l11 ^ s0 AxS(F)) ! (l10 0 ! s10 + s11 The formula F5 does not contain any set expression and consists of arithmetical constraints only. 3.1
Thus with aS we can transform a given formula in BAPAS to a formula in pure arithmetic. The process 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 2 F there exist infinitely many a; b 2 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.
1userpages.uni-koblenz.de/~mbender/sum_full.pdf Theorem 3.4 (Equisatisfiability for sum constructive structures). For all formulae F in BAPAS, F is sum constructive satisfiable if and only if aS(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 aS(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 aS(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 aS(F).
Corollary 3.5 (Model Construction). For all formulae F in BAPAS, all sum constructive arith-structures A and all assignments b : X ! A , we can construct a sum-structure A 0 and an assignment b 0 : X ! A 0 such that, if A ; b j= aS(F) then A 0; b 0 j= 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 aS 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 aS(F) is bounded by O(22size(F)). 2. The time for the transformation of F to aS(F) is bounded by O(22size(F)).
3. The number of quantifier alternations in F and aS(F) are identical.
Proof. (Idea). The proofs for these three properties can be done by following the procedure aS and analyzing how it changes the given formula. 4
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 [
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
is already work on sets with constraints on infimum and supremum of sets showing that this fragment
can be useful [
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 ([
The implementation of the presented method a 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 anonymous reviewers, as well.