The Noble Art of Linear Decorating Harold Schellinx Abstract: Linear logic (Girard, 1987) is a refinement of the formulation of classical logic as a sequent calculus (Gentzen, 1935). The `intervention' is simple: in the `classical' formulation a formula, present as a hypothesis in a derivation, can be used an unlimited number of times, and any formula can be introduced as a hypothesis, even it is not used. Furthermore, deriving a theorem a number of times is equivalent to deriving it only once, and whenever a certain conclusion has been reached, say $X$, it is possible to add another one, say $Y$ (as in `$X$ or $Y$'). In the linear formulation this kind of practice is restricted. Contraction and weakening are only allowed if the formula in question is marked with a modality. This in turn leads to the introduction of two variants of familiar logical connectives: an {\em additive} and a {\em multiplicative} variant. If linear typing is ignored, a derivation in classical logic is nothing but a derivation in classical or intuitionistic logic. Schellinx main question is the following: Take some derivation $\pi$ in sequent calculus for classical or intuitionistic logic. Can we transform it into a sequent derivation in linear logic in a way that essentially preserves its structure, i.e. can we define a {\em linear decoration} of the original proof? And if `yes', then is there an {\em optimal} way to do this? Schellinx shows, for example, that for some fragments, for instance that consisting of rules for implication, universal first order quantification, and universal second order (propositional) quantification, this linear decorating is completely {\em deterministic}. Schellinx main concern is with {\em mappings}: from formulas to linear formulas, from classical and intuitionistic proofs to linear proofs, from classical (intuitionistic) proofs to classical (intuitionistic) proof, and from linear proofs to linear proofs, mappings that in most cases will preserve, at least, what he calls the {\em skeleton} of the original, in the case `linear to linear' moreover its {\em dynamics} (i.e. behaviour under cut elimination) Schellinx introduces a number of technical devices for these purposes. In chapter 5 the {\em exponential graph} of a derivation is introduced. This graph permits the characterization of those derivations in linear logic that are {\em dilatable}, that is, derivations in which {\em all} modalized formulas can be replaced by non-model formulas, withou changing the structure and the dynamics of the original. The most important result is that a fully expanded linear derivation is dilatable iff her exponential graph is acyclic. In chapter 6, the notion {\em constrictive morphism} is introduced, which can be used to optimalize modal translations. This leads to well--defined restrictions on rules of the sequent calculus, that maintain completeness with respect to provability. Schellinx formulates `alternative' sequent calculi for intuitionistic and classical logic for which the optimal modal translations are decorated: {\bf ILU}, {\bf LKT} and {\bf LKQ}.