Ce rapport présente un calcul des séquents où les théories exprimées sous la forme de systèmes de réécriture sont traduites en règles ad hoc pour le calcul des séquents. Cela permet à la fois de réduire la taille des démonstrations en vue de la mise en oeuvre d'un assistant et de raisonner dans la théorie vide, ce qui ramène la preuve de la cohérence d'une théorie à une démonstration d'élimination des coupures dans le système de déduction dérivé de cette théorie. Le rapport expose différentes versions classiques et intuitionnistes du système, ainsi que l'ébauche d'un langage de termes de preuve. Après quelques exemples d'application du système, un prototype d'assistant à la démonstration fondé sur la version classique y est présenté.