Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: chou@cs.ucla.edu
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: FWD: Recent proofs with nqthm?
In-Reply-To: Your message of "Fri, 24 Feb 1995 23:06:36 PST." <9502250706.AA09027@maui.cs.ucla.edu>
Date: Mon, 27 Feb 1995 20:07:47 +0000
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:132330:950227204141"@cl.cam.ac.uk>


> 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.

Tom