Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 6 Jun 1994 14:54:09 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27712;
          Mon, 6 Jun 1994 07:50:54 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from ULTRASTAR.EE.CORNELL.EDU by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA27708;
          Mon, 6 Jun 1994 07:50:52 -0600
Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) 
          id AA24634; Mon, 6 Jun 94 09:50:07 EDT
Message-Id: <9406061350.AA24634@ultrastar.EE.CORNELL.EDU>
From: markaa@ultrastar.EE.CORNELL.EDU (Mark D. Aagaard)
Date: Mon, 6 Jun 1994 09:50:06 -0400
Organization: Cornell University, Electrical Engineering, Ithaca NY 14853
X-Address: 389 Engineering and Theory Center
X-Phone: (607) 255 0302
X-Fax: (607) 255 9072
X-Mailer: Mail User's Shell (7.2.4 2/2/92)
To: hol2000@leopard.cs.byu.edu
Subject: Re: An Alternate Subgoal Package


| Jim Grundy writes:
|
| Instead, I think we should start with a thereom of the form (Goal |- Goal).
| And progrees the proof by working on the assumptions of the thorem, slowly
| reducing them to true via a process of breaking them up into simpler subgoals.

I think, but I may be wrong about this, that Lambda begins a
proof for hardware verification with (Spec |- Spec), which
the user refines to (Imp |- Spec).  This seems to be similar
to the style that Jim proposes.  
 
 -mark aagaard