We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(2^{2^{poly(n)}},O(n)). Providing a matching lower bound, we show that there is some fixed ground tree rewrite graph whose first-order theory is hard for ATIME(2^{2^{poly(n)}},poly(n)) with respect to logspace reductions. Finally, we prove that there exists a fixed ground tree rewrite graph together with a single unary predicate in form of a regular tree language such that the resulting structure has a non-elementary first-order theory.

Comment: accepted for Logical Methods in Computer Science

• 03D05 - Automata and formal grammars in connection with logical questions
• 03D15 - Complexity of computation (including implicit computational complexity)
• 68Q15 - Complexity classes (hierarchies, relations among complexity classes, etc.)
• 68Q17 - Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
• 68Q25 - Analysis of algorithms and problem complexity
• 68Q42 - Grammars and rewriting systems