Theorem proving with the real numbers
Author(s)
Bibliographic Information
Theorem proving with the real numbers
(Distinguished dissertations)
Springer, c1998
Available at 9 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
Note
Includes bibliographical references (p. [169]-183) and index
Description and Table of Contents
Description
A discussion of 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.
Table of Contents
Introduction.- Symbolic Computation.- Verification.- Higher Order Logic.- Theorem Proving v Model Checking.- Automated vs Interactive Theorem Proving.- The Real Numbers.- Concluding Remarks.- Constructing the Real Numbers.- Properties of the Real Numbers.- Uniqueness of the Real Numbers.- Constructing the Real Numbers.- Positional Expansions.- Cantor's Method.- Dedekind's Method.- What Choice?- Lemmas about Nearly-Multiplicative Functions.- Details of the Construction.- Adding Negative Numbers.- Handling Equivalence Classes.- Formalized Analysis.- Explicit Calculations.- A Decision Procedure for Real Algebra.- Computer Algebra Systems.- Floating Point Verification.- Conclusions.- Logical Foundations of HOL.- Recent Developments.
by "Nielsen BookData"