[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Book: "Theorem Proving with the Real Numbers"
- To: email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org, email@example.com, firstname.lastname@example.org
- Subject: Book: "Theorem Proving with the Real Numbers"
- From: John Harrison <John.Harrison@cl.cam.ac.uk>
- Date: Thu, 24 Sep 1998 23:04:44 +0100
- cc: John.Harrison@cl.cam.ac.uk
(My apologies for multiple copies of this message.)
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
You can conveniently order the book directly from that page.
Theorem Proving with the Real Numbers
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
If people are interested, I can make the rest of the HOL code available
John Harrison (http://www.cl.cam.ac.uk/users/jrh).