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 dened by higherorder rewrite rules. In a previous work, we dened general syntactic conditions based on the notion of computability closure for ensuring the termination of the combination of rewriting and -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 nite, the equations are linear and satisfy general syntactic conditions also based on the notion of computability closure. This includes equations like associativity and commutativity and provides an original treatment of termination modulo equations.

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Frédéric Blanqui
• Keywords: Computability Closure, CORR 2006, Education, Equations, General Syntactic Conditions