Affordable Access

Publisher Website

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
  • Computer Science
  • Mathematics

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.