I am undertaking the task of formalizing Interval Newton Methods in Isabelle. To the best of my knowledge this hasn't been formalized in other proof assistants or theorem provers. However, I want to confirm this impression with you.

The methods I'm talking about are as described in Chapter 8 of Introduction to Interval Analysis. The idea would be to start verifying a one-dimensional version (reusing theories already present in Isabelle) and then extending it into a multivariate setting.

The most similar thing I have found come from ENS of Lyon where they have developed Gappa and produced this Phd thesis. But the first is a generic tool for floating points numbers and the second only deals with interval Newton methods collateraly.

Is there any reference you're aware of that provides a formalization of Interval Newton Methods in a proof assistant or theorem prover?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.