Nuprl is a proof development system. Much of our effort has gone into a technology for creating and displaying proofs.
When we talk about proofs in our writing, we generally mean formal proofs. This is especially true under this heading of proof technology. While the idea of a proof in the sense discovered by the Greeks and used centrally in mathematics since then is widely used, the technical notion of proof that we have in mind is relatively new, since the 1970s, and much of our technical work has contributed to creating a new notion of formal proof, one that incorporates computer programs (called tactics) to fill in details, and one that allows computers to carry out various kinds of steps such as calculation, symbolic evaluation and rewriting of one term to another. The central new idea that we introduced is called a tactic-tree proof. It built on and extended the idea pioneered in the Edinburgh LCF system of a tactic.
The underlying basis of tactic-tree proofs is the notion of a sequent. Gentzen introduced sequent based proof systems, his L-systems. But we wanted to present proofs in a top-down refinement style rather than Gentzen's bottom-up style. This led us to presentations of sequent proofs in the style of Beth's tableaux. Following Bates, we call this top down sequent logic a Refinement Logic (RL).
Our first writing on Refinement Logics is Joe Bate's thesis. This is also the primitive logic of the article Proofs as Programs. The idea is that proofs are interactively built by refining a single goal into subgoals using an inference rule.
The user is presented with a goal, called a conjecture, and interacts with the system to try to prove it. We can also think of the activity as a systematic attempt to falsify the conjecture. A conjecture consists of a formula G to be proved, generally under hypotheses, say the list of formulas, A1,...,An. (These hypotheses arise for example in considering a goal of the form A => B, read "A implies B". To prove this we assume A and try to prove B, so the subgoal will have conclusion B under hypothesis A.) Call the list of hypotheses H. An inference rule will generate new subgoals which also consist of conclusion Gi under hypotheses Hi. As interaction proceeds, a tree is created whose nodes are goals and rules.
In 1982 we saw a way for tactics as pioneered by Edinburgh LCF to fit into this notion of a proof attempt, namely a tactic is a program that attempts to build a subproof at a node (so a rule is the degenerate case of building one more layer of the tree). If the program succeeds, the subproof is stored at the node and the unproven subgoals are listed as new goals. Thus if the subproof is hidden, a tactic application looks like a rule application, it generates subgoals and builds one new layer of the tree. So tactics have the look of derived rules. This proof mechanism is the heart of Nuprl's inference engine. Our addition created a more local notion of tactic than the one in LCF, we called it a refinement tactic, and we also created a new concept called a transformation tactic. These are defined in our paper. This idea is further developed in Griffin's thesis, and interesting properties of refinement logics are demonstrated in Harper's thesis.
Currently the most concise and rigorous treatment of tactic-tree proofs is in our work on reflection. The definition in the LICS paper, The Semantics of Reflected Proof is nearly a formal account. More details appear in Atiken's thesis, and our work on reflection uses the Nuprl data type corresponding to this definition.
There is a great deal of scope to conduct proof theory on this new concept of proof. For the most part we have been concerned with its efficient implementation and use, but from time to time there are interesting theoretical ideas that appear in the PRL seminar and in our Research Notes. One line of work has been to look at adding so-called logic variables (or metavariables) into proofs since they are so natural for refinement proofs of existential statements. Howe has written about this as well as Pientka and Kreitz .
Another new idea has been to consider the use of infinitary lambda terms to capture the sharing structure explicitly.
The notion of proof we use traces its historical roots to the seminal work of Gerhard Gentzen on Natural Deduction (ND) and Sequent Calculi. Gentzen introduced the N-calculi (NK, NJ for classical and Intuitionistic natural deduction) and the L-calculi (LK, LJ for classical and Intuitionistic sequent calculi).
Our work on PLCV used a new kind of ND calculus, block structured. This work was inspired by the Automath Project of N.G.deBruijn which extended natural deduction calculi to account for organizing mathematical knowledge as well as organizing proofs. An ND calculus with tactics seems like an extremely attractive formalism. Proofs are "readable and natural".
But the notion of a sequent captures almost exactly the information that we wanted to present to a user as the goal of an inference step. We needed to follow Per Martin-Löf in extending the concept to include typing judgements among the possible hypotheses. It turns out that Beth's notion of a Tableau proof captures the idea of a refinement proof discussed above. So Nuprl proofs can be seen as "tactic-tableaux," that is, adding tactics to tableau proofs.
One of the best accounts of tableau proofs for the predicate calculus is Ray Smullyan's classic book, First-Order Logic, recently reprinted by Dover.