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

### Abstract

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.

### License

### History

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