Abstract: This paper extends the theory of proof nets from Multiplicative Linear Logic to Multiplicative and Additive Linear Logic, by removing the additive boxes. This yields uniqueness of normal form for that fragment and a classification of permutability of inferences in the calculus of sequents for classical Linear Logic.
Previous | Index | Next An error occured whilst processing this directive