Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy

preprint2014arXivOpen access

Abstract

It is shown that for any fixed i>0i>0, the Σi+1Σ_{i+1}-fragment of Presburger arithmetic, i.e., its restriction to i+1i+1 quantifier alternations beginning with an existential quantifier, is complete for ΣiEXP\mathsfΣ^{\mathsf{EXP}}_{i}, the ii-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between NEXP\mathsf{NEXP} and EXPSPACE\mathsf{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Σ_1-fragment of Presburger arithmetic: given a Σ1Σ_1-formula Φ(x)Φ(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.

Explore this paper’s authors, topics and related work.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Reviews 0

Write a reviewWrite

No reviews yet.

Discussion 0

Add a commentWrite

No comments yet.