Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
  • Produktbild: Theorem Proving with the Real Numbers
  • Produktbild: Theorem Proving with the Real Numbers

Theorem Proving with the Real Numbers

Aus der Reihe Distinguished Dissertations

Fr. 137.00

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

20.11.2011

Verlag

Springer London

Seitenzahl

186

Maße (L/B/H)

23.5/15.5/1.2 cm

Gewicht

312 g

Auflage

Softcover reprint of the original 1st ed. 1998

Sprache

Englisch

ISBN

978-1-4471-1593-9

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

20.11.2011

Verlag

Springer London

Seitenzahl

186

Maße (L/B/H)

23.5/15.5/1.2 cm

Gewicht

312 g

Auflage

Softcover reprint of the original 1st ed. 1998

Sprache

Englisch

ISBN

978-1-4471-1593-9

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: GPSR Kontakt

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: Theorem Proving with the Real Numbers
  • Produktbild: Theorem Proving with the Real Numbers
  • 1. Introduction.- 1.1 Symbolic computation.- 1.2 Verification.- 1.3 Higher order logic.- 1.4 Theorem proving vs. model checking.- 1.5 Automated vs. interactive theorem proving.- 1.6 The real numbers.- 1.7 Concluding remarks.- 2 Constructing the Real Numbers.- 2.1 Properties of the real numbers.- 2.2 Uniqueness of the real numbers.- 2.3 Constructing the real numbers.- 2.4 Positional expansions.- 2.5 Cantor’s method.- 2.6 Dedekind’s method.- 2.7 What choice?.- 2.8 Lemmas about nearly-multiplicative functions.- 2.9 Details of the construction.- 2.9.1 Equality and ordering.- 2.9.2 Injecting the naturals.- 2.9.3 Addition.- 2.9.4 Multiplication.- 2.9.5 Completeness.- 2.9.6 Multiplicative inverse.- 2.10 Adding negative numbers.- 2.11 Handling equivalence classes.- 2.11.1 Defining a quotient type.- 2.11.2 Lifting operations.- 2.11.3 Lifting theorems.- 2.12 Summary and related work.- 3. Formalized Analysis.- 3.1 The rigorization and formalization of analysis.- 3.2 Some general theories.- 3.2.1 Metric spaces and topologies.- 3.2.2 Convergence nets.- 3.3 Sequences and series.- 3.3.1 Sequences.- 3.3.2 Series.- 3.4 Limits, continuity and differentiation.- 3.4.1 Proof by bisection.- 3.4.2 Some elementary analysis.- 3.4.3 The Caratheodory derivative.- 3.5 Power series and the transcendental functions.- 3.6 Integration.- 3.6.1 The Newton integral.- 3.6.2 The Riemann integral.- 3.6.3 The Lebesgue integral.- 3.6.4 Other integrals.- 3.6.5 The Kurzweil-Henstock gauge integral.- 3.6.6 Formalization in HOL.- 3.7 Summary and related work.- 4. Explicit Calculations.- 4.1 The need for calculation.- 4.2 Calculation with natural numbers.- 4.3 Calculation with integers.- 4.4 Calculation with rationals.- 4.5 Calculation with reals.- 4.5.1 Integers.- 4.5.2 Negation.- 4.5.3 Absolute value.- 4.5.4 Addition.- 4.5.5 Subtraction.- 4.5.6 Multiplication by an integer.- 4.5.7 Division by an integer.- 4.5.8 Finite summations.- 4.5.9 Multiplicative inverse.- 4.5.10 Multiplication of real numbers.- 4.5.11 Thanscendental functions.- 4.5.12 Comparisons.- 4.6 Summary and related work.- 5. A Decision Procedure for Real Algebra.- 5.1 History and theory.- 5.2 Real closed fields.- 5.3 Abstract description of the algorithm.- 5.3.1 Preliminary simplification.- 5.3.2 Reduction in context.- 5.3.3 Degree reduction.- 5.3.4 The main part of the algorithm.- 5.3.5 Reduction of formulas without an equation.- 5.3.6 Reduction of formulas with an equation.- 5.3.7 Reduction of intermediate formulas.- 5.3.8 Proof of termination.- 5.3.9 Comparison with Kreisel and Krivine.- 5.4 The HOL Implementation.- 5.4.1 Polynomial arithmetic.- 5.4.2 Encoding of logical properties.- 5.4.3 HOL versions of reduction theorems.- 5.4.4 Overall arrangement.- 5.5 Optimizing the linear case.- 5.5.1 Presburger arithmetic.- 5.5.2 The universal linear case.- 5.6 Results.- 5.7 Summary and related work.- 6. Computer Algebra Systems.- 6.1 Theorem provers vs. computer algebra systems.- 6.2 Finding and checking.- 6.2.1 Relevance to our topic.- 6.2.2 Relationship to NP problems.- 6.2.3 What must be internalized?.- 6.3 Combining systems.- 6.3.1 Thust.- 6.3.2 Implementation issues.- 6.4 Applications.- 6.4.1 Polynomial operations.- 6.4.2 Differentiation.- 6.4.3 Integration.- 6.4.4 Other examples.- 6.5 Summary and related work.- 7. Floating Point Verification.- 7.1 Motivation.- 7.1.1 Comprehensible specifications.- 7.1.2 Mathematical infrastructure.- 7.2 Floating point error analysis.- 7.3 Specifying floating point operations.- 7.3.1 Round to nearest.- 7.3.2 Bounded relative error.- 7.3.3 Error commensurate with likely input error.- 7.4 Idealized integer and floating point operations.- 7.5 A square root algorithm.- 7.6 A CORDIC natural logarithm algorithm.- 7.7 Summary and related work.- 8. Conclusions.- 8.1 Mathematical contributions.- 8.2 The formalization of mathematics.- 8.3 The LCF approach to theorem proving.- 8.4 Computer algebra systems.- 8.5 Verification applications.- 8.6 Concluding remarks.- A. Logical foundations of HOL.- B. Recent developments.