@Article{	  kreitz.ea:matrix:2004,
  abstract	= { We develop a matrix characterization of logical validity
		  in MELL, the multiplicative fragment of propositional
		  linear logic with exponentials and constants. To prove the
		  correctness and completeness of our characterization, we
		  use a purely proof theoretical justification rather than
		  semantical arguments. Our characterization is based on
		  concepts similar to matrix characterizations proposed by
		  Wallen for other non-classical logics. It provides a
		  foundation for developing proof search procedures for MELL
		  by adopting techniques that are based on these concepts and
		  also makes it possible to adopt algorithms that translate
		  the machine-found proofs back into the usual sequent
		  calculus for MELL.},
  author	= {Christoph Kreitz and Heiko Mantel},
  copyright	= {Kluwer},
  journal	= {Journal of Automated Reasoning},
  language	= {USenglish},
  pages		= {121--166},
  title		= {A Matrix Characterization for Multiplicative Exponential
		  Linear Logic},
  volume	= 32,
  year		= 2004,
  user		= {hmantel}
}