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; Thu, 11 Feb 1993 18:34:51 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19034; Thu, 11 Feb 93 08:46:12 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA19028; Thu, 11 Feb 93 08:46:07 -0800 Received: by panther.cs.uidaho.edu id AA11696 (5.65c/IDA-1.4.4 for info-hol@ted); Thu, 11 Feb 1993 08:52:47 -0800 From: Mike Coe Message-Id: <199302111652.AA11696@panther.cs.uidaho.edu> Subject: power of HOL To: info-hol@edu.uidaho.cs.ted Date: Thu, 11 Feb 93 8:52:46 PST X-Mailer: ELM [version 2.3 PL11] I have to do a term paper for my advanced theory of computation class this semester. I would like to do it on the computational power of HOL. Just what can be proven/not proven with HOL. Does the logic put any limits on what can be proven? Are there any good papers or books on this subject out there. any references would be greatly appreciated. mike -- Michael L Coe Laboratory of Applied Logic University of Idaho coe@leopard.cs.uidaho.edu