Sciweavers

TPHOL
2005
IEEE

Real Number Calculations and Theorem Proving

14 years 4 months ago
Real Number Calculations and Theorem Proving
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem proving framework. First, we formally establish upper and lower bounds for trigonometric and transcendental functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations can be performed in an algebraic setting. This pragmatic approach has been implemented as a strategy in PVS. The strategy provides a safe way to perform explicit calculations over real numbers in formal proofs.
César Muñoz, David Lester
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where TPHOL
Authors César Muñoz, David Lester
Comments (0)