# A 22 2 pnupper bound on the complexity of Presburger Arithmetic

- Authors
- Journal
- Journal of Computer and System Sciences 0022-0000
- Publisher
- Elsevier
- Publication Date
- Volume
- 16
- Issue
- 3
- Identifiers
- DOI: 10.1016/0022-0000(78)90021-1
- Disciplines

## Abstract

Abstract The decision problem for the theory of integers under addition, or “Presburger Arithmetic,” is proved to be elementary recursive in the sense of Kalmar. More precisely, it is proved that a quantifier elimination decision procedure for this theory due to Cooper determines, for any n, the truth of any sentence of length n within deterministic time 2 2 2 pn for some constant p > 1. This upper bound is approximately one exponential higher than the best known lower bound on nondeterministic time. Since it seems to cost one exponential to simulate a nondeterministic algorithm with a deterministic one, it may not be possible to significantly improve either bound.

## There are no comments yet on this publication. Be the first to share your thoughts.