Advertisement

Philosophical Aspects of Computerized Verification of Mathematics

  • N. G. de Bruijn
Conference paper
  • 223 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)

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].

Keywords

Mathematical Object Conveyor Belt Natural Deduction Word Group Mathematical Text 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • N. G. de Bruijn
    • 1
  1. 1.Department of Mathematics and Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations