Cut Elimination in Deduction Modulo by Abstract Completion

Guillaume Burel 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Deduction Modulo implements Poincaré's principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction modulo is logically equivalent to first-order logic, proofs in such systems are quite different and dramatically simpler with one cost: cut elimination may not hold anymore. We prove first that it is even undecidable to know, given a congruence over propositions, if cuts can be eliminated in the sequent calculus modulo this congruence. Second, to recover the cut admissibility, we show how computation rules can be added following the classical idea of completion a la Knuth and Bendix. Because in deduction modulo, rewriting acts on terms as well as on propositions, the objects are much more elaborated than for standard completion. Under appropriate hypothesis, we prove that the sequent calculus modulo is an instance of the powerful framework of abstract canonical systems and that therefore, cuts correspond to critical proofs that abstract completion allows us to eliminate. In addition to an original and deep understanding of the interactions between deduction and computation and of the expressivity of abstract canonical systems, this provides a mechanical way to transform a sequent calculus modulo into an equivalent one admitting the cut rule, therefore extending in a significant way the applicability of mechanized proof search in deduction modulo.
Type de document :
Communication dans un congrès
Sergei Artemov and Anil Nerode. Symposium on Logical Foundations of Computer Science LFCS'07, Jun 2007, New York, United States. Springer Verlag, 4514, pp.115-131, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-72734-7_9〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00115556
Contributeur : Guillaume Burel <>
Soumis le : lundi 26 février 2007 - 15:22:48
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 14:32:52

Fichiers

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

Identifiants

Collections

Citation

Guillaume Burel, Claude Kirchner. Cut Elimination in Deduction Modulo by Abstract Completion. Sergei Artemov and Anil Nerode. Symposium on Logical Foundations of Computer Science LFCS'07, Jun 2007, New York, United States. Springer Verlag, 4514, pp.115-131, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-72734-7_9〉. 〈inria-00115556v3〉

Partager

Métriques

Consultations de la notice

223

Téléchargements de fichiers

102