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

TL;DR

This paper formalizes a decision procedure for univariate real arithmetic in Isabelle/HOL, ensuring correctness and leveraging parallelism, based on the BKR algorithm which efficiently computes consistent sign assignments for polynomials.

Contribution

It provides a formal proof of the BKR decision procedure for univariate real arithmetic within Isabelle/HOL, extending existing libraries and enabling verified reasoning.

Findings

Formal proof of BKR algorithm in Isabelle/HOL

Efficient handling of sign assignments for polynomials

Enhanced Isabelle/HOL libraries for algebra and analysis

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.