Seminár z teoretickej informatiky - Marek Košta
v piatok 21.4.2017 o 11:00 hod. v miestnosti M/213
Od: Rastislav Královič
Prednášajúci: Marek Košta
Názov: Real Quantifier Elimination
Termín: 21.4.2017, 11:00 hod., M/213
In this talk I will discuss the problem of real quantifier elimination from both theoretical and practical points of view. I will first formally introduce the problem and shortly discuss its time complexity. Afterwards I will explain the two most prominent practically applicable methods for real quantifier elimination: (1) Cylindrical Algebraic Decomposition and (2) Virtual Substitution. On the way I will briefly mention some of my results on novel concepts for Virtual Substitution. Finally, I will show how concrete problems can be easily solved by the computer logic system Redlog, which implements various methods for real quantifier elimination.