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.

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

BSD License

History

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

Topics

Session Sturm_Tarski

Depends on

Used by

Cite

× 
@article{Sturm_Tarski-AFP,
  author  = {Wenda Li},
  title   = {The Sturm–Tarski Theorem},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Sturm_Tarski.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: