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