Regaining cut admissibility in deduction modulo using abstract completion

stract Completion Guillaume Burel a,c,∗ Claude Kirchner b,c aNancy-Universit´e, Universit´e Henri Poincar´e bINRIA Bordeaux - Sud-Ouest cLORIA, ´Equipe Pareo, Bˆatiment B, Campus Scientifique, 54506 Vandœuvre-l`es-Nancy Cedex 1 Deduction modulo is a way to combine computation and deduction in proofs, by applying the inference rules of a deductive system (e.g. natural deduction or sequent calculus) modulo some congruence that we assume here to be presented by a set of rewrite rules. Using deduction modulo is equivalent to proving in a theory corresponding to the rewrite rules, and leads to proofs that are often shorter and more readable. However, cuts may be not admissible anymore. We define a new system, the unfolding sequent calculus, and prove its equivalence with the sequent calculus modulo, especially w.r.t. cut-free proofs. It permits to show that it is even undecidable to know if cuts can be eliminated in the sequent calculus modulo a given rewrite system. Then, to rec...

• Type: Journal
• Year: 2010
• Where: IANDC
• Authors: Guillaume Burel, Claude Kirchner
• Keywords: Deduction Modulo, IANDC 2010, Sequent Calculus, Sequent Calculus Modulo