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 18:53:03 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01656;
          Tue, 7 Jun 1994 11:50:29 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from cornell.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA01652; Tue, 7 Jun 1994 11:50:28 -0600
Received: from msiadmin.cit.cornell.edu ([128.253.216.2]) by cornell.edu 
          with SMTP id <579917-4>; Tue, 7 Jun 1994 13:49:44 -0400
Date: Tue, 7 Jun 1994 13:49:25 -0400
From: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Received: from msipawn.409col_ave by msiadmin.cit.cornell.edu (4.1/1.5) 
          id AA10448; Tue, 7 Jun 94 13:49:25 EDT
Message-Id: <9406071749.AA10448@msiadmin.cit.cornell.edu>
To: hol2000@leopard.cs.byu.edu, jug@itd.dsto.gov.au
Subject: Re: An Alternate Subgoal Package

The style of proof you are suggesting is based on a Gentzen style L system.
See the references appended.

Regards,

Garrel

**********************************************************************

@article{gentzen:untersuchungen,
        author = "Gerhard Gentzen",
        title = "Untersuchungen {{\"u}ber} das logische {Schliessen}",
        journal = "Mathematische Zeitschrift",
        volume = 39,
        year = 1934,
        pages = "176--210, 405--431",
        note = "Translated in Szabo (ed.), {\em The Collected Papers
                of Gerhard Gentzen} as ``Investigations into Logical
                Deduction''"
}

@incollection{gentzen:investigations,
        author = "Gerhard Gentzen",
        title = "Investigations into Logical Deduction",
        booktitle = "The Collected Papers of Gerhard Gentzen",
        editor = "M. E. Szabo",
        publisher = "North-Holland Publishing Company",
        address = "Amsterdam and London",
        year = 1969,
        pages = "68--131"
}