[isabelle] New AFP entry: The Sturm-Tarski Theorem



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!




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.