zbMATH — the first resource for mathematics

A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic. (English) Zbl 0381.03021

03C10 Quantifier elimination, model completeness and related topics
03D15 Complexity of computation (including implicit computational complexity)
03B25 Decidability of theories and sets of sentences
Full Text: DOI
[1] Borosh, I.; Treybig, L.B., Bounds on positive integral solutions of linear Diophantine equations, (), 299-304 · Zbl 0291.10014
[2] Cooper, D.C., Theorem proving in arithmetic without multiplication, Machine intelligence, 7, 91-99, (1972) · Zbl 0258.68046
[3] Ferrante, J.; Rackoff, C., A decision procedure for the first order theory of real addition with order, () · Zbl 0277.02010
[4] Fischer, M.; Rabin, M., Super-exponential complexity of Presburger arithmetic, () · Zbl 0319.68024
[5] Meyer, A., Weak monadic second order theory of successor is not elementary recursive, (1972), manuscript
[6] Presburgbr, M., Über die vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt, Comptes-rendus du ler congres des mathématiciens des pays slavs, (1929)
[7] \scM. Rabin, private communication. 1972.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.