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:	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.