  Linear logic is a substructural logic proposed as a refinement of classical
and intuitionistic logics, with applications in programming languages, game
semantics, and quantum physics. We present a template for Gentzen-style linear
logic sequents that supports verification of logic inference rules using
automatic theorem proving. Specifically, we use the Z3 Theorem Prover [8] to
check targeted inference rules based on a set of inference rules that are
presumed to be valid. To demonstrate the approach, we apply it to validate
several derived inference rules for two different fragments of linear logic:
MLL+Mix (Multiplicative Linear Logic extended with a Mix rule) and MILL
(Multiplicative Intuitionistic Linear Logic).
