Skip to main content
SpringerLink
Log in

Philosophical Aspects of Computerized Verification of Mathematics

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1397))

  • 327 Accesses

Abstract

This invited lecture discusses various philosophical aspects of computerized verification of mathematics. Particular attention is given to the influences of type-theoretical verification systems. The paper is halfway between a full paper and an extended abstract. The reason is that an extensive text of a very similar lecture (Venice, 1995) is to be published in [7].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N.G. de Bruijn, A survey of the project Automath. In: To H.B. Curry: Essays in combinatory logic, lambda calculus and formalism, ed. J.P. Seldin and J.R. Hindley, Academic Press 1980, pp. 579–606. Reprinted in: Nederpelt [8].

    Google Scholar 

  2. N.G. de Bruijn, Checking mathematics with computer assistance. In Notices American Mathematical Society, vol 38(1), Jan. 1991, pp 8–15.

    Google Scholar 

  3. N.G. de Bruijn, Formalization of constructivity in Automath. In: Geuvers, J.H. and de Vrijer, R.C. (editors), Selected Papers on Automath, Studies in Logic, vol. 133. North-Holland 1994 Nederpelt [8].

    Google Scholar 

  4. N.G. de Bruijn, The Mathematical Vernacular, a language for mathematics with typed sets. In: Geuvers, J.H. and de Vrijer, R.C. (editors), Selected Papers on Automath, Studies in Logic, vol. 133. North-Holland 1994 Nederpelt [8].

    Google Scholar 

  5. N.G. de Bruijn, On the roles of types in mathematics. In: The Curry-Howard Isomorphism, ed. Ph. de Groote. Cahiers du Centre de Logique, vol. 8, pp. 27–54. Academia, Louvain-la-Neuve (Belgique) 1995.

    Google Scholar 

  6. N.G. de Bruijn, Reflections on Automath. In: Geuvers, J.H. and de Vrijer, R.C. (editors), Selected Papers on Automath, Studies in Logic, vol. 133. North-Holland 1994 Nederpelt [8].

    Google Scholar 

  7. N.G. de Bruijn, Type-theoretical checking and philosophy of mathematics. In: “Twenty-Five Years of Constructive Type Theory”, to be published by Oxford University Press.

    Google Scholar 

  8. Nederpelt, R.P., Geuvers, J.H. and de Vrijer, R.C. (editors), Selected Papers on Automath, Studies in Logic, vol. 133. North-Holland 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computing Science, Eindhoven University of Technology, PO Box 513, 5600MB, Eindhoven, The Netherlands

    N. G. de Bruijn

Authors
  1. N. G. de Bruijn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Bruijn, N.G. (1998). Philosophical Aspects of Computerized Verification of Mathematics. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64406-4

  • Online ISBN: 978-3-540-69778-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation