### Abstract

We formalize the univariate case of Ben-Or, Kozen, and Reif's
decision procedure for first-order real arithmetic (the BKR
algorithm). We also formalize the univariate case of Renegar's
variation of the BKR algorithm. The two formalizations differ
mathematically in minor ways (that have significant impact on the
multivariate case), but are quite similar in proof structure. Both
rely on sign-determination (finding the set of consistent sign
assignments for a set of polynomials). The method used for
sign-determination is similar to Tarski's original quantifier
elimination algorithm (it stores key information in a matrix
equation), but with a reduction step to keep complexity low.

BSD License