Page "Presburger arithmetic" Paragraph 20

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 any decision algorithm for Presburger arithmetic has a worst-case runtime of at least, for some constant c > 0.

Hence, the decision problem for Presburger arithmetic is an example of a decision problem that has been proved to require more than exponential run time.

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 means 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 ).