The Nuprl Open Logical Environment

Stuart Allen, Robert Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo.

In D. McAllester, ed., 17th International Conference on Automated Deduction (CADE-17),
LNAI 1831, pp. 170-176, Springer Verlag, 2000.


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.

Paper is available in
postscript and pdf format
  Slides of the conference presentation are available in compressed postscript and pdf format
(Presentation: Lori Lorigo)

Bibtex Entry

Back to overview of papers
@InProceedings{inp:Allen+00a, author = "Stuart Allen and Robert Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo", title = "The {\sf Nuprl} Open Logical Environment", booktitle = "17$^{th}$ International Conference on Automated Deduction", year = "2000", editor = "D. McAllester", volume = "1831", series = "Lecture Notes in Artificial Intelligence", pages = "170--176", publisher = "Springer Verlag" }