Cylindrical decomposition : a way to solve 1st order logic of the real numbers

Add to your list(s) Download to your calendar using vCal

• Mathieu Huot (University of Cambridge)
• Friday 24 June 2016, 11:15-12:15
• Rainbow Room (FS07), Computer Laboratory.

If you have a question about this talk, please contact Ian Orton.

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.

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

• Logic & Semantics for Dummies
• Rainbow Room (FS07), Computer Laboratory
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.