The Nuprl
proof rules naturally extend the
Lambda--prl
proof rules and as such
are organized along roughly the same lines.
However, the logic of Nuprl
is considerably more powerful than that
of Lambda--prl
, and the rules are correspondingly more complex.
The Nuprl
rules are classified into three broad categories: * introduction*,
* elimination* and * equality*; the equality rules are further broken
down into * computation rules* and * equality rules* for each of the
term constructors.
The introduction and elimination rules are analogous to those
in Lambda--prl
; the equality rules are a new feature of the Nuprl
logic.

The differences between the logic of Lambda--prl and Nuprl can be briefly summarized as follows:

- Strengthening the type structure.

The Lambda--prl logic is based on two primitive types, integers and lists of integers. The Nuprl logic extends this to a much richer type structure. - Identifying propositions with types.

In Lambda--prl propositions were specific syntactic entities. In Nuprl propositions are simply certain kinds of types. Demonstrating the truth of a proposition amounts to presenting an object of that type so that a proposition is treated as the type of its justifications. - Well-formedness.

In Lambda--prl well--formedness of propositions was checked by the system. The richness of the Nuprl type structure, however, precludes the possibility of automatically checking whether or not an expression is a type. By the identification of propositions with types this property extends to propositions as well. - Explicit treatment of equality and simplification.

In Lambda--prl equality and simplification were by and large taken care of by the`arith`rule, which handled simple arithmetic, substitutivity of equality and simplification of terms (such as`hd[1,2]=1`). The Nuprl logic, however, is sufficiently rich that such a treatment is no longer possible. Consequently there are rules for equality of terms and for computation.

Thu Sep 14 08:45:18 EDT 1995