Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 23 Feb 1993 17:18:48 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15351; Tue, 23 Feb 93 09:04:51 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from CORNELLC.CIT.CORNELL.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA15346; Tue, 23 Feb 93 09:04:44 -0800 Received: from msiadmin.cit.cornell.edu by CORNELLC.cit.cornell.edu (IBM VM SMTP V2R2) with TCP; Tue, 23 Feb 93 11:49:49 EST Date: Tue, 23 Feb 93 11:50:15 EST From: garrel@edu.cornell.cit.msiadmin (Garrel Pottinger-MSI Visitor) Received: from msipawn.409col_ave by msiadmin.cit.cornell.edu (4.1/1.5) id AA19096; Tue, 23 Feb 93 11:50:15 EST Message-Id: <9302231650.AA19096@msiadmin.cit.cornell.edu> To: kaufmann@com.cli Subject: Re: power of HOL Cc: info-hol@edu.uidaho.cs.ted We were planning to use non-standard analysis in the Ariel project at ORA (i.e., for purposes of proving asymptotic correctness of floating point programs), and we were planning to use HOL as the theorem prover. Worrying about whether we could legitimately do that was what got me started thinking about the completeness question for the HOL logic. I'm not sure what happened to Ariel after I got laid off at the beginning of December 1991. You could find out by sending a message to Bret Hartman (bret@oracorp.com). Regards, Garrel