Abstract

Presburger arithmetic is the first-order theory of the natural numbers with addition. We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, ifp= are a subset of the free variables in a Presburger formula, we can define a counting functiong to be the number of solutions to the formula, for a givenp. We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. Finally, we translate known computational complexity results into this setting and discuss open directions.