Subformula semantics for strong negation systems

We present a semantics for strong negation systems on the basis of the subformula property of the sequent calculus. The new models, called subformula models, are constructed as a special class of canonical Kripke models for providing the way from the cut-elimination theorem to model-theoretic results. This semantics is more intuitive than the standard Kripke semantics for strong negation systems.