# The Sturm-Tarski Theorem

 Title: The Sturm-Tarski Theorem Author: Wenda Li Submission date: 2014-09-19 Abstract: We have formalized the Sturm-Tarski theorem (also referred as the Tarski theorem), which generalizes Sturm's theorem. Sturm's theorem is usually used as a way to count distinct real roots, while the Sturm-Tarksi theorem forms the basis for Tarski's classic quantifier elimination for real closed field. BibTeX: @article{Sturm_Tarski-AFP, author = {Wenda Li}, title = {The Sturm-Tarski Theorem}, journal = {Archive of Formal Proofs}, month = sep, year = 2014, note = {\url{https://isa-afp.org/entries/Sturm_Tarski.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: BenOr_Kozen_Reif, Budan_Fourier, Count_Complex_Roots, Winding_Number_Eval Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.