Elementary bounds for presburger arithmetic
Generate an AI Snapshot to get a quick, structured summary of this paper.
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is proved here that there exists a decision procedure for this theory of integers under addition, involving quantifier elimination, for which there is a superexponential upper bound on the size of formula produced when all variables have been eliminated.
Abstract
We consider the first-order theory whose language has as nonlogical symbols the constant symbols 0 and 1, the binary relation symbols = and This theory of integers under addition is commonly called the 'Presburger Arithmetic' and is known to be decidable for truth [Presburger (1929), Hilbert and Bernays (1968)]. We prove here that there exists a decision procedure for this theory, involving quantifier elimination, for which there is a superexponential upper bound on the size of formula produced when all variables have been eliminated.