Abstract : In this paper we propose new calculi for the multiplicative fragment of Mixed Linear Logic (MMLL) which is a logic that combines both commutative and non-commutative connectives. These based-on sequent and proof net calculi, that can be seen as a new proof-theoretical formulation of MMLL, are based on the definition of dependency relations. We provide a proof-search procedure for MMLL that is based on proof nets construction with associated sets of dependencies.
Didier Galmiche, Jean-Marc Notin. Calculi with dependency relations for Mixed Linear Logic. International Workshop on Logic and Complexity in Computer Science - LCCS'2001, 2001, Creteil/France, pp.81-102. ⟨inria-00100564⟩