Presburger arithmetic with bounded quantifier alternation

ABSTRACT

This paper concerns both the complexity aspects of PA and the pragmatics of improving algorithms for dealing with restricted subcases of PA for uses such as program verification. We improve the Cooper-Presburger decision procedure and show that the improved version permits us to obtain time and space upper bounds for PA classes restricted to a bounded number of alternations of quantifiers. The improvement is one exponent less than the upper bounds for the decision problem for full PA. The pragmatists not interested in complexity bounds can read the results as substantiation of the intuitive feeling that the improvement to the Cooper-Presburger algorithm is a real, rather than ineffectual, improvement. (It can be easily shown that the bounds obtained here are not achievable using the Cooper-Presburger procedure).

REFERENCES

• 1: Borosh I. and Treybig, L. B. Bounds on positive integral solutions of linear diophantine equations. Proc. AMS 55, March, 1976.
• 2: Cooper, D. C. Theorem-proving in arithmetic without multiplication. Machine Intell. 7, J. Wiley, 1972.
• 3: Ferrante, J. and Rackoff, C. A decision procedure for the first order theory of real addition with order. SIAM J. Comp., March, 1975.
• 4: M. J. Fischer , M. O. Rabin, SUPER-EXPONENTIAL COMPLEXITY OF PRESBURGER ARITHMETIC, Massachusetts Institute of Technology, Cambridge, MA, 1974
• 5: Derek C. Oppen, Elementary bounds for presburger arithmetic, Proceedings of the fifth annual ACM symposium on Theory of computing, p.34-37, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804033]
• 6: Presburger, M. Uber die Vollstandigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Compte-Rendus dei Congres des Math. des pays slavs, Warsaw, 1929.
• 7: Shostak, R. An efficient decision algorithm for arithmetic with function symbols. Talk at Workshop on Auto. Deduction, Aug. 1977.
• 8: Suzuki, N. and Jefferson, D. Verification decidability of Presburger array programs. CMU Comp. Sci. Report,, June, 1977.