Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 25 May 1994 04:05:52 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA09925; Tue, 24 May 1994 20:51:51 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from corona.cis.umassd.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA09921; Tue, 24 May 1994 20:51:49 -0600 Received: by argo.cis.umassd.edu id AA11221 (5.65c/IDA-1.4.4 for info-hol@lal.cs.byu.edu); Tue, 24 May 1994 22:52:25 -0400 From: Sebastian Maneth Message-Id: <199405250252.AA11221@argo.cis.umassd.edu> Subject: cut elimination in HOL To: info-hol@leopard.cs.byu.edu Date: Tue, 24 May 94 22:52:23 EDT X-Mailer: ELM [version 2.3 PL11] Hi, I am fairly new to HOL, and have a couple of questions: The way I understand it, a proof in HOL is represented by applications of ML functions to axioms or existing Theorems. If a sequence of such applications is of correct type, one will get a new Theorem. My question is, how can I actually construct a proof tree that I can thereafter manipulate. 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. 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 make up my own data structures in e.g. ML. (it would be much nicer to use a package like HOL that has so many useful tools...) Has anyone done something like that in HOL, or knows a good way to do it? (with 'it' I mean applying rewrite rules to a proof, to implement cut elimination, or any proof manipulation) Thanks for your help, Sebastian semaneth@cis.umassd.edu