Super-Exponential Complexity of Presburger Arithmetic.
MASSACHUSETTS INST OF TECH CAMBRIDGE PROJECT MAC
Pagination or Media Count:
Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic the first order theory of the real numbers under addition, and Presburger arithmetic -- the first order theory of addition on the natural numbers. There is a fixed constant c 0 such that for every non-deterministic decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 sup cn steps. In the case of Presburger arithmetic, the corresponding bound is 2 sup 2 sup cn. These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized. Author
- Theoretical Mathematics