Theorem proving with the real numbers
著者
書誌事項
Theorem proving with the real numbers
（Distinguished dissertations）
Springer, c1998
大学図書館所蔵 件 / 全9件
-
該当する所蔵館はありません
- すべての絞り込み条件を解除する
注記
Includes bibliographical references (p. [169]-183) and index
内容説明・目次
内容説明
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.
目次
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.
「Nielsen BookData」 より