Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Fri, 14 Jul 95 11:27:12 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9507141527.AA12739@ultrastar.EE.CORNELL.EDU>
To: info-hol@leopard.cs.byu.edu
Subject: making theorem provers easier to use


my 2 cents worth on this discussion:

There is a tension here between making a tool easy to use and having a
sound basis.  HOL's claim to fame is it's very small and easy to understand
basis and the fact that most proof done in HOL is directly or
indirectly built on top of that base.  

There are several directions to go if you want to make a theorem
prover like HOL more useful:

1)  Improve the user interface.  This can be a huge help, but is only
part of the problem.

2)  Add more powerful libraries and tactics to help people solve the
problems they are likely to come across.  The problem here is this
means there are more library routines, ML functions, etc for the
new user to learn.  There needs to be a mechanism for organizing the
tools available so users can find them.  

3)  Allow decision procedures to automate some of the tedium.  If you
do this you are getting away from HOL's strength which is its simple
basis.  

I believe the answer is a combination of all three approaches.
Decision procedures can be a huge help, but in the context of
a formal proof it is important to know what you have relied upon to
obtain your goal.  Some sort of mechanism to annotate proofs with the
decision procedures they rely on is the solution that I propose.

I also believe that for specific application areas you can package up
the tactics, definitions etc commonly used and provide a nice
interface for a theorem prover.  The user only needs to learn a few
tactics to make great strides, provided they follow your conventions.
The user still has the full power and tedium of the theorem if they
choose not to use your techniques.

A few years ago we attempted to automate hardware verification for
digital circuits.  Mark Aagaard and I developed a library in Nuprl,
and Phil Windley did the same in HOL88. We provided functions
(create_hw_module for primitives, and create_pmod for parameterized
modules) which generated all the definitions you needed to prove
hardware modules.  We also provided four or five tactics which allowed
you to solve most of the hardware goals a user encountered.  These
included boolean simplification, case analysis with boolean
simplification, rewriting sequential statements, etc.  [See HUG'94
our paper on SuperDuperHWTac].

Although others haven't used this particular library, I think this
mode of operation goes a long way to solving the problems of users and
relieving tedium.  Tedium arises from doing the same thing over and
over again...  These steps can be automated.

Once again,  this is not the whole solution, just another approach.
Application oriented environments + user interfaces + decision
procedures ....  Now there's a theorem proving environment I could get
something done in!

Miriam Leeser
mel@ee.cornell.edu