Rewriting modulo in Deduction modulo

Abstract : We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computable closure for ensuring the termination of the combination of rewriting and beta-reduction. Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computable closure. This includes equations like associativity and commutativity, and provides an original treatment of termination modulo equations.
Type de document :
Communication dans un congrès
Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Jun 2003, Valencia, Spain. 2706, 2003, LNCS
Liste complète des métadonnées

https://hal.inria.fr/inria-00105625
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 16:34:37
Dernière modification le : jeudi 10 mai 2018 - 02:06:34
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:24:55

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Rewriting modulo in Deduction modulo. Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Jun 2003, Valencia, Spain. 2706, 2003, LNCS. 〈inria-00105625〉

Partager

Métriques

Consultations de la notice

100

Téléchargements de fichiers

64