![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Friday 24 June 2016, 11:15-12:15
Cylindrical decomposition : a way to solve 1st order logic of the real numbers
- 👤 Speaker: Mathieu Huot (University of Cambridge)
- 📅 Date & Time: Friday 24 June 2016, 11:15 - 12:15
- 📍 Venue: Rainbow Room (FS07), Computer Laboratory
Questions? Contact
Ian Orton
Abstract
I will explain what is exactly 1st order logic of the real numbers and show why this is unclear whether it is even decidable.
Tarski found an algorithm in 1951 but with very (very) high complexity and I will present Collins’ algorithm from 1975, which is much better. The problem is also shown to be really hard (EXPSPACE difficult…).
I will present the algorithm in a semi formal way (formal would require several hours) to give both the intuition and a few interesting facts, and I will also try to explain why the problem is still interesting, i.e. give some applications.
Series This talk is part of the Logic & Semantics for Dummies series.
Included in Lists
- Logic & Semantics for Dummies
- Rainbow Room (FS07), Computer Laboratory
- tcw57’s list
- yk373's list
Note: Ex-directory lists are not shown.