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

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We present a formal tool for verification of multivariate nonlinearinequalities. Our verification method is based on interval arithmetic withTaylor approximations. Our tool is implemented in the HOL Light proof assistantand it is capable to verify multivariate nonlinear polynomial andnon-polynomial inequalities on rectangular domains. One of the main features ofour work is an efficient implementation of the verification procedure which canprove non-trivial high-dimensional inequalities in several seconds. Wedeveloped the verification tool as a part of the Flyspeck project (a formalproof of the Kepler conjecture). The Flyspeck project includes about 1000nonlinear inequalities. We successfully tested our method on more than 100Flyspeck inequalities and estimated that the formal verification procedure isabout 3000 times slower than an informal verification method implemented inC++. We also describe future work and prospective optimizations for our method.

Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations