The BKR Decision Procedure for Univariate Real Arithmetic

Katherine Kosaian 🌐, Yong Kiam Tan 🌐 and André Platzer 🌐

April 24, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Session BenOr_Kozen_Reif