Proof Nets for Multiplicative and Additive Linear Logic

Gianluigi Bellin

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.

LFCS report ECS-LFCS-91-161

Previous | Index | Next