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:
History and Prospects for First-Order Automated Deduction Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

The Lean Theorem Prover (System Description)

verfasst von : Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer

Erschienen in: Automated Deduction - CADE-25

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.

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 Beagle – A Hierarchic Superposition Theorem Prover
Nächstes Kapitel System Description: E.T. 0.1
Fußnoten
Literatur
1.
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011) CrossRef
2.
3.
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C. et al.: The Coq proof assistant reference manual: Version 6.1 (1997)
4.
Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 257–268. ACM (2014)
5.
6.
Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), pp. 50–66. Springer, Berlin (1990)
7.
de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. Preprint (arXiv)
8.
Delahaye, D., Woltzenlogel Paleo, B. (eds.): All about proofs, proofs for all. Mathematical Logic and Foundations, vol. 55 (2015)
9.
10.
Goguen, H.H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 521–540. Springer, Heidelberg (2006) CrossRef
11.
Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009) CrossRef
12.
Martin-Löf, P.: Intuitionistic type theory. Bibliopolis (1984)
13.
McBride, C., Goguen, H.H., McKinna, J.: A few constructions on constructors. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 186–200. Springer, Heidelberg (2006) CrossRef
14.
McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell 2004, pp. 1–9. ACM, New York (2004)
15.
Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)CrossRefMATH
16.
Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
17.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science and Business Media (2002)
18.
Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009) CrossRef
19.
Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
20.
Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–330 (1992)
21.
Slind, K.: Function definition in higher-order logic. In: von Wright, Joakim, Harrison, J., Grundy, John (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996) CrossRef
22.
Streicher, T.: Investigations into intensional type theory. Ph.D. thesis, LMU (1993)
23.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)
24.
Wenzel, M.M.: Isabelle/Isar - a versatile environment for human-readable formal proof documents. Technical report ( 2002)
Metadaten
Titel
The Lean Theorem Prover (System Description)
verfasst von
Leonardo de Moura
Soonho Kong
Jeremy Avigad
Floris van Doorn
Jakob von Raumer
Copyright-Jahr
2015
Buch
Automated Deduction - CADE-25

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

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

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_26