# [isabelle] New AFP entry: Sturm's Theorem (and proof method!)

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Sturm's Theorem (and proof method!)
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Sun, 12 Jan 2014 21:45:41 +0100
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Sturm's Theorem
Manuel Eberl
Sturm's Theorem states that polynomial sequences with certain properties,
so-called Sturm sequences, can be used to count the number of real roots of a
real polynomial. This work contains a proof of Sturm's Theorem and code for
constructing Sturm sequences efficiently. It also provides the “sturm” proof
method, which can decide certain statements about the roots of real polynomials,
such as “the polynomial P has exactly n roots in the interval I” or “P(x) > Q(x)
for all x in R”.
http://afp.sourceforge.net/entries/Sturm_Sequences.shtml

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