Verified Quadratic Virtual Substitution for Real Arithmetic
by Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer
André Platzer
2021
The BKR Decision Procedure for Univariate Real Arithmetic
by Katherine Cordwell, Yong Kiam Tan and André Platzer