Guaranteed proofs using interval arithmetic

This paper presents a set of tools for mechanical rea-soning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and Taylor’s series expansions. Although the tools are designed for the proof assistant system PVS, expertise on PVS is not required. The ultimate goal of the tools is to provide guaranteed proofs of numerical proper-ties with a minimal human-theorem prover interaction.