Skip to main content
SpringerLink
Log in

Theorem Proving with the Real Numbers

  • Book
  • © 1998

Overview

Authors:
  1. John Harrison

    1. New Museums Site, University of Cambridge Computer Laboratory, Cambridge, UK

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • Formal development of classical mathematics using a computer * Combines traditional lines of research in theorem proving and computer algebra * Shows usefulness of real numbers in verification

Part of the book series: Distinguished Dissertations (DISTDISS)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (8 chapters)

  1. Front Matter

    Pages i-xii
    Download chapter PDF

  2. Introduction

    • John Harrison
    Pages 1-11

  3. Constructing the Real Numbers

    • John Harrison
    Pages 13-38

  4. Formalized Analysis

    • John Harrison
    Pages 39-67

  5. Explicit Calculations

    • John Harrison
    Pages 69-86

  6. A Decision Procedure for Real Algebra

    • John Harrison
    Pages 87-114

  7. Computer Algebra Systems

    • John Harrison
    Pages 115-133

  8. Floating Point Verification

    • John Harrison
    Pages 135-154

  9. Conclusions

    • John Harrison
    Pages 155-159

  10. Back Matter

    Pages 161-186
    Download chapter PDF
Back to top

Keywords

About this book

This book discusses the use of the real numbers in theorem proving. Typ­ ically, 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 float­ ing 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 de­ scribe 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.

Authors and Affiliations

  • New Museums Site, University of Cambridge Computer Laboratory, Cambridge, UK

    John Harrison

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation