Linear integer arithmetic, also known as Presburger arithmetic, is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by fixed integers. Sets of natural numbers that can be defined in this logic are ultimately periodic sets. More generally, these are semi-linear sets, introduced in the 1960s by Parikh.
This talk will introduce Presburger arithmetic and three methods for deciding whether a given sentence in it is true. These methods are rooted in geometry, automata theory, and symbolic computation, respectively. We will also discuss how these methods and ideas extend to other arithmetic theories and other problems (including some recent research results).