Presburger Arithmetic is the sub-category of First Order Logic, which deals with quantification over Integers, with addition, order relation, and multiplication and divisibility by constants. Our goal is to decide the truth value of sentence of Presburger Arithmetic by eliminating the quantifiers.
Source: Derek C. Oppen, A $2^{2^{2^{pn}}}$ Upper Bound on the Complexity of Presburger Arithmetic, 323-332, Journal of Computer and System Sciences, 1978.
https://www.sciencedirect.com/science/article/pii/0022000078900211
