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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

DeepAlgebra - An Outline of a Program

verfasst von : Przemysław Chojecki

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 outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX exploiting syntactic parsers. We describe its application to a repository of human-written facts and definitions in algebraic geometry (The Stacks Project). We use deep learning techniques.

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
Nächstes Kapitel Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
Fußnoten
1
Other standard ITPs include HOL (Light), Isabelle and ACL2.
 
2
Other standard ATPs include Vampyre, Z3 and JProver.
 
3
Partly because of the clear dependancy graph of definitions and theorems used in the Stacks Project, cf. section Hammers.
 
4
Of course ARLT does not necessarily mean mathematics and thus in different scientific disciplines by a dictionary we mean a (semi)-automated way of passing between human-written science and according formal verificators.
 
5
Instead of a diagram we will have a bunch of sentences of the form “\(f: X \rightarrow Y\) is a morphism such that...”.
 
6
To be precise - we need a syntactic parser for syntax analysis; recently Google went open-source with its syntactic parser SyntaxNet and implemented it into TensorFlow [18]; spacy.io builds upon this Natural Language Understanding tool.
 
7
One has to be careful with non-technical terms, but in the worst case they can also be defined as separate Types. The way out is to only start adding new Types/variables once DeepAlgebra finds a “Let ... be” expression or a similar one.
 
8
We should mention also a proof reconstruction module which translates a proof found by an ATP back to an ITP, so that it is accepted formally by an ITP as valid.
 
Literatur
1.
Alemi, A., Chollet, F., Irving, G., Szegedy, C., Urban, J.: DeepMath - deep sequence models for premise selection. arXiv:​1606.​04442
2.
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). doi:10.​1007/​978-3-319-20615-8_​17 CrossRef
3.
4.
Czajka, L., Kaliszyk, C.: Goal translation for a hammer for COQ (Extended Abstract). In: HaTT (2016)
5.
6.
7.
Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39634-2_​14 CrossRef
8.
Hales, T.: Developments in Formal Proofs. Seminaire Bourbaki 1086.abs/1408.6474
9.
Heras, J., Komendantskaya, E.: Proof-pattern search in COQ/SSReflect. In: Proceedings of the 6th COQ workshop (2014)
10.
11.
12.
13.
14.
Schulz, S.: E - A Brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002)MATH
15.
16.
17.
18.
19.
Urban, J., Vyskočil, J.: Theorem proving in large formal mathematics as an emerging AI field. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 240–257. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-36675-8_​13 CrossRef
Metadaten
Titel
DeepAlgebra - An Outline of a Program
verfasst von
Przemysław Chojecki
Copyright-Jahr
2017
Buch
Intelligent Computer Mathematics

Print ISBN: 978-3-319-62074-9

Electronic ISBN: 978-3-319-62075-6

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-62075-6_1