Accession Number : AD0775004

Title :   Super-Exponential 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 (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)

Descriptors :   *Mathematical logic, *Addition, Groups(Mathematics), Number theory, Algorithms, Theorems

Subject Categories : Theoretical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE