Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Sturm's Theorem (and proof meth...


view this post on Zulip Email Gateway (Aug 19 2022 at 13:31):

From: Tobias Nipkow <nipkow@in.tum.de>
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


Last updated: Apr 25 2024 at 01:08 UTC