Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC