A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL by Katherine Kosaian π§, Yong Kiam Tan π§ and AndrΓ© Platzer π§ Dec 15
Verified Quadratic Virtual Substitution for Real Arithmetic by Matias Scharager π§, Katherine Kosaian π§, Stefan Mitsch π§ and AndrΓ© Platzer π§ Oct 02
The BKR Decision Procedure for Univariate Real Arithmetic by Katherine Kosaian π, Yong Kiam Tan π and AndrΓ© Platzer π Apr 24