Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 26 May 94 11:19:22 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9405261519.AA09210@ultrastar.EE.CORNELL.EDU>
To: semaneth@cis.umassd.edu
Cc: info-hol@leopard.cs.byu.edu
In-Reply-To: Sebastian Maneth's message of Tue, 24 May 94 22:52:23 EDT <199405250252.AA11221@argo.cis.umassd.edu>
Subject: proof trees in Nuprl ( was cut elimination in HOL)


Nuprl saves representations of proof trees.  Each node consists of the
current assumption list, the tactic applied and the subgoal generated.
(I believe what is saved is the tactics applied, and the proof tree is
regenerated when you examine a proof.)  

Proof trees are objects that can be manipulated in Nuprl.  For example
there are a special class of tactics called transformation tactics
that allow you to do things like copy portions of a proof tree from
one proof to another.  The tactics that succeed are grafted onto the
new proof tree, and if a tactic fails, the rest of the tree is empty.  
This sort of manipulation is very useful for dealing with two branches
of a proof that are similar after a case split, doing a new proof that
closely resembles a proof you have already done, and just trying out
new approaches on a proof.

I don't know very much about cut elimination, so I do not know if this
will help you.

For more information about the Nuprl system, send email to
       nuprlnotes@cs.cornell.edu