English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR)decision procedure for first-order real arithmetic in Isabelle/HOL. BKR'salgorithm has good potential for parallelism and was designed to be used inpractice. Its key insight is a clever recursive procedure that computes the setof all consistent sign assignments for an input set of univariate polynomialswhile carefully managing intermediate steps to avoid exponential blowup fromnaively enumerating all possible sign assignments (this insight is fundamentalfor both the univariate case and the general case). Our proof combines ideasfrom BKR and a follow-up work by Renegar that are well-suited forformalization. The resulting proof outline allows us to build substantially onIsabelle/HOL's libraries for algebra, analysis, and matrices. Our mainextensions to existing libraries are also detailed.

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