Seminár z teoretickej informatiky - Marek Košta

v piatok 21.4.2017 o 11:00 hod. v miestnosti M/213

18. 04. 2017 18.28 hod.
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.