scientific article; zbMATH DE number 1064597
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].
- Forcing the truth of a weak form of Schanuel's conjecture
- A note on Schanuel's conjectures for exponential logarithmic power series fields
- On the expressiveness and decidability of o-minimal hybrid systems
- On the decidability of the real field with a generic power function
- scientific article; zbMATH DE number 1169378 (Why is no real title available?)
- A note on the decidability of exponential terms
- THE UNIFORM SCHANUEL CONJECTURE OVER THE REAL NUMBERS
- Embedding the prime model of real exponentiation into o‐minimal exponential fields
- Weighted o-minimal hybrid systems
- Automated tail bound analysis for probabilistic recurrence relations
- On decidability of time-bounded reachability in CTMDPs
- Schanuel's conjecture and the roots of elementary functions
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4355928)
