From: Tobias Nipkow <nipkow@in.tum.de>
The Sturm-Tarski Theorem
Wenda Li
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.
http://afp.sourceforge.net/entries/Sturm_Tarski.shtml
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC