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', 'Yong Kiam Tan', 'André 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', 'Steve Zdancewic']},
	publisher = {ACM},
	year = {2023},
	isbn = {9798400700262},
	address = {New York},
	doi = {10.1145/3573105.3575672}
}