<div dir="ltr">Dear colleagues, <br><br>on Friday 24 September 2021 (tomorrow) at 17:00 we will have the first talk (see details below) in the Symbolic Computation Istanbul Meetings (SCIM) series.<br><br>For more information about the meetings, please visit <a href="https://alcyon-lab.gitlab.io/lab/scim">https://alcyon-lab.gitlab.io/lab/scim</a><br>To register for SCIM, please visit <a href="https://tinyurl.com/symbolicmeetings">https://tinyurl.com/symbolicmeetings</a><br>The meetings take place in IMBM (<a href="http://www.imbm.org.tr">http://www.imbm.org.tr</a>), but we plan to broadcast in zoom as well. <br>To receive the zoom link, for this talk and future talks, you should register in the form above.<br><br>Students are very welcome to join SCIM. <br>Please let interested parties know about SCIM. <div><br></div><div>Apologies for multiple postings. <br><br>================<br>Speaker: Dr. Madalina Erascu (Faculty of Mathematics & Informatics, West University of Timisoara, Romania)<br>Title: Using Real Quantifier Elimination for Synthesizing Optimal Numerical Algorithms<br>Abstract:<br>Various problems in mathematics, science and engineering can be reduced to real quantifier elimination (quantifier elimination over real closed fields). Around 1930, Alfred Tarski showed that real quantifier elimination can be carried out algorithmically. In 1975, George Collins provided a dramatically more efficient algorithm. Since then, there has been intensive research to make further improvement of efficiency for a certain important class of formulas (inputs). In our research, we consider formulas arising in the synthesis of optimal numerical algorithms. In this talk, we present a case study on the square root problem: given the real number x and the error bound eps, find a real interval such that it contains sqrt(x) and its width is less than eps. As usual, we begin by fixing an algorithm schema, namely, iterative refining: the algorithm starts with an initial interval and repeatedly updates it by applying a refinement function, say R on it until it becomes narrow enough. Then the synthesis amounts to finding a refinement function R that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these can be formulated as quantifier elimination over the real numbers. Hence, in principle, they can be all carried out automatically. However the computational requirement is so huge, making the automatic synthesis practically impossible with the current general quantifier elimination software. Hence, we did some hand derivations and were able to synthesize semi-automatically optimal algorithms under suitable assumptions.<br><br>This is joint work with Hoon Hong.<br>================<br><br>Sincerely, <br>Zafeirakis Zafeirakopoulos<br></div></div>