Sciweavers

Share
IANDC
2010

Regaining cut admissibility in deduction modulo using abstract completion

8 years 7 months ago
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...
Guillaume Burel, Claude Kirchner
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where IANDC
Authors Guillaume Burel, Claude Kirchner
Comments (0)
books