A first complete algorithm for real quantifier elimination in Isabelle/HOL

@INPROCEEDINGS{DBLP:conf/cpp/KosaianTP23,
	study = {https://www.isa-afp.org/entries/Quantifier_Elimination_Hybrid.html},

  author    = {Katherine Kosaian and
               Yong Kiam Tan and
               Andr{\'{e}} Platzer},
  title     = {A First Complete Algorithm for Real Quantifier Elimination in {Isabelle/HOL}},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on
               Certified Programs and Proofs},
  pages     = {211-224},
  editor    = {Brigitte Pientka and
               Steve Zdancewic},
  publisher = {ACM},
  year      = {2023},
  isbn      = {9798400700262},
  address   = {New York},
  doi       = {10.1145/3573105.3575672},
}```