The BKR Decision Procedure for Univariate Real Arithmetic

Title:	The BKR Decision Procedure for Univariate Real Arithmetic
Authors:	Katherine Cordwell, Yong Kiam Tan and André Platzer
Submission date:	2021-04-24
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.
BibTeX:	@article{BenOr_Kozen_Reif-AFP, author = {Katherine Cordwell and Yong Kiam Tan and André Platzer}, title = {The BKR Decision Procedure for Univariate Real Arithmetic}, journal = {Archive of Formal Proofs}, month = apr, year = 2021, note = {\url{https://isa-afp.org/entries/BenOr_Kozen_Reif.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Algebraic_Numbers, Sturm_Tarski
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.