Grid structures and undecidable constraint theories

Abstract

We express conditions for a term to be a finite grid-like structure. Together with definitions of term properties by excluding "forbidden patterns" we obtain three new undecidability results in three areas: the Ǝ*ᵄ*-fragment of the theory of one-step rewriting for linear and shallow rewrite systems, the emptiness for automata with equality tests between first cousins (i.e. only tests at depth 2 below the current node are available), and the Ǝ*ᵄ*-fragment of the theory of set constraints.