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; Tue, 26 Sep 1995 19:47:04 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA087227944; Tue, 26 Sep 1995 11:52:24 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA087187926; Tue, 26 Sep 1995 11:52:06 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 26 Sep 1995 18:14:56 +0100 X-Mailer: exmh version 1.6.1 5/23/95 X-Uri: To: Konrad Slind Cc: info-hol@leopard.cs.byu.edu, Richard.Boulton@cl.cam.ac.uk Subject: Re: At a Los for something to do? (III) In-Reply-To: Your message of "Tue, 26 Sep 1995 14:51:02 BST." <95Sep26.145108met.8084@sunbroy14.informatik.tu-muenchen.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Tue, 26 Sep 1995 18:14:45 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:035350:950926171512"@cl.cam.ac.uk> Konrad asks: > Has anybody got a PRENEX_CONV? There's one in the sources of the arith library. It can probably be done more efficiently. The arith library contains a lot of normalisation code. I discuss some of the efficiency issues in Section 5.2.4 of my PhD thesis: http://www.cl.cam.ac.uk/users/rjb/phd/ and also a bit in my paper in this year's HOL workshop: http://www.cl.cam.ac.uk/users/rjb/papers/ Richard. ------------------------------------------------------------------------------ Richard J. Boulton, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom Telephone: +44 (0)1223 334729, Fax: +44 (0)1223 334678 E-mail: Richard.Boulton@cl.cam.ac.uk, URL: http://www.cl.cam.ac.uk/users/rjb/ ------------------------------------------------------------------------------