Elementary bounds for presburger arithmetic

ABSTRACT

We consider the first-order theory whose language has as nonlogical symbols the constant symbols 0 and 1, the binary relation symbols &equil; and <, the unary function symbol − and the binary function symbol + 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.

REFERENCES

• 1: Cooper, D.C. (1972). Theorem Proving in Arithmetic without Multiplication. To appear in Machine Intelligence 7.
• 2: Hilbert, D. and Bernays, P. (1968).Grundlagen der Mathematik I. Berlin, Heidelberg, New York: Springer-Verlag.
• 3: Meyer, A. (1972). Weak Monadic Second Order Theory of Successor is Not Elementary Recursive. Unpublished manuscript.
• 4: Presburger, M. (1929). Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Compte-Rendus du I Congres des Mathematiciens des pays Slavs. Warsaw.
• 5: Rabin, M. (1972). Private communication.
• 6: Rabin, M., Fischer, M. and Meyer, A. (1973). Private communications.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
          Subjects: Computer arithmetic

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Alternation and nondeterminism
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Recursive function theory

General Terms:
Theory