No label defined (Q4355928)

Let \(T_{\exp}\) be the first-order theory of structure \(R_{\exp}= ({\mathbf R}; +, \cdot, -,0,1, \exp)\), where \({\mathbf R}\) is the field of reals and exp denotes exponentiation . It was a well-known question of Tarski whether \(T_{\exp}\) is decidable; Wilkie proved in 1996 that \(T_{\exp}\) is model complete -- a major step towards answering the question -- and in such a (constructive) manner that the question of decidability of \(T_{\exp}\) is reduced to the question of the decidability of the existential theory, \({\mathcal E}_{\exp}\), of \({\mathbf R}_{\exp}\). Subsequently, Macintyre and Wilkie showed that, assuming the well-known Shanuel's Conjecture in Number Theory, \({\mathcal E}_{\exp}\) is decidable. In this paper Wilkie describes an ``algorithm'' which decides the truth of sentences of \({\mathcal E}_{\exp}\). Of course the algorithm is guaranteed to work only assuming Shanuel's Conjecture. For the entire collection see [Zbl 0868.00035].