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; Tue, 7 Jun 1994 00:49:15 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA24384;
          Mon, 6 Jun 1994 17:47:05 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from itd0.dsto.gov.au by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA24380;
          Mon, 6 Jun 1994 17:46:52 -0600
Received: from tcs22.dsto.gov.au by itd0.dsto.gov.au 
          with SMTP (5.64+1.3.1+0.50/DSTO-1.0) id AA24371;
          Tue, 7 Jun 1994 09:15:10 +0930
Date: Tue, 7 Jun 1994 09:15:10 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9406062345.AA24371@itd0.dsto.gov.au>
To: hol2000@leopard.cs.byu.edu
Subject: Re: An Alternate Subgoal Package
In-Reply-To: Mail from 'hol2000-request@lal.cs.byu.edu' dated: Mon, 06 Jun 94 12:34:09 +0100

> ... and is the alternative method actually better?

I don't know that it is better.
I can, as I said, think of just the following advantages:
+ You don't have to check to see if a tactic is valid as there is no danger
  of the decomosition step working and the proof step failing.
+ Since this is sort of a one pass process rather than the presently used two
  pass process, there may be potential for a speed increase.
There may be other advantages (can someone suggest any)
(Also, I have to agree with John, it has (to some of us at least) the 
 advantage of being a really neat idea.)

There may be disadvantages to counter-ballance these.
Alternatively, this may be the better solution, but if not much changes about
HOL2000 then these advantages may not be enough to justify rewriting the 
subgoal package.

Those of you out there who have experiance with either using or implenenting
both syles of subgoal systems, don't hold back, let us hear your impressions.

Jim