2015/06/30 by Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
Computer Science · Mathematics · #Algebra over a field #Algebraic number #Algorithm #Computation #Computer science #Correctness #Exploit #Formal Methods in Verification #HOL #Logic, programming, and type systems #Mathematics #Multivariate statistics #Polynomial #Polynomial and algebraic computation #Programming language #Pure mathematics #Symbolic computation #Theoretical computer science #Univariate #cs.LO
paper · pdf · doi:10.1007/s10817-017-9424-6
published as Journal of Automated Reasoning, 2017 · 24 pages
openalex publication_date 2017/08/08 · arxiv created 2018/04/10 · arxiv updated 2018/04/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
We present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decomposition. We follow the approach of untrusted certificates, separating solving from verifying: efficient external tools perform expensive real algebraic computations, producing evidence that is formally checked within Isabelle’s logic. This allows us to exploit highly-tuned computer algebra systems like Mathematica to guide our procedure without impacting the correctness of its results. We present experiments demonstrating the efficacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.