Proving Bounds on Real-Valued Functions with Computations | Zendy

Guillaume Melquiond | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Proving Bounds on Real-Valued Functions with Computations

Author(s) -

Guillaume Melquiond

Publication year - 2008

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/978-3-540-71070-7_2

Subject(s) - mathematical proof , computer science , computation , interval arithmetic , proof assistant , automated theorem proving , interval (graph theory) , computer assisted proof , floating point , formal proof , theoretical computer science , algorithm , calculus (dental) , algebra over a field , programming language , mathematics , pure mathematics , combinatorics , medicine , mathematical analysis , geometry , dentistry , bounded function

International audienceInterval-based methods are commonly used for computing numerical bounds on expressions and proving inequalities on real numbers. Yet they are hardly used in proof assistants, as the large amount of numerical computations they require keeps them out of reach from deductive proof processes. However, evaluating programs inside proofs is an efficient way for reducing the size of proof terms while performing numerous computations. This work shows how programs combining automatic differentiation with floating-point and interval arithmetic can provide some efficient yet guaranteed solvers within the Coq proof system

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research