[Prev][Next][Index][Thread]
Book: "Theorem Proving with the Real Numbers"
[While not connected with the contemporary lines of research in type theory,
the following book discusses the formalization of some non-trivial classical
mathematics in simple type theory. It will be of particular relevance to
those interested in mechanized theorem proving, and in how informal
mathematics fits into formal systems.]
People interested in the formalization of mathematics, computer-aided
verification and related fields may like to know that a revised version
of my PhD thesis is now available from Springer-Verlag. The following
information is taken from the publisher's Web page
http://www.springer.co.uk/comp/books/key.html
You can conveniently order the book directly from that page.
Theorem Proving with the Real Numbers
John Harrison
Theorem Proving with the Real Numbers discusses the formal development
of classical mathematics using a computer. It combines traditional
lines of research in theorem proving and computer algebra and shows
the usefulness of real numbers in verification. This book aims to show
that a theory of real numbers is useful in practice as well as
theoretically interesting, and that the 'LCF' style of theorem proving
is well suited to the kind of work described.
CONTENTS: Introduction - Constructing the Real Numbers - Formalized
Analysis - Explicit Calculations - A Decision Procedure for Real
Algebra - Computer Algebra Systems - Floating Point Verification -
Conclusions - Logical Foundations of HOL - Recent Developments -
Bibliography - Index
200 pages 234 x 156mm hardcover 1998 3-540-76256-6 #40.00
Some of the theories described are distributed in the examples directory
of the HOL Light prover, available via the Web page
http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html
If people are interested, I can make the rest of the HOL code available
electronically.
John Harrison (http://www.cl.cam.ac.uk/users/jrh).