4
$\begingroup$

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?

$\endgroup$

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.