Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 13 Jan 1993 10:02:55 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25581; Wed, 13 Jan 93 01:48:56 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA25576; Wed, 13 Jan 93 01:48:42 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Wed, 13 Jan 1993 09:48:05 +0000 To: Konrad Slind Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Bottleneck in HOL (was Re: BETA_CONV) In-Reply-To: Your message of Wed, 13 Jan 93 00:05:52 +0100. <93Jan13.000602met.8121@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 13 Jan 93 09:47:58 +0000 From: Richard Boulton Message-Id: <"swan.cl.ca.363:13.01.93.09.48.08"@cl.cam.ac.uk> Konrad writes: > In my opinion, and I'm totally off topic here (and > perhaps flagrantly wrong!), the bottleneck in the HOL system these days > is not the system; it's the user and the low level at which they > operate. Take the library of sets for example: it takes hol90 approx. 45 > seconds to prove all the theorems in the library. How long did it take > to write the proofs? I don't disagree with this. However, one way to get the user working at a higher level is to provide more decision procedures and `intelligent' tactics. These can be very computationally intensive in any system, but especially in HOL. If you give the user a tactic that takes a decade to run they simply won't use it, but will look for a slick manual proof instead. So, we're back to making HOL `more efficient', whatever that means. Richard.