Theorem proving with the real numbers
Author(s)
Bibliographic Information
Theorem proving with the real numbers
（Distinguished dissertations）
Springer, c1998
Available at / 9 libraries
-
No Libraries matched.
- Remove all filters.
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"