### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Session BenOr_Kozen_Reif

- More_Matrix
- BKR_Algorithm
- Matrix_Equation_Construction
- BKR_Proofs
- BKR_Decision
- Renegar_Algorithm
- Renegar_Proofs
- Renegar_Decision

### Depends on

- Algebraic Numbers in Isabelle/HOL
- The Sturm–Tarski Theorem

### Used by

- Hardness of Lattice Problems
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Fisher’s Inequality: Linear Algebraic Proof Techniques for Combinatorics

## Cite

×

BenOr_Kozen_Reif-AFP

    @article{BenOr_Kozen_Reif-AFP,
      author  = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
      title   = {The BKR Decision Procedure for Univariate Real Arithmetic},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/BenOr_Kozen_Reif.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Apr 25, 2021 : Isabelle2021