Subclasses of Presburger arithmetic and the weak EXP hierarchy

The work

AuthorsChristoph Haase
Typeinproceedings
Year2014
Citekeyhaase2014subclasses

Where it appeared

Published inProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherAssociation for Computing Machinery
Pages1--10

Abstract

It is shown that for any fixed i > 0, the Σi+1-fragment of Presburger arithmetic, i.e., its restriction to i + 1 quantifier alternations beginning with an existential quantifier, is complete for ΣiEXP, the i-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between NEXP and EXPSPACE. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer & Rabin in 1974. Moreover, we apply some of the techniques developed in the proof of the lower bound in order to establish bounds on sets of naturals definable in the Σ1-fragment of Presburger arithmetic: given a Σ1-formula Φ(x), it is shown that the set of non-negative solutions is an ultimately periodic set whose period is at most doubly-exponential and that this bound is tight.

A copy is held

pdf, 568.9 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-14 11:31 UTC

Cite it as

@inproceedings{haase2014subclasses,
  title        = {Subclasses of Presburger arithmetic and the weak EXP hierarchy},
  author       = {Christoph Haase},
  year         = {2014},
  booktitle    = {Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  pages        = {1--10},
  publisher    = {Association for Computing Machinery},
  eprint       = {1401.5266},
  doi          = {10.1145/2603088.2603092},
}

This record lives at https://refs.drheap.org/haase2014subclasses/ and will keep doing so.