[Prev][Next][Index][Thread]

Two sided proof nets with units

Date: Fri, 29 Nov 91 23:46:08 EST

We wish to announce the following preprint:


               The logic of weakly distributive categories I:

                      Two sided proof nets with units

                         R. Blute      R.A.G. Seely



                                  Abstract

We define a two sided notion of proof nets, suitable for logics, like the
logic of weakly distributive categories, which have the two-tensor structure
(with/par) of linear logic, but lack a negation operator.  These proof nets
have a structure more closely parallel to that of traditional natural
deduction than Girard's one-sided nets do.  In particular, there is no cut,
and cut elimination is replaced by normalization.  We prove a
sequentialisation theorem for these nets and the corresponding sequent
calculus, and deduce the coherence theorem for weakly distributive
categories as an application.  We extend these techniques to cover the case
of non symmetric tensors ("planar logic").

One significant feature of this version of proof nets is that we are able to
include the units for the tensors in our presentation.  With this, we are
able to extend these nets to the full case of multiplicative linear logic
(with units), and prove sequentialisation there.  This represents an
improvement over the treatment via one sided nets, which cannot handle the
units successfully.

====================================================

The preprint may be obtained by anonymous ftp from  triples.Math.McGill.CA
(132.206.150.30) in the usual manner, or by contacting one of the authors.

Via ftp:  Login as anonymous, use your email ID as password.
The various files are located in the directory  pub/rags/nets
You will find a PostScript file, a DVI file, and the TeX source code.  If
you want to take the TeX source code, read the nets.README file first, to 
find out what macro files are also necessary.  (And for other instructions.)

At the moment only the extended abstract will be found in this ftp
directory; shortly the full paper (including other results, such as
conservativity of the extension from weakly distributive categories to
*-autonomous categories, in the unit-free case,) will be placed there as
well.  If you wish to be notified of such "upgrades", drop one of us a line.
(Or just browse, from time to time.)

Authors' address:

Department of Mathematics
McGill University
805 Sherbrooke St. W.
Montreal
Quebec  H3A 2K6
Canada

FAX: (514) 398-3899

Phone: (514) 398-3804


Authors' email addresses:

Blute:  blute@triples.math.mcgill.ca
Seely:  rags@triples.math.mcgill.ca