This tutorial is intended as an introduction to the Nuprl system. It leads you through using Nuprl's term and proof editor, and gets you to prove a theorem from predicate calculus.
No previous familiarity with the Nuprl system is assumed, but you should be familiar with some presentation of propositional and predicate logic in a two-sided sequent style. By two-sided we mean that introduction rules are given for each connective on each side of the turnstile. The two-sided style is less common than the one-sided style in which introduction and elimination rules are given for each connective on the right hand side of the turnstile. The one-sided style often goes by the name of natural deduction. The two-sided style turns out to be more convenient for automation. In Nuprl, the introduction rules are used bottom-up, so each specifies how to take apart or decompose some connective.
Basic reference material that covers this tutorial can be found in Section 12. For more detailed information on the Nuprl system you should consult the Nuprl Reference Manual and for information about the ML language, the Nuprl ML Manual.