Sequents and link graphs: contraction criteria for refinements of multiplicative linear logic

Abstract

In this thesis we investigate certain structural refinements of multiplicative linear logic, obtained by removing structural rules like commutativity and associativity, in addition to the removal of weakening and contraction, which characterizes linear logic. We define a notion of sequent that is able to capture these subtle structural distinctions. For each of our calculi (MLL, NCLL, CNL, and NL<>R) we introduce a theory of two-sided proof structures, which, in many respects, turns out to be more appropriate than the standard one-sided approach. We prove correctness criteria, stating which among those proof structures correspond to proofs, i.e. are proof nets. For this we introduce a contraction relation defined on the space of link graphs, a notion sufficiently general to capture both proof structures and sequents, and the key-concept in this work, which is a step towards a unification of the logical core of many distinct calculi.