Skip to main content
SpringerLink
Log in

An approach to theorem proving on the basis of a typed lambda-calculus

  • Thursday Morning
  • Conference paper
  • First Online:
5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980 (CADE 1980)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 87))

Included in the following conference series:

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N.G. de Bruijn, The mathematical language AUTOMATH, its usage and some of its extensions, Symposium on Automatic Demonstration, IRIA, Versailles, France, 1968. (Lecture notes in Mathematics, Vol. 125, pp. 29–61, Springer-Verlag, Berlin, 1970.)

    Google Scholar 

  2. N.G. de Brujin, AUTOMATH, a language for mathematics, Lecture Notes prepared by B. Fawcett, Les Presses de l'Université de Montréal, Canada, 1973.

    Google Scholar 

  3. D.T. van Daalen, A description of AUTOMATH and some aspects of its language theory, Proceedings of the Symposium APLASM, Vol. I, ed. P. Braffort, Orsay, France, 1973.

    Google Scholar 

  4. D.T. van Daalen, The language theory of Automath, doctoral dissertation, Technol. University Eindhoven, The Netherlands, 1980.

    Google Scholar 

  5. L.S. van Benhtem Jutting, Checking Landau's "Grundlagen" in the AUTOMATH system, doctoral dissertation, Technol. University Eindhoven, The Netherlands, 1977. (Mathematical Centre Tracts 83, Amsterdam, The Netherlands, 1979.)

    Google Scholar 

  6. R.P. Nederpelt, Strong normalization in a typed lambda calculus with lambda structured types, doctoral dissertation, Technol. University Eindhoven, The Netherlands, 1973.

    Google Scholar 

  7. R.P. Nederpelt, Presentation of natural deduction, Recueil des Travaux de l'Institut Mathématique, Nouvelle série, tome 2 (10), p. 115–126, Symposium: Set Theory, Foundations of Mathematics, Beograd, Jugo-Slavia, 1977.

    Google Scholar 

  8. J. Zucker, Formalization of classical mathematics in AUTOMATH, Actes of the International Logic Colloquium, Clermont-Ferrand, France, 1975.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Technology, Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    R. P. Nederpelt

Authors
  1. R. P. Nederpelt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wolfgang Bibel Robert Kowalski

Rights and permissions

Reprints and permissions

Copyright information

© 1980 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nederpelt, R.P. (1980). An approach to theorem proving on the basis of a typed lambda-calculus. In: Bibel, W., Kowalski, R. (eds) 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. CADE 1980. Lecture Notes in Computer Science, vol 87. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10009-1_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-10009-1_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-10009-6

  • Online ISBN: 978-3-540-38140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation