Sciweavers

Share
CORR
2006
Springer

Rewriting modulo in Deduction modulo

10 years 4 months ago
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.
Frédéric Blanqui
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CORR
Authors Frédéric Blanqui
Comments (0)
books