A Matrix Characterization for MELL

We present a matrix characterization of logical validity in the multiplicative fragment of linear logic with exponentials. In the process we elaborate a methodology for proving matrix characterizations correct and complete. Our characterization provides a foundation for matrix-based proof search procedures for $ \mathcal{M}\mathcal{E}\mathcal{L}\mathcal{L} $ \mathcal{M}\mathcal{E}\mathcal{L}\mathcal{L} as well as for procedures which translate machine-found proofs back into the usual sequent calculus