SAL Home MATH Misc


Nuprl is a proof development system and a system for implementing mathematics.

Problem solving is a significant part of science and mathematics and is the most intellectually significant part of programming. Solving a problem involves understanding the problem, analyzing it, exploring possible solutions, writing notes about intermediate results, reading about relevant methods, checking results, and eventually assembling a solution. Nuprl is a computer system which provides assistance with this activity. It supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics; with it one can express concepts associated with definitions, theorems, theories, books and libraries. Moreover, the theory is sensitive to the computational meaning of terms, assertions and proofs, and the system can carry out the actions used to define that computational meaning. Thus Nuprl includes a programming languages, but in a broader sense it is a system for implementing mathematics.

Current Version:   4.2

License Type:   ??

Home Site:

Source Code Availability:

Yes (FTP Site below)

Available Binary Packages:

  • Debian Package: No
  • RedHat RPM Package: No
  • Other Packages: Yes (FTP Site below)

Targeted Platforms:


Software/Hardware Requirements:

Lisp implementation

Other Links: (FTP site)

Mailing Lists/USENET News Groups:


User Comments:

  • None

See A Screen Shot? (Not Yet)

  SAL Home   |   Mathematics   |   Misc

Comments? SAL@KachinaTech.COM
Copyright © 1995-2001 by Herng-Jeng Jou
Copyright © 1997-2001 by Kachina Technologies, Inc.
All rights reserved.