Email Gateway (Aug 19 2022 at 15:52): Email Gateway (Aug 19 2022 at 15:52):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: Apr 25 2024 at 01:08 UTC