It is a tacit assumption of much linguisticinquiry that alldistinctderivations of a string should assign distinct meanings. But despite the tidinessof such derivational uniqueness, there seems to be no a priorireason to assume that a gramma r must have this property. Ifa grammar exhibits derivational equivalence, whereby distinct derivations of a string assign the same meanings, naive exhaustive search for all derivations will be redundant, and quite possibly intractable. In this paper we show how notions of derivation-reduction and normal form can be used to avoid unnecessary work while parsing with grammars exhibiting derivational equivalence. With grammar regarded as analogous to logic, derivations are proofs; what we are advocating is proof-reduction, and normal form proof; the invocation of these logicaltechniques adds a further paragraph to the story of parsing-as-deduction.