act Completion (Full Version) Guillaume Burel Claude Kirchner August 6, 2007 Deduction Modulo implements Poincar´e’s principle by identifying deduction and computation as diff...
Abstract. We give a simple and direct proof that super-consistency implies cut elimination in deduction modulo. This proof can be seen as a simplification of the proof that super-...
Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, that relies ...
We present constructive arithmetic in Deduction modulo with rewrite rules only. In natural deduction and in sequent calculus, the cut elimination theorem and the analysis of the st...