Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: Sebastian Maneth <semaneth@cis.umassd.edu>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: cut elimination in HOL
In-Reply-To: Your message of "Tue, 24 May 94 22:52:23 EDT." <199405250252.AA11221@argo.cis.umassd.edu>
Date: Wed, 25 May 94 11:39:48 +0100
From: Sara Kalvala <Sara.Kalvala@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:099800:940525104021"@cl.cam.ac.uk>


Hi, Sebastian,

Thomas Forster is interested in the issue of cut elimination too, and
he may reply directly to your message.

> My question is, how can I actually construct a proof tree that I can
> thereafter manipulate.

In the HOL world the term proof tree has often been used to refer to
the tree of tactics in a proof rather than the tree of inferences.
Proofs are mostly interesting only as transients to prove theorems,
and proof trees even when they are supported through add-ons to HOL
are mostly for proof development and informal understanding. These
structures do not map easily in a one-to-one way to the tree of
inferences, which is what you are interested in. However, you may want
to check out my paper at the '91 HOL meeting (at Davis) and this
year's papers (to be presented at Malta) by Konrad Slind and Tom
Schubert/John Briggs.

> If the only data struture for a proof is multiple application of ML
> functions and use of existing theorems, it seems like there is not a
> notion of a proof tree at all, but rather only the single steps in a
> proof. 

To reason about HOL proofs itself, there is the new theory about HOL
proofs, also to be presented by Joakim von Wright at Malta and
available as documentation for the contrib directory HOLproof. Wai
Wong has developed a method for recording HOL proofs in terms of the
primitive inferences; however, he stores the proof as a sequence of
inference applications rather than a tree, it might need some
twiddling to do what you want, but it is possible. The package is
described in the Manual for the record_proof library.

> I want to implement a form of cut elimination for higher order logic proofs,
> and I am wandering if HOL is the right system to use; or if I should rather

The only other system I am at all familiar with is Isabelle, and it
also implements Higher-Order Logic. One advantage is that inference
rules are examinable objects rather than ML functions; hovewer, a
theorem does not record the sequence of inferences used in proving it,
and one might have to look at the tactics used in the proof, again.
There is a proposal to include this information (in the barest form
possible) in a later release of Isabelle, and I am looking for this
feature too.

Hope this helps,

							- Sara