We describe results on decision procedures for sets with cardinalities, as 
well some recent extensions.  These extensions also involve investigations 
of properties of formulas in Presburger arithmetic and integer
 linear programming.