@article{DBLP:journals/jcss/Ben-OrKR86,
  author    = {Michael Ben{-}Or and
               Dexter Kozen and
               John H. Reif},
  title     = {The Complexity of Elementary Algebra and Geometry},
  journal   = {J. Comput. Syst. Sci.},
  volume    = {32},
  number    = {2},
  pages     = {251--264},
  year      = {1986},
  skipurl       = {https://doi.org/10.1016/0022-0000(86)90029-2},
  doi       = {10.1016/0022-0000(86)90029-2},
  timestamp = {Sat, 20 May 2017 00:25:56 +0200},
  biburl    = {https://dblp.org/rec/journals/jcss/Ben-OrKR86.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{Tarski,
  author="Tarski, Alfred",
  title="A Decision Method for Elementary Algebra and Geometry",
  address="Santa Monica, CA",
  year="1951",
  doi="",
  publisher="RAND Corporation",
  url = {https://www.rand.org/pubs/reports/R109.html}
}


@article{DBLP:journals/jsc/Renegar92b,
  author    = {James Renegar},
  title     = {On the Computational Complexity and Geometry of the First-Order Theory
               of the Reals, Part {III:} {Q}uantifier Elimination},
  journal   = {J. Symb. Comput.},
  volume    = {13},
  number    = {3},
  pages     = {329--352},
  year      = {1992},
  skipurl       = {https://doi.org/10.1016/S0747-7171(10)80005-7},
  doi       = {10.1016/S0747-7171(10)80005-7},
  timestamp = {Wed, 17 May 2017 14:25:48 +0200},
  biburl    = {https://dblp.org/rec/journals/jsc/Renegar92b.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{algRAG,
  title={Algorithms in Real Algebraic Geometry},
  author={Saugata Basu and Richard Pollack and Marie-Fran\c{c}oise Roy},
  skipseries={Algorithms and Computation in Mathematics},
  skipvolume={10},
  year={2006},
  publisher={Springer},
  address={Berlin, Heidelberg},
  edition={second},
  doi={10.1007/3-540-33099-2}
}

@article{AssiaQE,
  author    = {Cyril Cohen and
               Assia Mahboubi},
  title     = {Formal proofs in real algebraic geometry: from ordered fields to quantifier
               elimination},
  journal   = {Log. Methods Comput. Sci.},
  volume    = {8},
  number    = {1},
  year      = {2012},
  skipurl       = {https://doi.org/10.2168/LMCS-8(1:2)2012},
  doi       = {10.2168/LMCS-8(1:2)2012},
  timestamp = {Thu, 25 Jun 2020 21:29:12 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1201-3731.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{cohen_phd,
  title =	 {{Formalized algebraic numbers: construction and
                  first-order theory}},
  author =	 {Cohen, Cyril},
  keywords =	 {Coq; Formal proofs; Formalization of mathematics;
                  Small scale reflection; Algebraic numbers;
                  Constructive mathematics; Quantifier elimination;
                  Real numbers},
  language =	 {English},
  affiliation =	 {Laboratoire d'informatique de l'{\'E}cole
                  polytechnique - LIX, INRIA Saclay - Ile de France,
                  Microsoft Research - Inria Joint Centre},
  school =	 {{\'E}cole polytechnique},
  year =	 2012,
  month =	 {{Nov}},
  url =		 {https://perso.crans.org/cohen/papers/thesis.pdf},
}

@unpublished{CyrilReduction,
author = {Cyril Cohen},
title = {Formalization of a sign determination algorithm in real algebraic geometry},
year = {2021},
note = {Preprint on webpage at https://hal.inria.fr/hal-03274013/document}
}

@INPROCEEDINGS{DBLP:conf/cpp/KosaianTP23,
  author    = {Katherine Kosaian and
               Yong Kiam Tan and
               Andr{\'{e}} Platzer},
  title     = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
  booktitle = {CPP},
  pages     = {},
  editor    = {Brigitte Pientka and
               Steve Zdancewic},
  publisher = {ACM},
  year      = {2023},
  isbn      = {},
  address   = {New York},
  doi       = {10.1145/3573105.3575672},
}
