Real Number Calculations and Theorem Proving

When handling proofs of properties in the real world we often need to assert that one numeric quantity is greater than another. When these numeric quantities are real-valued, it is often tempting to get out the calculator to calculate the values of the expressions and then enter the results directly into the theorem prover as “facts” or axioms, since formally proving the desired properties can often be very tiresome. Obviously, such a procedure poses a few risks.

An alternative approach, presented in this paper, is to prove the correctness of an arbitrarily accurate calculator for the reals. If this calculator is expressed in terms of the underlying integer arithmetic operations of the theorem-prover’s implementation language, then there is a reasonable expectation that a practical evaluator of real-valued expressions may have been constructed.

Obviously, there are some constraints imposed by computability theory. It is well known, for example, that it is not possible to determine the sign of a computable real in finite time. We show that for all practical purposes, we need not worry about such fussy details. After all, mathematicians have – throughout the centuries – been prepared to make such calculations without being overly punctilious about the computability of the operations they were performing!

We report on the experience of validating and using a real number calculator in PVS.