Skip to main content
SpringerLink
Log in

Building theories in Nuprl

  • Conference paper
  • First Online:
Logic at Botik '89 (Logic at Botik 1989)

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

Included in the following conference series:

Abstract

This paper provides an account of how mathematical knowledge is represented, reasoned about, and used computationally in a mechanized constructive theorem proving environment. We accomplish this by presenting a particular theory developed in the Nuprl proof development system: finite set theory culminating in Ramsey's theorem. We believe that this development is interesting as a case study in the relationship between constructive mathematics and computer science. Moreover, the aspects we emphasize — the high-level development of definitions and lemmas, the use of tactics to automate reasoning, and the use of type theory as a programming logic — are not restricted in relevance to this particular theory, and indicate the promise of our approach for other branches of constructive mathematics.

This research was supported in part by NSF grants CCR8502243 and DCR8303327.

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. David A. Basin. Building theories in Nuprl. Technical Report 88-932, Cornell University, 1988.

    Google Scholar 

  2. David A. Basin. An environment for automated reasoning about partial functions. In 9th International Conference On Automated Deduction, pages 101–110, Argonne, Illinois, 1988.

    Google Scholar 

  3. Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979.

    Google Scholar 

  4. N. G. de Bruijn. A survey of the project AUTOMATH. In Essays in Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.

    Google Scholar 

  5. W.R. Cleaveland II. Type-Theoretic Models of Concurrency. PhD thesis, Cornell, 1987.

    Google Scholar 

  6. R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

    Google Scholar 

  7. R.L. Constable, Knoblock T., and J Bates. Writing programs that construct proofs. Journal of Automated Reasoning, 1(3):285–326, 1985.

    Google Scholar 

  8. Thierry Coquand and Gérard Huet. Constructions: A higher order proof system for mechanizing mathematics. In B. Buchberger, editor, EUROCAL '85: European Conference on Computer Algebra, pages 151–184. Springer-Verlag, 1985.

    Google Scholar 

  9. Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In 9th International Conference On Automated Deduction, Argonne, Illinois, 1988.

    Google Scholar 

  10. A. Ferro et al. Decision procedures for elementary fragments of set theory. In Fifth Conference on Automated Deduction, Les Arcs, France, 1980.

    Google Scholar 

  11. Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    Google Scholar 

  12. Ronald L. Graham, Bruce L. Rothschild, and Joel H. Spencer. Ramsey Theory. John Wiley & Sons, 1980.

    Google Scholar 

  13. Douglas J. Howe. Implementing number theory: An experiment with Nuprl. In 8th International Conference On Automated Deduction, Oxford, UK, 1986.

    Google Scholar 

  14. Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.

    Google Scholar 

  15. Christoph Kreitz. Constructive automata theory implemented with the Nuprl proof development system. Technical Report 86-779, Cornell University, 1986.

    Google Scholar 

  16. Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, Amsterdam, 1982. North Holland.

    Google Scholar 

  17. David A. McAllester. ONTIC: A knowledge representation system for mathematics. Technical Report 979, MIT, 1987.

    Google Scholar 

  18. Lawrence Paulson. Lessons learned from LCF: a survey of natural deduction proofs. Comp. J., 28(5), 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853, Ithaca, NY

    David A. Basin

Authors
  1. David A. Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Albert R. Meyer Michael A. Taitslin

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Basin, D.A. (1989). Building theories in Nuprl. In: Meyer, A.R., Taitslin, M.A. (eds) Logic at Botik '89. Logic at Botik 1989. Lecture Notes in Computer Science, vol 363. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51237-3_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-51237-3_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51237-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation