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

*To*: coq-club@pauillac.inria.fr, info-hol@leopard.cs.byu.edu, isabelle-users@cl.cam.ac.uk, lics-request@research.bell-labs.com, protagonist@cs.kun.nl, pvs@csl.sri.com, qed@mcs.anl.gov, softverf@leopard.cs.byu.edu, theorem-provers@ai.mit.edu, types@cs.indiana.edu*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 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).

- Prev by Date:
**PVS 2.2 now available on mirror sites** - Next by Date:
**Re: remove** - Prev by thread:
**PVS 2.2 now available on mirror sites** - Next by thread:
**Re: remove** - Index(es):