Nuprl


Also found in: Wikipedia.

Nuprl

/nyu p*rl/ Nearly Ultimate PRL.

A system for interactive creation of formal mathematics, including definitions and proofs. It has an extremely rich type system, including dependent functions, products, sets, quotients and universes. Types are first-class citizens. It is built on Franz Lisp and Edinburgh ML.

["Implementing Mathematics in the Nuprl Proof Development System", R.L. Constable et al, P-H 1986].
Mentioned in ?
References in periodicals archive ?
Bridges" or "ad-hoc" information exchange solutions: The pairs of systems in this category include bridges combining PVS, HOL, or Isabelle with Maple, NuPRL with Weyl, Omega with Maple/GAP, Isabelle with Summit, and most recently, Lean with Mathematica [35,45-51], The example given above, bridging Isabelle and Maple, is an example of an approach from this category.
Similar algorithms have also been used in proofcheckers for dependent type theories, such as NuPrl [Howe 1988] and Lego [Pollack 1990].
For recent notable work, I focus on some significant theorem-proving systems: the geometry theorem provers of Chou (Chou, Gao, and Zhang 1994; Chou 1988); the Boyer and Moore (1988) interactive theorem prover NQTHM and its successor ACL2 (Kaufmann and Moore 1996); the rewrite rule laboratory (RRL) of Kaput and Zhang (1995); the resolution prover OTTER (McCune and Otter 1997; McCune 1994) and the equational logic prover EQP by McCune (1996); the interactive higher-order logic provers NUPRL (Constable et al.
Lucent Technologies (Bell Laboratories) is using a combination of HOL and NUPRL tO verify the SCI cache coherency protocol.
The ability to tackle these real-world problems is primarily the result of the improved capabilities of interactive systems such as NQTHM, ACL2, PVS, NUPRL, HOL, COQ (Coquand and Huet [INRIA] 1988), and ISABELLE (Paulson [Cambridge] 1994).
However, many other systems now have user communities of their own, some sizable: NQTHM, ACL2, and RRL, for example, and the higher-order logic systems HOL, NUPRL, ISABELLE, PVS, COQ, and TPS.
The verification of the SCI cache coherency protocol mentioned earlier uses a linking of HOL and NUPRL, which allows many theorems from HOL to be imported into NUPRL.
The Horus/Ensemble project has also investigated a number of issues beyond those addressed in Coyote to date, including development of a theoretical framework based on Nuprl [Constable et al.
This category may itself be subdivided into provers for a specific logic like the Boyer-Moore prover [4] and LCF [12], and generic provers such as ELF [13], NuPRL [7], and Isabelle [24].
NuPRL features transformation tactics to support the reuse of proofs.
PRL and later NuPRL use mathematical proofs as the basic part of a program development system.