Talk:Presburger arithmetic

has at least a runtime of 2^(2^(cn)) for some constant c. Here, n is the length of the Presburger statement. Hence, the problem is one of the few that provably need more than polynomial run time.

You mean more than polynomial or more than exponential ? --Taw

Both. But "polynomial time" P is a pretty important class of problems, and this is one of the few problems that can be shown not to be in there, so that's why I explicitly mentioned polynomial time. --AxelBoldt

I know just a little of mathematics but I don't see clearly the meaning of the last theorem... ? x ? y : ( (? z : x + z = y + 1) ? (? z : ¬ (((1 + y) + 1) + z = x) ) ) May be the last part of it is " = z + x " instead of " + z = x ". --jimmer_lactic