Cut Admissibility by Saturation

Abstract : Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with *conditional* term rewriting rules.
Type de document :
Communication dans un congrès
Gilles Dowek. Joint International Conference, RTA-TLCA 2014, Jul 2014, Vienna, Austria. Springer, 8560, pp.124-138, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08918-8_9〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01097428
Contributeur : Guillaume Burel <>
Soumis le : vendredi 19 décembre 2014 - 15:59:35
Dernière modification le : mardi 10 juillet 2018 - 17:02:03
Document(s) archivé(s) le : lundi 23 mars 2015 - 18:28:36

Fichier

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

Identifiants

Collections

Citation

Guillaume Burel. Cut Admissibility by Saturation. Gilles Dowek. Joint International Conference, RTA-TLCA 2014, Jul 2014, Vienna, Austria. Springer, 8560, pp.124-138, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08918-8_9〉. 〈hal-01097428〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

81