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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Modular First Formalisation of Combinatorial Design Theory Kapitel lesen Erstes Kapitel lesen

2021 | OriginalPaper | Buchkapitel

Beautiful Formalizations in Isabelle/Naproche

verfasst von : Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Erik Sturzenhecker

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present short example formalizations of basic theorems from number theory, set theory, and lattice theory which ship with the new \(\mathbbm {N}\)aproche component in Isabelle 2021. The natural proof assistant \(\mathbbm {N}\)aproche accepts input texts in the mathematical controlled natural language ForTheL. Some ForTheL texts that proof-check in \(\mathbbm {N}\)aproche come close to ordinary mathematical writing. The formalization examples demonstrate the potential to write mathematics in a natural yet completely formal language and to delegate tedious organisatorial details and obvious proof steps to strong automated theorem proving so that mathematical ideas and the “beauty” of proofs become visible.

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 A Modular First Formalisation of Combinatorial Design Theory
Nächstes Kapitel Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
Literatur
1.
Cramer, M.: Proof-checking mathematical texts in controlled natural language. PhD thesis, University of Bonn (2013)
2.
3.
Frerix, S., Koepke, P.: Automatic proof-checking of ordinary mathematical texts. In: Proceedings of the Workshop Formal Mathematics for Mathematicians (2018)
4.
5.
Hersh, R.: What is Mathematics, Really?. Oxford University Press, Oxford (1997)
6.
Inglis, M., Aberdein, A.: Beauty is not simplicity: an analysis of mathematicians’ proof appraisals. Philosophia Math. 23, 87–109 (2014)MathSciNetCrossRef
7.
Isabelle contributors. The Isabelle 2021 release (February 2021)
8.
Knaster, B., Tarski, A.: Un théorème sur les fonctions d’ensembles. Annales de la Société Polonaise de Mathématique 6, 133–134 (1928)MATH
9.
Koepke, P.: Textbook mathematics in the Naproche-SAD system. In: Joint Proceedings of the FMM and LML Workshops (2019)
10.
König, J.: Mathematische Annalen. Zum Kontinuumsproblem 60, 177–180 (1905)
11.
Kühlwein, D., Cramer, M., Koepke, P., Schröder, B.: The Naproche system (2009)
12.
Ziegler, G.M., Aigner, M.: Proofs from THE BOOK. 4th edition, Springer, Berlin (2009)
13.
McAllister, J.W.: Mathematical beauty and the evolution of the standards of mathematical proof. In: Emmer, M. (ed) The Visual Mind II, pp. 15–34. MIT Press, Cambridge (2005)
14.
15.
Paskevich, A.: Méthodes de formalisation des connaissances et des raisonnements mathématiques: aspects appliqués et théoriques. PhD thesis, Université Paris (12, 2007)
16.
Paskevich, A.: The syntax and semantics of the ForTheL language (2007)
17.
Paulson, L.C.: Alexandria: Large-scale formal proof for the working mathematician (2018)
18.
19.
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)MathSciNetCrossRef
20.
21.
Verchinine, K., Lyaletski, A., Paskevich, A., Anisimov, A.: On correctness of mathematical texts from a logical and practical point of view. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 583–598. Springer, Heidelberg (2008). https://​doi.​org/​10.​1007/​978-3-540-85110-3_​47CrossRef
22.
Metadaten
Titel
Beautiful Formalizations in Isabelle/Naproche
verfasst von
Adrian De Lon
Peter Koepke
Anton Lorenzen
Adrian Marti
Marcel Schütz
Erik Sturzenhecker
Copyright-Jahr
2021
Buch
Intelligent Computer Mathematics

Print ISBN: 978-3-030-81096-2

Electronic ISBN: 978-3-030-81097-9

Copyright-Jahr: 2021

DOI
https://doi.org/10.1007/978-3-030-81097-9_2

Premium Partner

    Bildnachweise