
Accession Number : AD0775004
Title : SuperExponential Complexity of Presburger Arithmetic.
Descriptive Note : Technical memo.,
Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE PROJECT MAC
Personal Author(s) : Fischer,Michael J. ; Rabin,Michael O.
Report Date : FEB 1974
Pagination or Media Count : 27
Abstract : 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 (nondeterministic) 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)
Descriptors : *Mathematical logic, *Addition, Groups(Mathematics), Number theory, Algorithms, Theorems
Subject Categories : Theoretical Mathematics
Distribution Statement : APPROVED FOR PUBLIC RELEASE