[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Book: "Theorem Proving with the Real Numbers"


(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

  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).