Undecidable properties of flat term rewrite systems (Q734041)

Reachability, joinability, termination or strong normalization, confluence, weak normalization, and unique normalization are some fundamental properties of term rewrite systems (TRS) that are known to be undecidable in general. Their decidablity has been investigated for some particular classes. In this paper, the authors give new simple proofs for the undecidability of reachability, joinability, and confluence for flat TRS. They also give proofs for the undecidability of weak and unique normalizations for flat TRS.