Skip to main content
SpringerLink
Log in

The Nuprl Open Logical Environment

  • Conference paper
Automated Deduction - CADE-17 (CADE 2000)

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

Included in the following conference series:

Abstract

The Nuprl system is a framework for reasoning about mathematics and programming. Over the years its design has been substantially improved to meet the demands of large-scale applications. Nuprl LPE, the newest release, features an open, distributed architecture centered around a flexible knowledge base and supports the cooperation of independent formal tools. This paper gives a brief overview of the system and the objectives that are addressed by its new architecture.

Part of this work was supported by DARPA grant F 30620-98-2-0198.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

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. Aagaard, M., Leeser, M.: Verifying a logic synthesis tool in Nuprl. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663. pp. 72-83. Springer, Heidelberg (1993)

    Google Scholar 

  2. Benzmiiller, C., et al.: Ωmega: Towards a mathematical assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 252–256. Springer, Heidelberg (1997)

    Google Scholar 

  3. Constable, R., et al.: Implemeriting Mathematics with the NuPRL proof development system. Prentice Hall, Englewood Cliffs (1986)

    Google Scholar 

  4. Clavel, M., Duran, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)

    Google Scholar 

  5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 240–243. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Felty, A., Howe, D.: Hybrid Interactive Theorem Proving using Nuprl and HOL. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 351–365. Springer, Heidelberg (1997)

    Google Scholar 

  7. Gordon, M., Melham, T.: Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  8. Howe, D.: Importing mathematics from HOL into NuPRL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267–282. Springer, Heidelberg (1996)

    Google Scholar 

  9. Jackson, P.: The Nuprl Proof Development System. Version 4-2, Department of Computer Science. Cornell University, Ithica (1994)

    Google Scholar 

  10. Kreitz, C., Hayden, M., Hickey, J.: A proof environment for the development of group communication systems. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 317–332. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Kreitz, C.: Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637. Cornell University. Department of Computer Science (1997)

    Google Scholar 

  12. Kreitz, C.: Automated fast-track reconfiguration of group communication systems. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 104–118. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Kreitz, C., Otten, J., Schmitt, S., Pientka, B.: Matrix-based Constructive Theorem Proving. In: Intellectics and Computational Logic. Kluwer, Dordrecht (2000)

    Google Scholar 

  14. Liu, X., Kreitz, C., van Renesse, R., Hickey, J., Hayden, M., Birman, K., Constable, R.: Building reliable, high-performance communication systems from components. SOSP 1999, Operating Systems Review 34(5), 80–92 (1999)

    Article  Google Scholar 

  15. The MathBus Term Structure, http://www.cs.Cornell.edu/simlab/papers/mathbus/mathTerm.htm

  16. Metaprl home page, http://ensembleOl.cs.Cornell.edu:12000/cvsweb/meta-prl

  17. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

    Google Scholar 

  18. Naumov, P.: Publishing formal mathematics on the web. Technical Report TR98-1689. Cornell University. Department of Computer Science (1998)

    Google Scholar 

  19. Naumov, P.: Importing Isabelle formal mathematics into Nuprl. Technical Report TR99-1734. Cornell University. Department of Computer Science (1999)

    Google Scholar 

  20. Owre, S.: PVS: Combining specification, proof checking and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  21. Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361–386. Academic Press, London (1990)

    Google Scholar 

  22. Srinivas, Y.V., Jüllig, R.: SPECWARE: Formal Support for composing software. In Mathematics of Program Construction (1995)

    Google Scholar 

  23. Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison Wesley, Reading (1988)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Stuart F. Allen, Robert L. Constable, Rich Eaton, Christoph Kreitz & Lori Lorigo

Authors
  1. Stuart F. Allen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rich Eaton
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Christoph Kreitz
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Lori Lorigo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

    David McAllester

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Allen, S.F., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L. (2000). The Nuprl Open Logical Environment. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_12

Download citation

  • DOI: https://doi.org/10.1007/10721959_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67664-5

  • Online ISBN: 978-3-540-45101-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation