Automata for Reduction Properties Solving

We introduce a new class of tree automata, which we call Reduction Automata (RA), and we use it to prove the decidability of the whole first order of theory of reduction (the theory of reduction is the set of true sentences built up with unary predicates redt(x) "x is reducible by t", i.e. "some instance of t is a subterm of x"). So we link rewriting, logic and formal languages.