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