The First-Order Theory of Ground Tree Rewrite Graphs

Authors Stefan Göller, Markus Lohrey

Thumbnail PDF


  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Author Details

Stefan Göller
Markus Lohrey

Cite AsGet BibTex

Stefan Göller and Markus Lohrey. The First-Order Theory of Ground Tree Rewrite Graphs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 276-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


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.
  • ground tree rewriting systems
  • first-order theories
  • complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads