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; Fri, 12 Feb 1993 02:02:58 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA24325; Thu, 11 Feb 93 17:39:51 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from cli.com by ted.cs.uidaho.edu (16.6/1.34) id AA24319; Thu, 11 Feb 93 17:39:45 -0800 Received: by CLI.COM (4.1/1); Thu, 11 Feb 93 11:59:41 CST Date: Thu, 11 Feb 93 12:00:08 CST From: Matt Kaufmann Message-Id: <9302111800.AA00626@thunder.CLI.COM> Received: by thunder.CLI.COM (4.1/CLI-1.2) id AA00626; Thu, 11 Feb 93 12:00:08 CST To: coe@edu.uidaho.cs.panther Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: Mike Coe's message of Thu, 11 Feb 93 8:52:46 PST <199302111652.AA11696@panther.cs.uidaho.edu> Subject: power of HOL Here's a possibly relevant point, which I'll post to the HOL mailing list in case someone more expert than I can correct what I say here... One thing that may not often be mentioned, but I think is true, is that the HOL logic is incomplete for the ``intended'' HOL model. (The intended model is obtained by starting with atoms and closing under function space formation.) But this doesn't matter really; theorem provers are generally limited much more by efficiency/heuristic considerations than theoretical completeness anyhow. -- Matt Kaufmann