Regaining Cut Admissibility in Deduction Modulo using Abstract Completion

Guillaume Burel 1, * Claude Kirchner 1, 2
* Auteur correspondant
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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 recover the cut admissibility, we propose a procedure to complete the rewrite system such that the sequent calculus modulo the resulting system admits cuts. This is done by generalizing the Knuth-Bendix completion in a non-trivial way, using the framework of abstract canonical systems. These results enlighten the entanglement between computation and deduction, and the power of abstract completion procedures. They also provide an effective way to obtain systems admitting cuts, therefore extending the applicability of deduction modulo in automated theorem proving.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2010, 208 (2), pp.140-164. 〈10.1016/j.ic.2009.10.005〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00132964
Contributeur : Guillaume Burel <>
Soumis le : mercredi 18 novembre 2009 - 17:49:25
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 10:44:58

Fichiers

gencomp_ic.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Burel, Claude Kirchner. Regaining Cut Admissibility in Deduction Modulo using Abstract Completion. Information and Computation, Elsevier, 2010, 208 (2), pp.140-164. 〈10.1016/j.ic.2009.10.005〉. 〈inria-00132964v2〉

Partager

Métriques

Consultations de la notice

271

Téléchargements de fichiers

157