Theorem Proving with the Real Numbers – John Harrison | buch7 – Der soziale Buchhandel
Bitte warten ...
icon suche icon merkliste icon warenkorb
Blick ins Buch

Theorem Proving with the Real Numbers

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.

Taschenbuch 11/2011
kostenloser Standardversand in DE gewöhnlich ca. 4-5 Werktage (Print on Demand)

Die angegebenen Lieferzeiten beziehen sich auf den Paketversand und sofortige Zahlung (z.B. Zahlung per Lastschrift, PayPal oder Sofortüberweisung).
Der kostenlose Standardversand (2-5 Werktage) benötigt in der Regel länger als der kostenpflichtige Paketversand (1-2 Werktage). Sonderfälle, die zu längeren Lieferzeiten führen können (Bsp: Bemerkung für Kundenservice, Zahlung per Vorkasse oder Sendung ins Ausland) haben wir hier für Sie detailliert beschrieben.

Spenden icon Dank Ihres Kaufes spendet buch7 ca. 4,31 € bis 8,00 €.

Die hier angegebene Schätzung beruht auf dem durchschnittlichen Fördervolumen der letzten Monate und Jahre. Über die Vergabe und den Umfang der finanziellen Unterstützung entscheidet das Gremium von buch7.de.

Die genaue Höhe hängt von der aktuellen Geschäftsentwicklung ab. Natürlich wollen wir so viele Projekte wie möglich unterstützen.

Den tatsächlichen Umfang der Förderungen sowie die Empfänger sehen Sie auf unserer Startseite rechts oben, mehr Details finden Sie hier.

Weitere Informationen zu unserer Kostenstruktur finden Sie hier.

Inhaltsverzeichnis

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.

Produktdetails

EAN / 13-stellige ISBN 978-1447115939
10-stellige ISBN 1447115937
Verlag Springer London
Sprache Englisch
Anmerkungen zur Auflage Softcover reprint of the original 1st ed. 1998
Editionsform Hardcover / Softcover / Karten
Einbandart Taschenbuch
Erscheinungsdatum 20. November 2011
Seitenzahl 200
Beilage Paperback
Format (L×B×H) 23,5cm × 15,5cm × 1,1cm
Gewicht 312g
Warengruppe des Lieferanten Naturwissenschaften - Informatik, EDV
Mehrwertsteuer 5% (im angegebenen Preis enthalten)
Bestseller aus dieser Kategorie

Naturwissenschaften - Informatik, EDV

Noch nicht das passende gefunden?
Verschenken Sie einfach einen Gutschein.

Auch hier werden natürlich 75% des Gewinns gespendet.

Gutschein kaufen

Was unsere Kunden sagen:

Impressum Datenschutz Hilfe / FAQ