BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cylindrical decomposition : a way to solve 1st order logic of the 
 real numbers  - Mathieu Huot (University of Cambridge)
DTSTART:20160624T101500Z
DTEND:20160624T111500Z
UID:TALK69157@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:I will explain what is exactly 1st order logic of the real num
 bers and\nshow why this is unclear whether it is even decidable.\n\nTarski
  found an algorithm in 1951 but with very (very) high complexity\nand I wi
 ll present Collins' algorithm from 1975\, which is much better.\nThe probl
 em is also shown to be really hard (EXPSPACE difficult...).\n\nI will pres
 ent the algorithm in a semi formal way (formal would require\nseveral hour
 s) to give both the intuition and a few interesting facts\,\nand I will al
 so try to explain why the problem is still interesting\,\ni.e. give some a
 pplications. 
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR