Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.14
URN: urn:nbn:de:0030-drops-139099
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13909/
Cordwell, Katherine ; Tan, Yong Kiam ; Platzer, André
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
| pdf-format: |
|
Abstract
We formalize the univariate fragment of Ben-Or, Kozen, and Reif’s (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR’s algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a follow-up work by Renegar that are well-suited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL’s libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed.
BibTeX - Entry
@InProceedings{cordwell_et_al:LIPIcs.ITP.2021.14,
author = {Cordwell, Katherine and Tan, Yong Kiam and Platzer, Andr\'{e}},
title = {{A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13909},
URN = {urn:nbn:de:0030-drops-139099},
doi = {10.4230/LIPIcs.ITP.2021.14},
annote = {Keywords: quantifier elimination, matrix, theorem proving, real arithmetic}
}
| Keywords: | quantifier elimination, matrix, theorem proving, real arithmetic | |
| Seminar: | 12th International Conference on Interactive Theorem Proving (ITP 2021) | |
| Issue date: | 2021 | |
| Date of publication: | 21.06.2021 | |
| Supplementary Material: |
Our formalization is available on the Archive of Formal Proofs (AFP). Model (formal proof development): https://www.isa-afp.org/entries/BenOr_Kozen_Reif.html |
