In model theory, Tarski's exponential function problem asks whether the theory of the real numbers together with the exponential function is decidable. Alfred Tarski had previously shown that the theory of the real numbers (without the exponential function) is decidable.

The problem

is a structure over the language of ordered rings, with the usual interpretation given to each symbol. It was proved by Tarski that the theory of the real field there is an effective procedure for determining whether

to the language that was interpreted as the exponential function.

Conditional and equivalent results

The problem can be reduced to finding an effective procedure for determining whether any given exponential polynomial. showed that Schanuel's conjecture implies such a procedure exists, and hence gave a conditional solution to Tarski's problem., and indeed, Macintyre and Wilkie proved that only a real version of Schanuel's conjecture is required to imply the decidability of this theory.

Even the real version of Schanuel's conjecture is not a necessary condition is a non-singular solution of the system

.

References