the set of true Σi PA statements with each quantifier block limited to j variables. '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers. PA(1, j) is in P, while PA(1) is NP-complete. For i > 0 and j > 2, PA(i + 1, j) is ΣiP-complete. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block. For i>0, PA(i+1) is ΣiEXP-complete (and is TimeAlternations(2nO(i), i)-complete). Short Presburger Arithmetic () is complete (and thus NP complete for ). Here, 'short' requires bounded (i.e. ) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size). Also, two variable PA (without the restriction of being 'short') is NP-complete. Short (and thus ) PA is in P, and this extends to fixed-dimensional parametric integer linear programming. Applications Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist. For example, the Coq proof assistant system features the tactic omega for Presburger arithmetic and the Isabelle proof assistant contains a verified quantifier elimination procedure by . The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers: describe an automatic theorem prover which uses the simplex algorithm on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recent satisfiability modulo theories solvers use complete integer programming techniques to handle quantifier-free fragment of Presburger arithmetic theory. Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems. This approach is the basis of at least five proof-of-correctness systems for computer programs, beginning with the Stanford Pascal Verifier in the late 1970s and continuing through to Microsoft's Spec# system of 2005. Presburger-definable integer relation Some properties are now given about integer relations definable in Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers. A relation is Presburger-definable if and only if it is a semilinear set. A unary integer relation , that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a threshold and a positive period such that, for all integer such