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; Thu, 26 May 1994 22:05:20 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28384; Thu, 26 May 1994 14:51:55 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA28376; Thu, 26 May 1994 14:51:37 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 26 May 1994 20:20:50 +0100 To: info-hol@leopard.cs.byu.edu Subject: Re: Decidability In-Reply-To: Your message of "Wed, 25 May 94 13:34:09 EDT." <9405251734.AA12452@msiadmin.cit.cornell.edu> Date: Thu, 26 May 94 20:20:46 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:083840:940526192053"@cl.cam.ac.uk> Garrel writes: | A couple of years ago, I extended Henkin's result to cover the HOL logic and | reported this in a message to info-hol. If enough people are interested, | I can resend the report. The relevant message is still available in the info-hol archive, as a search for "completeness" on Windley's World Wide Web quickly reveals. Those still stuck in the FTP Age can get it from: ftp.cl.cam.ac.uk in directory hvg/info-hol-archive Here is the relevant part of the index. 0485 27 Jan 92 Tobias Nipkow Overloading of constant names 0486 27 Jan 92 Kim Dam Petersen Re: Generic graphs (was: Overloading 0487 28 Jan 92 Garrel Pottinger Report on completeness to follow > 0488 28 Jan 92 Garrel Pottinger Report on HOL completeness theorem 0489 29 Jan 92 Juanito Camilleri Change of address...... 0490 30 Jan 92 Roger Jones EMACS thanks 0491 30 Jan 92 Ching-Tsun Chou Problem with running HOL on a NeXT John.