Cut Admissibility by Saturation

International audienceDeduction modulo is a framework in which theories are integrated intoproof systems such as natural deduction or sequent calculus bypresenting them using rewriting rules. When only terms are rewritten,cut admissibility in those systems is equivalent to the confluence ofthe rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This isno longer true when considering rewriting rules involvingpropositions. In this paper, we show that, in the same way that it ispossible to recover confluence using Knuth-Bendix completion, one canregain cut admissibility in the general case using standardsaturation techniques. This work relies on a view of propositionrewriting rules as oriented clauses, like term rewriting rules can beseen as oriented equations. This also leads us to introduce anextension of deduction modulo with *conditional* term rewritingrules