The BKR Decision Procedure for Univariate Real Arithmetic (Q7361604)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry BenOr_Kozen_Reif
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | The BKR Decision Procedure for Univariate Real Arithmetic |
AFP entry BenOr_Kozen_Reif |
Statements
24 April 2021
0 references
Katherine Kosaian
0 references
Yong Kiam Tan
0 references
André Platzer
0 references
The BKR Decision Procedure for Univariate Real Arithmetic (English)
0 references
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.
0 references
