A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL by Katherine Cordwell 📧, Yong Kiam Tan 📧 and André Platzer 📧 Dec 15
The BKR Decision Procedure for Univariate Real Arithmetic by Katherine Cordwell 🌐, Yong Kiam Tan 🌐 and André Platzer 🌐 Apr 24