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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Benzmiiller, C., et al.: Ωmega: Towards a mathematical assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 252–256. Springer, Heidelberg (1997)
Constable, R., et al.: Implemeriting Mathematics with the NuPRL proof development system. Prentice Hall, Englewood Cliffs (1986)
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)
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)
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)
Gordon, M., Melham, T.: Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)
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)
Jackson, P.: The Nuprl Proof Development System. Version 4-2, Department of Computer Science. Cornell University, Ithica (1994)
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)
Kreitz, C.: Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637. Cornell University. Department of Computer Science (1997)
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)
Kreitz, C., Otten, J., Schmitt, S., Pientka, B.: Matrix-based Constructive Theorem Proving. In: Intellectics and Computational Logic. Kluwer, Dordrecht (2000)
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)
The MathBus Term Structure, http://www.cs.Cornell.edu/simlab/papers/mathbus/mathTerm.htm
Metaprl home page, http://ensembleOl.cs.Cornell.edu:12000/cvsweb/meta-prl
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Naumov, P.: Publishing formal mathematics on the web. Technical Report TR98-1689. Cornell University. Department of Computer Science (1998)
Naumov, P.: Importing Isabelle formal mathematics into Nuprl. Technical Report TR99-1734. Cornell University. Department of Computer Science (1999)
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)
Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361–386. Academic Press, London (1990)
Srinivas, Y.V., Jüllig, R.: SPECWARE: Formal Support for composing software. In Mathematics of Program Construction (1995)
Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison Wesley, Reading (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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