Super-Exponential Complexity of Presburger Arithmetic

  • Michael J. Fischer
  • Michael O. Rabin
Part of the Texts and Monographs in Symbolic Computation book series (TEXTSMONOGR)


Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic: the first-order theory of the real numbers under addition, and Presburger arithmetic — the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 cn steps. In the case of Presburger arithmetic, the corresponding bound is \({2^{{2^{cn}}}}\). These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized.


Decision Procedure Finite Abelian Group Scanning Head Binary Word Real Addition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag/Wien 1998

Authors and Affiliations

  • Michael J. Fischer
  • Michael O. Rabin

There are no affiliations available

Personalised recommendations