The decision problem for Presburger arithmetic is an interesting example in computational complexity theory and computation. Let "n" be the length of a statement in Presburger arithmetic. Then Fischer and Rabin (1974) proved that, in the worst case, the proof of the statement in first order logic has length at least formula_1, for some constant "c">0. Hence, their decision algorithm for Presburger arithmetic has runtime at least exponential. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of length "n" which have doubly exponential length proofs. Intuitively, this suggests there are computational limits on what can be proven by computer programs. Fischer and Rabin's work also implies that Presburger arithmetic can be used to define formulas which correctly calculate any algorithm as long as the inputs are less than relatively large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for Presburger Arithmetic was proved by Oppen (1978).