Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <4740.9502280940@frogland.inmos.co.uk>
Subject: Re: FWD: Recent proofs with nqthm?
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Tue, 28 Feb 1995 09:40:54 +0000 (GMT)
Content-Type: text
Content-Length: 2335

Tom Melham has said:
> > I wonder what HOL hackers have to say about the conclusions
> > of the following message.
> 
> Well, concerning 
> 
> >    - as far as I know, it is also the only prover which implements a
> >      generalization heuristics (which is also very useful for us).
> 
> I've heard it said by many people that the *real* strength of Boyer-Moore
> is in the simplifier, and not in the heuristics that choose inductions.
> 
> As regards comparisons of theorem provers in general, I think this is
> very problematic.  It's hard to get any scientific, objective, or
> balanced data in this area - few people are sufficiently familiar
> with more than one system, and most everyone's got a vested interest
> in keeping with the system they already use or support.  You've got
> to take with a grain of salt a lot of claims for the superiority of
> one system over another. (Let it be understood, however, that I am
> *not* claiming anything specific about Laurence Pierre's message - I
> am just pointing out some generalties).
> 
> As ever, there's no substitute for experience.  You could almost
> say, the most important thing is not which prover you are using,
> but rather how long you've been using it.

I think that Laurence Pierre's comments are based to a large extent on
their experience when they started their project  (? was it 1989). At
that time they found that Boyer-Moore was more usable than HOL and I
think having made the choice then  they haven't done much comparison
between the systems since as they have been developing for BM.

Since then HOL has improved a lot ... I suspect that things like the
recursive type definition stuff has appeared since then +  all the
libraries. While BM may still seem initially more approachable (after
all, when you start you do simple problems where the BM heuristics can
probably do everything automatically), I would suspect that HOL would
rate a lot higher now.


--------------------------------------------------------------------------
                               david shepherd
 SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, u.k.
          tel/fax: +44 1454 611638/617910    email: des@inmos.co.uk
               www: http://www.inmos.co.uk/~des/welcome.html
       "whatever you don't want, you don't want negative advertising"