License: Creative Commons Attribution 4.0 International 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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13909/
Go to the corresponding LIPIcs Volume Portal

Cordwell, Katherine ; Tan, Yong Kiam ; Platzer, André

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

pdf-format:
LIPIcs-ITP-2021-14.pdf (1 MB)

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
Collection: 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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI