The Sturm–Tarski Theorem

Wenda Li 🌐

September 19, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


November 9, 2022
Added theory file Tarski_Query_Impl to the entry proof session.


Session Sturm_Tarski