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 Plus annual

Presents the access of premium content as premium feature

Premium Content

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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Many problems in computer algebra and numerical analysis can be reduced tocounting or approximating the real roots of a polynomial within an interval.Existing verified root-counting procedures in major proof assistants are mainlybased on the classical Sturm theorem, which only counts distinct roots.  In this paper, we have strengthened the root-counting ability in Isabelle/HOLby first formally proving the Budan-Fourier theorem. Subsequently, based onDescartes' rule of signs and Taylor shift, we have provided a verifiedprocedure to efficiently over-approximate the number of real roots within aninterval, counting multiplicity. For counting multiple roots exactly, we haveextended our previous formalisation of Sturm's theorem. Finally, we combineverified components in the developments above to improve our previous certifiedcomplex-root-counting procedures based on Cauchy indices. We believe thoseverified routines will be crucial for certifying programs and building tactics.

Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem