Constrained rewriting in recognizable theories

Abstract. Rewriting has long been shown useful for equational reasoning but its expressive power is not always appropriate for certain situations, as for instance when dealing with relations over terms. That is why some generalizations of rewriting, such as strategic rewriting, conditional or constrained rewriting, have emerged. In particular, constraints over terms are very suitable to define sets of terms thanks to logic formulae. Works on constrained rewriting mainly focus on term algebra constraints (equality, disequality, matching, etc.) with a fixed predicate interpretation. We propose in this paper a notion of constrained rewriting whose constraints are first order formulae and we we concentrate on formulae whose predicates are freely interpreted as recognizables relations on tuples. We then then characterize a class of first order formulae for which we can decide the step of constrained rewriting. 1