THE COMPLEXITY OF THE FIRST-ORDER THEORY OF GROUND TREE REWRITE GRAPHS
Stefan Göller, Markus Lohrey · 2014
The uniform first-order theory of ground tree rewrite graphs is the set of all pairs consisting of a ground tree rewrite system and a first-order sentence that holds in the graph defined by the ground tree rewrite system. We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(22 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(22 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.