Sequents for the grammatical base logic NL are statements X ⇒ A, where X (the antecedent) is a structure, and A (the succedent) a type formula. The antecedent structure is required to be non-empty. A structure is either a single formula, or a binary branching tree with formulas at the leaves.  In the sequent rules below, the tree structure of the antecedent is indicated by bracketing (–,–).  The notation X[Y] refers to a structure X containing a distinguished substructure Y.  For every connective (type-forming operation), there are two inference rules, introducing the connective to the left or to the right of the derivability arrow.  In this sequent presentation, as in Gentzen's propositional logics, Cut is an admissible rule: every proof of a theorem that makes use of Cut inferences can be transformed into an equivalent cut-free derivation. Backward-chaining proof search in the cut-free system respects the subformula property and immediately yields a decision procedure.