基于BKR算法的一元实数运算的验证决策过程
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
摘要：
我们形式化的单变量片段的本-或，Kozen，和赖夫（BKR）的决定过程中的一阶真正的算术Isabelle/HOL。BKR的算法具有良好的并行性潜力，并被设计用于实践。它的关键见解是一个聪明的递归过程，该过程计算输入的一组单变量多项式的所有一致符号分配的集合，同时仔细管理中间步骤，以避免天真地枚举所有可能的符号分配的指数爆炸（这种见解对于单变量情况和一般情况都是基本的）。我们的证明结合了BKR的思想和Renegar的后续工作，非常适合形式化。由此产生的证明大纲使我们能够在Isabelle/HOL的代数、分析和矩阵库的基础上进行大量构建。我们对现有库的主要扩展也有详细说明。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
