Applications of quantifier elimination (Matyas Sustik, speaker):

I will introduce the concept of quantifier elimination (also called
variable elimination) techniques/algorithms.  Then we will discuss
three of the many application areas where the method has been
successfully used: geometry theorem proving, proving decidability
results and the design and analysis of various control systems and
feedback systems.  Finally we could discuss how these procedures may
benefit ACL2, how quantifier elimination might be used in
verification?