John Harrison.
PhD thesis, University of Cambridge. Published as Technical Report 408 by the
University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street,
Cambridge CB2 3QG, England.

## Abstract:

This thesis discusses the use of the real numbers in theorem proving.
Typically, theorem provers only support a few `discrete' datatypes such as the
natural numbers. However the availability of the real numbers opens up many
interesting and important application areas, such as the verification of
floating point hardware and hybrid systems. It also allows the formalization of
many more branches of classical mathematics, which is particularly relevant for
attempts to inject more rigour into computer algebra systems.
Our work is conducted in a version of the HOL theorem prover. We describe the
rigorous definitional construction of the real numbers, using a new version of
Cantor's method, and the formalization of a significant portion of real
analysis. We also describe an advanced derived decision procedure for the
`Tarski subset' of real algebra as well as some more modest but practically
useful tools for automating explicit calculations and routine linear arithmetic
reasoning.

Finally, we consider in more detail two interesting application areas. We
discuss the desirability of combining the rigour of theorem provers with the
power and convenience of computer algebra systems, and explain a method we have
used in practice to achieve this. We then move on to the verification of
floating point hardware. After a careful discussion of possible correctness
specifications, we report on two case studies, one involving a transcendental
function.

We aim to show that a theory of real numbers is useful in practice and
interesting in theory, and that the `LCF style' of theorem proving is well
suited to the kind of work we describe. We hope also to convince the reader
that the kind of mathematics needed for applications is well within the
abilities of current theorem proving technology.

**For copyright reasons, this thesis is no longer available
electronically. A slightly revised version is now published as a book:**

**
**

** Theorem Proving with the Real Numbers
John Harrison
Springer-Verlag, 1998
ISBN 3-540-762566-6
**

## Bibtex entry:

@BOOK{harrison-thesis,
author = "John Harrison",
title = "Theorem Proving with the Real Numbers",
publisher = "Springer-Verlag",
year = 1998}