In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. (from nLab).

References:
nLab