Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Isabelle/HOL Formalisation of Green’s Theorem Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Algebraic Numbers in Isabelle/HOL

verfasst von : René Thiemann, Akihisa Yamada

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, and a faster but approximative version.
To this end, we mechanize several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain. We moreover formalize algorithms for factorization of integer polynomials: Newton interpolation, factorization over the integers, and Kronecker’s factorization algorithm, as well as a factorization oracle via Berlekamp’s algorithm with the Hensel lifting.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Hereditarily Finite Sets in Constructive Type Theory
Nächstes Kapitel Modular Dependent Induction in Coq, Mendler-Style
Fußnoten
2
Here one cannot just evaluate the polynomial on the algebraic point and test the result is 0; we are defining the basic arithmetic operations needed for this evaluation.
 
3
However, we use a faster computer with 3.5 GHz instead of 2.66 GHz.
 
4
We contributed our formalization to the development version of Isabelle (May 2016). There one will find the general “ https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_24/419043_1_En_24_IEq104_HTML.gif ”.
 
5
As for the division algorithm, we have not been able to work with Isabelle’s existing type class for GCDs, as the GCD on polynomials is only available for fields.
 
6
These optimizations became part of the development version of Isabelle (May 2016).
 
7
We thank one of the anonymous reviewers for pointing us to this equality test.
 
8
Note that the quotient type can be in principle defined also directly on top of https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-43144-4_24/419043_1_En_24_IEq210_HTML.gif , such that the quotient and invariant construction is done in one step, but then code generator will fail in Isabelle 2016.
 
Literatur
1.
2.
Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 67–82. Springer, Heidelberg (2012)CrossRef
3.
Cohen, C., Djalal, B.: Formalization of a Newton series representation of polynomials. In: CPP 2016, pp. 100–109. ACM (2016)
4.
Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1:02), 1–40 (2012)MathSciNetMATH
5.
6.
Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: CPP 2015, pp. 75–83. ACM (2015)
7.
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)CrossRef
8.
Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013)CrossRef
9.
Knuth, D.E.: The Art of Computer Programming. Seminumerical Algorithms, vol. 2, 2nd edn. Addison-Wesley, Boston (1981)MATH
10.
Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1–13 (2010)
11.
Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP 2016, pp. 66–75. ACM (2016)
12.
Mahboubi, A.: Proving formally the implementation of an efficient gcd algorithm for polynomials. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 438–452. Springer, Heidelberg (2006)CrossRef
13.
Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)
14.
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
15.
16.
Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: CPP 2016, pp. 88–99. ACM (2016)
Metadaten
Titel
Algebraic Numbers in Isabelle/HOL
verfasst von
René Thiemann
Akihisa Yamada
Copyright-Jahr
2016
Buch
Interactive Theorem Proving

Print ISBN: 978-3-319-43143-7

Electronic ISBN: 978-3-319-43144-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-43144-4_24

Premium Partner

    Bildnachweise