The Hilbert method for transducer equivalence

This Hilbert Method, as discussed in this paper, is the idea to encode combinatorial objects used by automata, such as words or trees, into algebraic objects, such as numbers and polynomials, and to reason about the latter using results about polynomials like Hilbert's Basis Theorem. A typical application of the method is deciding of equivalence for string-to-string transducers that use registers.