The Nuprl Open Logical Environment

unofficial copies [PDF], [PS]

by Stuart F. Allen, Rich Eaton, Christoph Kreitz, and Lori Lorigo

Proceedings of 17th International Conference on Automated Deduction, 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.