La déduction modulo est un formalisme permettant de combiner règles de réécriture et systèmes de déduction. Une de ses forces vient que l'on permet de réécrire des propositions atomiques en propositions composées. Cela permet d'exprimer de nombreuses théories axiomatiques comme la théorie des ensembles de Zermerlo ou la Logique d'Ordre Supérieur dans un formalisme du premier ordre, sans aucun axiome. La contrepartie de cet souplesse est que dans le cas général, les bonnes propriétés, telles que l'élimination des coupures, sont perdues. Il faut donc trouver des condition sur les règles de réécriture permettant de prouver l'élimination des coupures.
Je présenterai une méthode sémantique, basée sur le paradigme correction-complétude forte qui permet de prouver l'élimination des coupures pour différentes conditions sur les règles de réécriture. Je présenterai aussi les grandes lignes des preuves qui permettent cela: ces preuves sont constructives. Je m'attacherai à montrer que le contenu calculatoire de telles preuves est un algorithme de tableaux, et ne peut être la normalisation de preuves. Ceci est relativement bien etudié dans le cas de la logique classique, mais semble être un fait nouveau en logique intuitionniste, y compris sans règles de réécriture.