Superdeduction is a systematic way to extend a deduction system like the sequent calculus by new deduction rules computed from the user theory. We show how this could be done in a systematic, correct and complete way. We prove in detail the strong normalization of a proof term language that models appropriately superdeduction. We finaly examplify on several examples, includ- ing equality and noetherian induction, the usefulness of this approach which is implemented in the lemuridæ system, written in TOM.