Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199507141222.AA138094551@bobcat.cs.byu.edu>
To: shaw@cs.ucdavis.edu
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Easy theorem-provers -- not the Soft. Eng. answer
In-Reply-To: Your message of Thu, 13 Jul 1995 15:00:46 -0700. <9507132200.AA13833@ice.cs.ucdavis.edu>
Date: Fri, 14 Jul 1995 06:22:31 -0600
From: Phil Windley <windley@cs.byu.edu>


On Thu, 13 Jul 95 15:00:46 -0700 shaw@cs.ucdavis.edu writes
+--------------------
| My opinion on the making-HOL-easier-for-the-software-engineer is not to do
| so. 

Well, from Tim and Rob's comments, it obvious that I was misunderstood.

I'm not calling for a dumming down of HOL.  

All I'm asking for is something like the PVS "grind" that removes the
tedium.   We have some nice libraries that actually go a long way toward
the gaol, but, IMHO, not far enough.  This is not a question that needs
lots of market research.  The choice is: "would I rather sit down and type
GRIND_TAC when I get to the tedious part or would I rather spend the next
30 minutes to 3 weeks (depending on experience) looking up theorems,
manipulating assoc. and comm. terms, etc."  The answer it seems is obvious.

We have the following libraries which are apropos:

taut
unwind
faust
reduce
arith
others???

They are fine in their own right, but:

1.) They do not go far enough

2.) They are not in the base system

3.) They are not integrated in anyway.

Some have argued for keeping the core small.  What compelling reason do we
have to make the core small that overrides making it useful?  

--phil--