Thue trees (Q1861534)

A new technique is introduced to prove undecidability results. This technique is based on the notion of a Thue tree. Also, examples are given how to apply this method to term rewriting, the Horn implication problem, and data dependencies. The strategy of proving undecidability results adapted in this paper is to reduce the problem of existence of a finite Thue tree to the problem under consideration.