|14:00 — 14:05||— Introduction —|
|14:05 — 15:20||James Worrell: On the first-order theory of real exponentiation (part 1)|
|15:20 — 15:30||— Discussion —|
|15:30 — 15:50||— Break —|
|15:50 — 17:05||James Worrell: On the first-order theory of real exponentiation (part 2)|
|17:05 — 17:25||— Discussion —|
We give a tutorial overview of the result of MacIntyre and Wilkie that the first-order theory of the reals with exponentiation is decidable assuming Schanuel's Conjecture. In the first half of the talk we describe the decision procedure for the existential fragment of the logic. The second half of the talk deals with effective model completeness, allowing us to reduce the general decision problem to the existential fragment.