Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9406081532.AA10246@switha.dcs.gla.ac.uk>
To: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Cc: hol2000@leopard.cs.byu.edu, jug@itd.dsto.gov.au, tfm@dcs.gla.ac.uk
Subject: Alternate Subgoal Package / Natural Deduction.
In-Reply-To: Your message of "Tue, 07 Jun 94 13:49:25 EDT." <9406071749.AA10448@msiadmin.cit.cornell.edu>
Date: Wed, 08 Jun 94 16:32:09 +0100


It's perhaps somewhat a matter of personal preference, but I'm afraid I
don't necessarily share Jim's view about the alternative subgoals:

jug> (Also, I have to agree with John, it has (to some of us at least) the 
jug>  advantage of being a really neat idea.)

This is mainly because, as Garrel points out:

> The style of proof you are suggesting is based on a Gentzen style L system.

and I've always thought of HOL as being essentially natural deduction.

I think one of the attractive aspects of HOL is that there is a really
clean, simple, and quite definite "story" one can tell (and understand)
about its logical basis. For me, this is really important -- for
example, in my HOL course I make sure the participants really
understand the logical status of tactics in terms of primitive
inference (i.e. natural deduction).  I'd be worried about anything
built on top of the core that makes this kind of understanding
difficult.  On the other hand, if it's (1) useful and (2) you *can* 
explain its logical basis in a satisfying way... then I'm generally
all for it.

Tom