We introduce a new class of tree automata, which we call Reduction Aut
omata (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 t
rue sentences built up with unary predicates red(t)(x) ''x is reducibl
e by t'', i.e. ''some instance of t is a subterm of x''). So we link r
ewriting, logic and formal languages.