[ list |
abstracts |
bib |
http ]

## The First-Order Theory of Sets with Cardinality Constraints is Decidable

paper pdf
paper ps
### Abstract

We show that the decidability of the first-order theory of
the language that combines Boolean algebras of sets of
uninterpreted elements with Presburger arithmetic
operations. We thereby disprove a recent conjecture that
this theory is undecidable. Our language allows relating the
cardinalities of sets to the values of integer variables,
and can distinguish finite and infinite sets. We use
quantifier elimination to show the decidability and obtain
an elementary upper bound on the complexity. Precise
program analyses can use our decidability result to verify
representation invariants of data structures that use an
integer field to represent the number of stored elements.

### Citation

Viktor Kuncak and Martin Rinard.
The first-order theory of sets with cardinality constraints is
decidable.
Technical Report 958, MIT CSAIL, July 2004.
Superseded by
[51].### BibTex Entry

@TECHREPORT{KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable,
author = {Viktor Kuncak and Martin Rinard},
title = {The First-Order Theory of Sets with Cardinality Constraints is Decidable},
institution = {MIT CSAIL},
year = 2004,
number = 958,
month = {July},
url = {http://arxiv.org/abs/cs/0407045},
note = {Superseded by
\cite{KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic}},
localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable.pdf}
}

[ list |
abstracts |
bib |
http ]