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 09:09:48 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA11947; Wed, 25 May 1994 02:00:43 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA11943; Wed, 25 May 1994 02:00:36 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Wed, 25 May 1994 09:56:19 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <03123-0@i80fs2.ira.uka.de>; Wed, 25 May 1994 10:02:39 +0200 To: info-hol@leopard.cs.byu.edu Subject: cut elimination(Proof trees) in HOL Date: Wed, 25 May 1994 10:02:37 +0200 From: schneide Message-Id: <"i80fs2.ira.125:25.04.94.08.02.41"@ira.uka.de> Sebastian wrote: |> it seems like there is not a notion of a proof |> tree at all, but rather only the single steps in a proof. Yes, that's right. However, you can reconstruct a proof tree of the HOL tactics, if you consider a sequence of t1 THEN t2 ... THEN tn as a linear sequence of nodes in the proof tree and t THENL[t1,...,tn] as a node t where the proof tree branches in n successor nodes. If you just consider your own proofs, then it is possible to create HOL tactics in the above manner, i.e. it is possible to construct a proof such that the tactic exactly corresponds to the proof tree. In general, this does however not hold. To see this consider a tactic as INDUCT_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] If a proof can be done by the application of this tactic, you have no chance to reconstruct the proof tree just of the above tactic, i.e. without looking at the goal. So, you can do whatever you like with your own proofs, but not with arbitrary proofs. There are however other tools for higher order logic, and I think (but I have never seen it) that Nuprl has a proof tree editor. Klaus.