Based-on dependency Calculi for Non-commutative Logic

In this paper we propose new calculi for the multiplicative fragment of Non-commutative Logic (MNL) which is a linear logic that combines both commutative and noncommutative connectives. Both sequent and proof net calculi, that are new prooftheoretical formulations of MNL, are based on dependency relations. After proving their main properties and also adequacy and sequentialization theorems between both calculi, we provide an algorithm for MNL proof nets construction that is correct and complete. Moreover the related correctness criterion for MNL proof nets is shown quadratic in time. The use of dependency graphs for deciding provability appears as a powerful tool for ecient proof search in such mixed logics