These slides show how to decide equivalence of tree-to-string transducers using the Hilbert Basis Theorem. The idea is based on

Helmut Seidl, Sebastian Maneth, Gregor Kemper:
Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable. FOCS 2015: 943-962

There are two parts:

1. consider grammars that generate tuples of rational numbers, and use the Hilbert Basis Theorem to show that the following is decidable: “given a grammar, decide if the only tuple that it generates is the zero tuple”. slides
2. reduce the equivalence problem for transducers to the zero-ness problem discussed above. slides