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



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