In the first part of this paper we present a theory of proof nets for fullmultiplicative linear logic, including the two units. It naturally extends thewell-known theory of unit-free multiplicative proof nets. A linking is nolonger a set of axiom links but a tree in which the axiom links are subtrees.These trees will be identified according to an equivalence relation based on asimple form of graph rewriting. We show the standard results ofsequentialization and strong normalization of cut elimination. In the secondpart of the paper we show that the identifications enforced on proofs are suchthat the class of two-conclusion proof nets defines the free *-autonomouscategory.
展开▼
